Theorem 0cn 8266

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 8232	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8222	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8254	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8220	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8252	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2306	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2203  (class class class)co 6050  ℂcc 8125  0cc0 8127  1c1 8128  ici 8129   + caddc 8130   · cmul 8132

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 2214  ax-1cn 8220  ax-icn 8222  ax-addcl 8223  ax-mulcl 8225  ax-i2m1 8232

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

This theorem is referenced by:  0cnd  8267  c0ex  8268  addlid  8412  00id  8414  cnegexlem2  8449  negcl  8473  subid  8492  subid1  8493  neg0  8519  negid  8520  negsub  8521  subneg  8522  negneg  8523  negeq0  8527  negsubdi  8529  renegcl  8534  mul02  8660  mul01  8662  mulneg1  8668  ixi  8857  negap0  8904  muleqadd  8942  divvalap  8948  div0ap  8976  recgt0  9124  0m0e0  9349  2muline0  9463  elznn0  9592  ser0  10895  0exp0e1  10906  expeq0  10932  0exp  10936  sq0  10992  bcval5  11125  shftval3  11512  shftidt2  11517  cjap0  11592  cjne0  11593  abs0  11743  abs2dif  11791  clim0  11970  climz  11977  serclim0  11990  sumrbdclem  12063  fsum3cvg  12064  summodclem3  12066  summodclem2a  12067  fisumss  12078  fsumrelem  12157  ef0  12358  eftlub  12376  sin0  12415  tan0  12417  4sqlem11  13099  cncrng  14717  cnfld0  14719  cnbl0  15399  cnblcld  15400  dvconst  15559  dvconstre  15561  dvconstss  15563  dvcnp2cntop  15564  dvrecap  15578  dveflem  15591  plyun0  15601  plycjlemc  15625  plycj  15626  dvply2g  15631  sinhalfpilem  15656  sin2kpi  15676  cos2kpi  15677  sinkpi  15712  1sgm2ppw  15863  trimul0or  16845  dcapnconst  16847