Theorem 0cn 7424

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 7394	. 2 |- ( ( _i x. _i ) + 1 ) = 0
2		ax-icn 7384	. . . 4 |- _i e. CC
3		mulcl 7413	. . . 4 |- ( ( _i e. CC /\ _i e. CC ) -> ( _i x. _i ) e. CC )
4	2, 2, 3	mp2an 417	. . 3 |- ( _i x. _i ) e. CC
5		ax-1cn 7382	. . 3 |- 1 e. CC
6		addcl 7411	. . 3 |- ( ( ( _i x. _i ) e. CC /\ 1 e. CC ) -> ( ( _i x. _i ) + 1 ) e. CC )
7	4, 5, 6	mp2an 417	. 2 |- ( ( _i x. _i ) + 1 ) e. CC
8	1, 7	eqeltrri 2158	1 |- 0 e. CC

Syntax hints:   e. wcel 1436  (class class class)co 5613   CCcc 7292   0cc0 7294   1c1 7295   _ici 7296   + caddc 7297   x. cmul 7299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067  ax-1cn 7382  ax-icn 7384  ax-addcl 7385  ax-mulcl 7387  ax-i2m1 7394

This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081

This theorem is referenced by:  0cnd  7425  c0ex  7426  addid2  7565  00id  7567  cnegexlem2  7602  negcl  7626  subid  7645  subid1  7646  neg0  7672  negid  7673  negsub  7674  subneg  7675  negneg  7676  negeq0  7680  negsubdi  7682  renegcl  7687  mul02  7809  mul01  7811  mulneg1  7817  ixi  8001  negap0  8047  muleqadd  8076  divvalap  8080  div0ap  8108  recgt0  8246  0m0e0  8469  2muline0  8574  elznn0  8698  iser0  9847  0exp0e1  9858  expeq0  9884  0exp  9888  sq0  9943  ibcval5  10067  shftval3  10157  shftidt2  10162  cjap0  10236  cjne0  10237  abs0  10386  abs00  10392  abs2dif  10434  clim0  10566  climz  10573  iserclim0  10586  isumrblem  10655  fisumcvg  10656  isummolem3  10659  isummolem2a  10660  fisumss  10670