Theorem 0cn 8161

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 8127	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8117	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8149	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8115	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8147	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2303	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℂcc 8020  0cc0 8022  1c1 8023  ici 8024   + caddc 8025   · cmul 8027

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8115  ax-icn 8117  ax-addcl 8118  ax-mulcl 8120  ax-i2m1 8127

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  0cnd  8162  c0ex  8163  addlid  8308  00id  8310  cnegexlem2  8345  negcl  8369  subid  8388  subid1  8389  neg0  8415  negid  8416  negsub  8417  subneg  8418  negneg  8419  negeq0  8423  negsubdi  8425  renegcl  8430  mul02  8556  mul01  8558  mulneg1  8564  ixi  8753  negap0  8800  muleqadd  8838  divvalap  8844  div0ap  8872  recgt0  9020  0m0e0  9245  2muline0  9359  elznn0  9484  ser0  10785  0exp0e1  10796  expeq0  10822  0exp  10826  sq0  10882  bcval5  11015  shftval3  11378  shftidt2  11383  cjap0  11458  cjne0  11459  abs0  11609  abs2dif  11657  clim0  11836  climz  11843  serclim0  11856  sumrbdclem  11928  fsum3cvg  11929  summodclem3  11931  summodclem2a  11932  fisumss  11943  fsumrelem  12022  ef0  12223  eftlub  12241  sin0  12280  tan0  12282  4sqlem11  12964  cncrng  14573  cnfld0  14575  cnbl0  15248  cnblcld  15249  dvconst  15408  dvconstre  15410  dvconstss  15412  dvcnp2cntop  15413  dvrecap  15427  dveflem  15440  plyun0  15450  plycjlemc  15474  plycj  15475  dvply2g  15480  sinhalfpilem  15505  sin2kpi  15525  cos2kpi  15526  sinkpi  15561  1sgm2ppw  15709  dcapnconst  16601