Theorem 0cn 8324

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 8290	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8280	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8312	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 430	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8278	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8310	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 430	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2312	1 ⊢ 0 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6088  ℂcc 8183  0cc0 8185  1c1 8186  ici 8187   + caddc 8188   · cmul 8190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  0cnd  8325  c0ex  8326  addlid  8472  00id  8474  cnegexlem2  8509  negcl  8533  subid  8552  subid1  8553  neg0  8579  negid  8580  negsub  8581  subneg  8582  negneg  8583  negeq0  8587  negsubdi  8589  renegcl  8594  mul02  8721  mul01  8723  mulneg1  8729  ixi  8919  negap0  8966  muleqadd  9006  divvalap  9012  div0ap  9040  recgt0  9188  0m0e0  9425  2muline0  9541  elznn0  9670  ser0  10991  0exp0e1  11002  expeq0  11028  0exp  11032  sq0  11088  bcval5  11223  shftval3  11614  shftidt2  11619  cjap0  11695  cjne0  11696  abs0  11846  abs2dif  11895  clim0  12076  climz  12083  serclim0  12096  sumrbdclem  12169  fsum3cvg  12170  summodclem3  12172  summodclem2a  12173  fisumss  12184  fsumrelem  12263  ef0  12464  eftlub  12482  sin0  12521  tan0  12523  4sqlem11  13209  cncrng  15015  cnfld0  15017  cnbl0  15760  cnblcld  15761  dvconst  15920  dvconstre  15922  dvconstss  15924  dvcnp2cntop  15925  dvrecap  15939  dveflem  15952  plyun0  15962  plycjlemc  15986  plycj  15987  dvply2g  15992  sinhalfpilem  16018  sin2kpi  16038  cos2kpi  16039  sinkpi  16074  1sgm2ppw  16289  dcapnconst  17318