Theorem 0cn 5393

Description: 0 is a complex number.

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		axi2m1 5350	. 2 |- ((i x. i) + 1) = 0
2		axicn 5335	. . . 4 |- i e. CC
3	2, 2	mulcli 5386	. . 3 |- (i x. i) e. CC
4		ax1cn 5334	. . 3 |- 1 e. CC
5	3, 4	addcli 5385	. 2 |- ((i x. i) + 1) e. CC
6	1, 5	eqeltrri 1592	1 |- 0 e. CC

Syntax hints:   e. wcel 999  (class class class)co 4021  CCcc 5297  0cc0 5299  1c1 5300  ici 5301   + caddc 5302   x. cmul 5304

This theorem is referenced by:  addid2 5394  cnegexlem2 5411  addcan 5417  subcl 5432  negcl 5433  subadd 5440  negid 5444  negsub 5447  subid1i 5457  negneg 5458  subid 5460  subid1 5461  neg11i 5471  neg11 5474  neg0 5480  renegcli 5481  mul01i 5496  mul02i 5497  1re 5500  0re 5505  mul01 5508  mul02 5509  mulneg1i 5510  mulneg1 5516  mul2neg 5519  negdi 5520  nncan 5534  addge0i 5664  add20i 5667  recextlem2 5748  mul0ori 5759  mul0or 5761  muleqadd 5765  divmul 5772  divmulOLD 5773  divcl 5780  divcan1 5788  divne0b 5790  recne0 5794  recid 5797  divrec 5801  divdir 5813  divdirOLD 5814  divcan3 5819  div0 5824  diveq0 5825  eqnegi 5862  eqneg 5863  2times 6065  elnn0 6183  nn0addcl 6202  elznn0 6231  nn0sub 6243  zltp1le 6263  shftval3 6607  shftidt 6614  seq1seqz 6630  seq0seqz 6631  seq00 6639  0exp 6679  exple1 6696  sumsqne0i 6723  sq0 6724  sqeqor 6738  binom2 6739  discrlem3 6748  sqr0 6762  sqrlem6 6768  sqrthi 6789  crne0i 6829  rimul 6834  cjreb 6890  cjmulrcl 6891  cjmulge0 6893  reneg 6894  readd 6895  imneg 6897  imadd 6898  cjcj 6901  cjadd 6902  cjmul 6903  cjneg 6904  addcj 6905  re0 6910  im0 6911  cj0 6916  cjne0 6921  abs00i 6932  absval2 6942  abs00 6943  absge0 6944  absmul 6948  absdiv 6950  abs0 6967  cjdiv 6979  absgt0 6983  abssub 6984  abstri 6988  abs2dif 6992  abs1mi 6994  abs3lem 6997  faclbnd 7035  faclbnd3 7037  faclbnd4lem3 7040  bcpasci 7059  fsum0 7129  serz0 7143  binomlem1 7156  binomlem4 7159  binomi 7162  clm0i 7173  clm0nnsi 7175  clm0ii 7179  clim0 7187  climuni 7189  iserzshft2i 7197  climuz0i 7198  serzclim0 7199  caucvg3 7258  serzf0i 7259  ser1f0i 7260  ser10 7262  ser1clim0 7263  cvgcmp3cetlem1 7278  infcvglem2 7312  arisumi 7316  geolim 7327  geolim1 7329  fsum0diag 7348  mulc1cncf 7369  efseq1ex 7396  ef0lem 7400  ef0 7425  efcj 7427  efadd 7457  ef4pi 7490  ef4p 7491  efcnlem4 7513  sin0ALT 7536  sinadd 7544  cosadd 7545  bcth 8117  cnaddabl 8210  cnid 8211  addinv 8212  vc0 8272  vcz 8273  vcoprne 8282  ip0r 8454  ipasslem8 8581  pythi 8594  siilem2 8596  minveclem30 8658  pilog 8851  avril1 8867  hvmul0 8976  hi01 9045  norm-iii 9090  normpythi 9092  ocsh 9239  pjthlem8 9309  pjthlem9 9310  h1de2ctlem 9561  pjmuli 9717  pjneli 9751  eigre 9844  eigorth 9847  0cnfn 9987  0lnfn 9992  lnopeq0i 10015  lnopunilem2 10019  lnfnconi 10073  nlelshi 10076  unierri 10120  abs2sqlet 10459  abs2sqltt 10460

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-1p 5152  df-plp 5153  df-mp 5154  df-ltp 5155  df-plpr 5229  df-mpr 5230  df-enr 5231  df-nr 5232  df-plr 5233  df-mr 5234  df-0r 5236  df-1r 5237  df-m1r 5238  df-c 5305  df-0 5306  df-1 5307  df-i 5308  df-r 5309  df-plus 5310  df-mul 5311

Copyright terms: Public domain