Theorem 0cn 8149

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 8115	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8105	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8137	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8103	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8135	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2303	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2200  (class class class)co 6007  ℂcc 8008  0cc0 8010  1c1 8011  ici 8012   + caddc 8013   · cmul 8015

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8103  ax-icn 8105  ax-addcl 8106  ax-mulcl 8108  ax-i2m1 8115

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

This theorem is referenced by:  0cnd  8150  c0ex  8151  addlid  8296  00id  8298  cnegexlem2  8333  negcl  8357  subid  8376  subid1  8377  neg0  8403  negid  8404  negsub  8405  subneg  8406  negneg  8407  negeq0  8411  negsubdi  8413  renegcl  8418  mul02  8544  mul01  8546  mulneg1  8552  ixi  8741  negap0  8788  muleqadd  8826  divvalap  8832  div0ap  8860  recgt0  9008  0m0e0  9233  2muline0  9347  elznn0  9472  ser0  10767  0exp0e1  10778  expeq0  10804  0exp  10808  sq0  10864  bcval5  10997  shftval3  11353  shftidt2  11358  cjap0  11433  cjne0  11434  abs0  11584  abs2dif  11632  clim0  11811  climz  11818  serclim0  11831  sumrbdclem  11903  fsum3cvg  11904  summodclem3  11906  summodclem2a  11907  fisumss  11918  fsumrelem  11997  ef0  12198  eftlub  12216  sin0  12255  tan0  12257  4sqlem11  12939  cncrng  14548  cnfld0  14550  cnbl0  15223  cnblcld  15224  dvconst  15383  dvconstre  15385  dvconstss  15387  dvcnp2cntop  15388  dvrecap  15402  dveflem  15415  plyun0  15425  plycjlemc  15449  plycj  15450  dvply2g  15455  sinhalfpilem  15480  sin2kpi  15500  cos2kpi  15501  sinkpi  15536  1sgm2ppw  15684  dcapnconst  16489