Theorem 0cn 8282

Description: 0 is a complex number. (Contributed by NM, 19-Feb-2005.)

Assertion

Ref	Expression
0cn	|- 0 e. CC

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 8248	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 8238	. . . 4 |- _i e. CC
3		mulcl 8270	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 426	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 8236	. . 3 |- 1 e. CC
6		addcl 8268	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 426	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2308	1 |- 0 e. CC

Syntax hints:   e. wcel 2205  (class class class)co 6058   CCcc 8141   0cc0 8143   1c1 8144   _ici 8145   + caddc 8146   x. cmul 8148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  0cnd  8283  c0ex  8284  addlid  8428  00id  8430  cnegexlem2  8465  negcl  8489  subid  8508  subid1  8509  neg0  8535  negid  8536  negsub  8537  subneg  8538  negneg  8539  negeq0  8543  negsubdi  8545  renegcl  8550  mul02  8677  mul01  8679  mulneg1  8685  ixi  8874  negap0  8921  muleqadd  8959  divvalap  8965  div0ap  8993  recgt0  9141  0m0e0  9366  2muline0  9480  elznn0  9609  ser0  10919  0exp0e1  10930  expeq0  10956  0exp  10960  sq0  11016  bcval5  11150  shftval3  11537  shftidt2  11542  cjap0  11617  cjne0  11618  abs0  11768  abs2dif  11816  clim0  11995  climz  12002  serclim0  12015  sumrbdclem  12088  fsum3cvg  12089  summodclem3  12091  summodclem2a  12092  fisumss  12103  fsumrelem  12182  ef0  12383  eftlub  12401  sin0  12440  tan0  12442  4sqlem11  13124  cncrng  14843  cnfld0  14845  cnbl0  15525  cnblcld  15526  dvconst  15685  dvconstre  15687  dvconstss  15689  dvcnp2cntop  15690  dvrecap  15704  dveflem  15717  plyun0  15727  plycjlemc  15751  plycj  15752  dvply2g  15757  sinhalfpilem  15782  sin2kpi  15802  cos2kpi  15803  sinkpi  15838  1sgm2ppw  15989  trimul0or  16971  dcapnconst  16973