Theorem 0cn 7949

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 7916	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 7906	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7938	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 7904	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7936	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2251	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809  0cc0 7811  1c1 7812  ici 7813   + caddc 7814   · cmul 7816

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7904  ax-icn 7906  ax-addcl 7907  ax-mulcl 7909  ax-i2m1 7916

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  0cnd  7950  c0ex  7951  addlid  8096  00id  8098  cnegexlem2  8133  negcl  8157  subid  8176  subid1  8177  neg0  8203  negid  8204  negsub  8205  subneg  8206  negneg  8207  negeq0  8211  negsubdi  8213  renegcl  8218  mul02  8344  mul01  8346  mulneg1  8352  ixi  8540  negap0  8587  muleqadd  8625  divvalap  8631  div0ap  8659  recgt0  8807  0m0e0  9031  2muline0  9144  elznn0  9268  ser0  10514  0exp0e1  10525  expeq0  10551  0exp  10555  sq0  10611  bcval5  10743  shftval3  10836  shftidt2  10841  cjap0  10916  cjne0  10917  abs0  11067  abs2dif  11115  clim0  11293  climz  11300  serclim0  11313  sumrbdclem  11385  fsum3cvg  11386  summodclem3  11388  summodclem2a  11389  fisumss  11400  fsumrelem  11479  ef0  11680  eftlub  11698  sin0  11737  tan0  11739  cncrng  13466  cnfld0  13468  cnbl0  14037  cnblcld  14038  dvconst  14164  dvcnp2cntop  14166  dvrecap  14180  dveflem  14190  sinhalfpilem  14215  sin2kpi  14235  cos2kpi  14236  sinkpi  14271  dcapnconst  14811