Theorem 0cn 8171

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 8137	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8127	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8159	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8125	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8157	. . 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 6018  ℂcc 8030  0cc0 8032  1c1 8033  ici 8034   + caddc 8035   · cmul 8037

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 8125  ax-icn 8127  ax-addcl 8128  ax-mulcl 8130  ax-i2m1 8137

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

This theorem is referenced by:  0cnd  8172  c0ex  8173  addlid  8318  00id  8320  cnegexlem2  8355  negcl  8379  subid  8398  subid1  8399  neg0  8425  negid  8426  negsub  8427  subneg  8428  negneg  8429  negeq0  8433  negsubdi  8435  renegcl  8440  mul02  8566  mul01  8568  mulneg1  8574  ixi  8763  negap0  8810  muleqadd  8848  divvalap  8854  div0ap  8882  recgt0  9030  0m0e0  9255  2muline0  9369  elznn0  9494  ser0  10796  0exp0e1  10807  expeq0  10833  0exp  10837  sq0  10893  bcval5  11026  shftval3  11392  shftidt2  11397  cjap0  11472  cjne0  11473  abs0  11623  abs2dif  11671  clim0  11850  climz  11857  serclim0  11870  sumrbdclem  11943  fsum3cvg  11944  summodclem3  11946  summodclem2a  11947  fisumss  11958  fsumrelem  12037  ef0  12238  eftlub  12256  sin0  12295  tan0  12297  4sqlem11  12979  cncrng  14589  cnfld0  14591  cnbl0  15264  cnblcld  15265  dvconst  15424  dvconstre  15426  dvconstss  15428  dvcnp2cntop  15429  dvrecap  15443  dveflem  15456  plyun0  15466  plycjlemc  15490  plycj  15491  dvply2g  15496  sinhalfpilem  15521  sin2kpi  15541  cos2kpi  15542  sinkpi  15577  1sgm2ppw  15725  dcapnconst  16692