Theorem 0cn 6481

Description: 0 is a complex number.

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		axi2m1 6438	. 2 |- ((_i x. _i) + 1) = 0
2		axicn 6423	. . . 4 |- _i e. CC
3	2, 2	mulcli 6474	. . 3 |- (_i x. _i) e. CC
4		ax1cn 6422	. . 3 |- 1 e. CC
5	3, 4	addcli 6473	. 2 |- ((_i x. _i) + 1) e. CC
6	1, 5	eqeltrri 1968	1 |- 0 e. CC

Syntax hints:   e. wcel 1300  (class class class)co 4884  CCcc 6384  0cc0 6386  1c1 6387  _ici 6388   + caddc 6389   x. cmul 6391

This theorem is referenced by:  addid2 6482  cnegexlem2 6500  addcan 6507  subcl 6524  negcl 6525  subadd 6532  negid 6536  negsub 6540  subid1i 6552  negneg 6553  subid 6555  subid1 6556  neg11i 6566  neg11 6569  neg0 6575  renegcli 6576  renegcliOLD 6577  mul01i 6594  mul02i 6595  1re 6598  0re 6603  mul01 6606  mul02 6607  mulneg1i 6608  negdii 6611  mulneg1 6615  mul2negOLD 6619  negdi 6620  nncanOLD 6636  addgt0i 6775  addge0i 6777  addge0iOLD 6778  add20i 6782  addgt0 6831  addgegt0 6833  addgtge0 6835  addge0 6837  ixi 6872  recextlem2 6875  mul0ori 6882  mul0or 6884  muleqadd 6889  divmul 6896  divcl 6901  divcan1 6909  divne0b 6911  recne0 6915  recid 6918  divrec 6922  divdir 6933  divcan3 6938  div0 6943  diveq0 6944  eqnegi 6982  eqneg 6983  2times 7188  elnn0 7310  nn0addcl 7329  elznn0 7358  nn0sub 7370  zltp1le 7390  shftval3 7761  shftidt 7768  seq1seqz 7784  seq0seqz 7785  seq00 7793  0exp 7832  exple1 7852  sumsqne0i 7879  sq0 7880  sqeqor 7895  binom2 7896  discrlem3 7908  sqr0 7922  sqrlem6 7928  sqrthi 7949  crne0i 7989  rimul 7994  cjreb 8050  cjmulrcl 8051  cjmulge0 8053  reneg 8054  readd 8055  imneg 8057  imadd 8058  cjcj 8061  cjadd 8062  cjmul 8063  cjneg 8064  addcj 8065  re0 8070  im0 8071  cj0 8076  cjne0 8082  abs00i 8093  absval2 8103  abs00 8104  absge0 8105  absmul 8109  absdiv 8111  abs0 8129  cjdiv 8141  absgt0 8145  abssub 8146  abstri 8150  abs2dif 8154  abs1mi 8156  abs3lem 8159  faclbnd 8197  faclbnd3 8199  faclbnd4lem3 8202  bcpasci 8221  fsum0 8299  serz0 8313  binomlem1 8326  binomlem4 8329  binomi 8332  clm0i 8343  clm0nnsi 8345  clm0ii 8349  clim0 8357  climuni 8359  iserzshft2i 8367  climuz0i 8368  serzclim0 8369  caucvg3 8428  serzf0i 8429  ser10 8432  ser1clim0 8433  cvgcmp3cetlem1 8449  infcvglem2 8483  arisumi 8487  explecnv 8495  geolim 8499  geolim1 8501  fsum0diag 8520  mulc1cncf 8541  efseq1ex 8568  ef0lem 8572  ef0 8597  efcj 8599  efadd 8629  ef4pi 8664  ef4p 8665  efcnlem4 8687  sin0ALT 8710  sinadd 8718  cosadd 8719  bcth 9310  cnaddabl 9434  cnid 9435  addinv 9436  vc0 9520  vcz 9521  vcoprne 9530  ip0r 9709  ipasslem8 9838  pythi 9851  siilem2 9853  minveclem30 9919  sinkpi 10063  pilog 10122  avril1 10142  hvmul0 10525  hi01 10595  norm-iii 10640  normpythi 10642  ocsh 10789  pjthlem8 10859  pjthlem9 10860  h1de2ctlem 11111  pjmuli 11269  pjneli 11303  eigre 11398  eigorth 11401  0cnfn 11541  0lnfn 11546  lnopeq0i 11569  lnopunilem2 11573  lnfnconi 11627  nlelshi 11630  unierri 11674  abs2sqle 13624  abs2sqlt 13625  divalglem9 13704  cntrsetlem 14999  fsumleisumi 15826  lmclim2 15850  idcncf 15884  totbndbnd 15944  heiborlem6 15960  heiborlem11 15965  heiborlem12 15966  heiborlem14 15968  heiborlem16 15970  heiborlem18 15972  bfplem8 16005  bfp 16009  reparpht 16065  pcopt 16084  cnaddablNEW 17139  cnaddablxNEW 17140

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398

Copyright terms: Public domain