Theorem 0cn 8170

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

Assertion

Ref	Expression
0cn	⊢ 0 ∈ ℂ

Proof of Theorem 0cn

Step	Hyp	Ref	Expression
1		ax-i2m1 8136	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8126	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8158	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8124	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8156	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2305	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  ℂcc 8029  0cc0 8031  1c1 8032  ici 8033   + caddc 8034   · cmul 8036

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1cn 8124  ax-icn 8126  ax-addcl 8127  ax-mulcl 8129  ax-i2m1 8136

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

This theorem is referenced by:  0cnd  8171  c0ex  8172  addlid  8317  00id  8319  cnegexlem2  8354  negcl  8378  subid  8397  subid1  8398  neg0  8424  negid  8425  negsub  8426  subneg  8427  negneg  8428  negeq0  8432  negsubdi  8434  renegcl  8439  mul02  8565  mul01  8567  mulneg1  8573  ixi  8762  negap0  8809  muleqadd  8847  divvalap  8853  div0ap  8881  recgt0  9029  0m0e0  9254  2muline0  9368  elznn0  9493  ser0  10794  0exp0e1  10805  expeq0  10831  0exp  10835  sq0  10891  bcval5  11024  shftval3  11387  shftidt2  11392  cjap0  11467  cjne0  11468  abs0  11618  abs2dif  11666  clim0  11845  climz  11852  serclim0  11865  sumrbdclem  11937  fsum3cvg  11938  summodclem3  11940  summodclem2a  11941  fisumss  11952  fsumrelem  12031  ef0  12232  eftlub  12250  sin0  12289  tan0  12291  4sqlem11  12973  cncrng  14582  cnfld0  14584  cnbl0  15257  cnblcld  15258  dvconst  15417  dvconstre  15419  dvconstss  15421  dvcnp2cntop  15422  dvrecap  15436  dveflem  15449  plyun0  15459  plycjlemc  15483  plycj  15484  dvply2g  15489  sinhalfpilem  15514  sin2kpi  15534  cos2kpi  15535  sinkpi  15570  1sgm2ppw  15718  dcapnconst  16665