HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 0cn 5300
Description: 0 is a complex number.
Assertion
Ref Expression
0cn |- 0 e. CC
Proof of Theorem 0cn
StepHypRef Expression
1 axi2m1 5257 . 2 |- ((i x. i) + 1) = 0
2 axicn 5242 . . . 4 |- i e. CC
32, 2mulcl 5293 . . 3 |- (i x. i) e. CC
4 ax1cn 5241 . . 3 |- 1 e. CC
53, 4addcl 5292 . 2 |- ((i x. i) + 1) e. CC
61, 5eqeltrr 1537 1 |- 0 e. CC
Colors of variables: wff set class
Syntax hints:   e. wcel 955  (class class class)co 3948  CCcc 5204  0cc0 5206  1c1 5207  ici 5208   + caddc 5209   x. cmul 5211
This theorem is referenced by:  addid2t 5301  cnegextlem2 5318  addcant 5324  subclt 5339  negclt 5340  subaddt 5347  negidt 5351  negsubt 5354  subid1 5364  negnegt 5365  subidt 5367  subid1t 5368  neg11 5378  neg11t 5381  neg0 5387  renegcl 5388  mul01 5403  mul02 5404  1re 5407  0re 5412  mul01t 5415  mul02t 5416  mulneg1 5417  mulneg1t 5423  mul2negt 5426  negdit 5427  nncant 5441  addge0 5573  add20 5576  recextlem2 5656  mul0or 5663  mul0ort 5665  muleqaddt 5669  divmult 5676  divclt 5681  divcan1t 5689  divcan2t 5690  divne0bt 5691  recne0t 5695  recidt 5698  divrect 5702  divdirt 5713  divcan3t 5718  div0t 5723  diveq0t 5724  eqneg 5760  eqnegt 5761  2timest 5951  elnn0 6048  nn0addclt 6067  elznn0 6096  nn0subt 6108  zltp1let 6128  shftval3t 6285  shftidt 6292  seq1seqz 6473  seq0seqz 6474  seq00 6482  0expt 6521  exple1t 6538  sq0t 6550  sumsqne0 6565  sq0 6566  sqeqort 6580  binom2t 6581  discrlem3 6588  sqr0 6602  sqrlem6 6608  sqrth 6629  crne0 6670  rimul 6675  cjrebt 6735  cjmulrclt 6736  cjmulge0t 6738  renegt 6739  readdt 6740  imnegt 6742  imaddt 6743  cjcjt 6746  cjaddt 6747  cjmult 6748  cjnegt 6749  addcjt 6750  re0 6755  im0 6756  cj0 6761  cjne0t 6766  abs00 6777  absval2t 6787  abs00t 6788  absge0t 6789  absmult 6793  absdivt 6795  abs0 6814  cjdivt 6827  absgt0t 6831  abssubt 6832  abstrit 6835  abs2dift 6839  abs1m 6841  abs3lemt 6844  faclbnd 6882  faclbnd3 6884  faclbnd4lem3 6887  bcpasc 6907  fsum0 6977  serz0 6991  binomlem1 7004  binomlem4 7007  binom 7010  clm0 7021  clm0nns 7023  clm0i 7027  clim0 7034  climuni 7036  iserzshft2 7044  climuz0 7045  serzclim0 7046  caucvg3t 7104  serzf0 7105  ser1f0 7106  ser10 7108  ser1clim0 7109  cvgcmp3cetlem1 7124  infcvglem2 7157  fnsmnt 7161  geolim 7172  geolim1 7174  fsum0diag 7193  mulc1cncf 7214  efseq1ex 7248  ef0lem 7252  ef0 7277  efcjt 7279  efaddt 7309  ef4p 7340  ef4pt 7341  efcnlem4 7362  sin0ALT 7387  sinaddt 7395  cosaddt 7396  bcth 7966  cnaddabl 8063  cnid 8064  addinv 8065  vc0 8125  vcz 8126  vcoprne 8136  ip0r 8304  ipasslem8 8428  pythi 8441  siilem2 8443  minveclem30 8505  pilog 8690  avril1 8723  hvmul0t 8814  hi01t 8883  norm-iiit 8928  normpyth 8930  ocsh 9072  pjthlem8 9141  pjthlem9 9142  h1de2ctlem 9394  pjmult 9551  pjnel 9585  eigret 9678  eigortht 9681  0cnfn 9820  0lnfn 9825  lnopeq0 9847  lnopunilem2 9851  lnfncon 9905  nlelsh 9908  unierr 9950  abs2sqlet 10279  abs2sqltt 10280
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-inf2 4597
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-fv 3188  df-rdg 3917  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-1o 4117  df-oadd 4119  df-omul 4120  df-er 4245  df-ec 4247  df-qs 4250  df-ni 4972  df-pli 4973  df-mi 4974  df-lti 4975  df-plpq 5007  df-mpq 5008  df-enq 5009  df-nq 5010  df-plq 5011  df-mq 5012  df-rq 5013  df-ltq 5014  df-1q 5015  df-np 5058  df-1p 5059  df-plp 5060  df-mp 5061  df-ltp 5062  df-plpr 5136  df-mpr 5137  df-enr 5138  df-nr 5139  df-plr 5140  df-mr 5141  df-0r 5143  df-1r 5144  df-m1r 5145  df-c 5212  df-0 5213  df-1 5214  df-i 5215  df-r 5216  df-plus 5217  df-mul 5218
Copyright terms: Public domain