Theorem 0cn 7782

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 7749	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 7739	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7771	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 423	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 7737	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7769	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 423	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2214	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 1481  (class class class)co 5782  ℂcc 7642  0cc0 7644  1c1 7645  ici 7646   + caddc 7647   · cmul 7649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1cn 7737  ax-icn 7739  ax-addcl 7740  ax-mulcl 7742  ax-i2m1 7749

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  0cnd  7783  c0ex  7784  addid2  7925  00id  7927  cnegexlem2  7962  negcl  7986  subid  8005  subid1  8006  neg0  8032  negid  8033  negsub  8034  subneg  8035  negneg  8036  negeq0  8040  negsubdi  8042  renegcl  8047  mul02  8173  mul01  8175  mulneg1  8181  ixi  8369  negap0  8416  muleqadd  8453  divvalap  8458  div0ap  8486  recgt0  8632  0m0e0  8856  2muline0  8969  elznn0  9093  ser0  10318  0exp0e1  10329  expeq0  10355  0exp  10359  sq0  10414  bcval5  10541  shftval3  10631  shftidt2  10636  cjap0  10711  cjne0  10712  abs0  10862  abs2dif  10910  clim0  11086  climz  11093  serclim0  11106  sumrbdclem  11178  fsum3cvg  11179  summodclem3  11181  summodclem2a  11182  fisumss  11193  fsumrelem  11272  ef0  11415  eftlub  11433  sin0  11472  tan0  11474  cnbl0  12742  cnblcld  12743  dvconst  12869  dvcnp2cntop  12871  dvrecap  12885  dveflem  12895  sinhalfpilem  12920  sin2kpi  12940  cos2kpi  12941  sinkpi  12976