Theorem 0cn 8046

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 8012	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8002	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8034	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8000	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8032	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2278	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2175  (class class class)co 5934  ℂcc 7905  0cc0 7907  1c1 7908  ici 7909   + caddc 7910   · cmul 7912

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1cn 8000  ax-icn 8002  ax-addcl 8003  ax-mulcl 8005  ax-i2m1 8012

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  0cnd  8047  c0ex  8048  addlid  8193  00id  8195  cnegexlem2  8230  negcl  8254  subid  8273  subid1  8274  neg0  8300  negid  8301  negsub  8302  subneg  8303  negneg  8304  negeq0  8308  negsubdi  8310  renegcl  8315  mul02  8441  mul01  8443  mulneg1  8449  ixi  8638  negap0  8685  muleqadd  8723  divvalap  8729  div0ap  8757  recgt0  8905  0m0e0  9130  2muline0  9244  elznn0  9369  ser0  10659  0exp0e1  10670  expeq0  10696  0exp  10700  sq0  10756  bcval5  10889  shftval3  11057  shftidt2  11062  cjap0  11137  cjne0  11138  abs0  11288  abs2dif  11336  clim0  11515  climz  11522  serclim0  11535  sumrbdclem  11607  fsum3cvg  11608  summodclem3  11610  summodclem2a  11611  fisumss  11622  fsumrelem  11701  ef0  11902  eftlub  11920  sin0  11959  tan0  11961  4sqlem11  12643  cncrng  14249  cnfld0  14251  cnbl0  14924  cnblcld  14925  dvconst  15084  dvconstre  15086  dvconstss  15088  dvcnp2cntop  15089  dvrecap  15103  dveflem  15116  plyun0  15126  plycjlemc  15150  plycj  15151  dvply2g  15156  sinhalfpilem  15181  sin2kpi  15201  cos2kpi  15202  sinkpi  15237  1sgm2ppw  15385  dcapnconst  15864