Theorem 0cn 8063

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 8029	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8019	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8051	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8017	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8049	. . 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 5943  ℂcc 7922  0cc0 7924  1c1 7925  ici 7926   + caddc 7927   · cmul 7929

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 8017  ax-icn 8019  ax-addcl 8020  ax-mulcl 8022  ax-i2m1 8029

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

This theorem is referenced by:  0cnd  8064  c0ex  8065  addlid  8210  00id  8212  cnegexlem2  8247  negcl  8271  subid  8290  subid1  8291  neg0  8317  negid  8318  negsub  8319  subneg  8320  negneg  8321  negeq0  8325  negsubdi  8327  renegcl  8332  mul02  8458  mul01  8460  mulneg1  8466  ixi  8655  negap0  8702  muleqadd  8740  divvalap  8746  div0ap  8774  recgt0  8922  0m0e0  9147  2muline0  9261  elznn0  9386  ser0  10676  0exp0e1  10687  expeq0  10713  0exp  10717  sq0  10773  bcval5  10906  shftval3  11080  shftidt2  11085  cjap0  11160  cjne0  11161  abs0  11311  abs2dif  11359  clim0  11538  climz  11545  serclim0  11558  sumrbdclem  11630  fsum3cvg  11631  summodclem3  11633  summodclem2a  11634  fisumss  11645  fsumrelem  11724  ef0  11925  eftlub  11943  sin0  11982  tan0  11984  4sqlem11  12666  cncrng  14273  cnfld0  14275  cnbl0  14948  cnblcld  14949  dvconst  15108  dvconstre  15110  dvconstss  15112  dvcnp2cntop  15113  dvrecap  15127  dveflem  15140  plyun0  15150  plycjlemc  15174  plycj  15175  dvply2g  15180  sinhalfpilem  15205  sin2kpi  15225  cos2kpi  15226  sinkpi  15261  1sgm2ppw  15409  dcapnconst  15933