Theorem 0cn 8318

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 8284	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8274	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8306	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 430	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8272	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8304	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 430	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2312	1 ⊢ 0 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177  0cc0 8179  1c1 8180  ici 8181   + caddc 8182   · cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1cn 8272  ax-icn 8274  ax-addcl 8275  ax-mulcl 8277  ax-i2m1 8284

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  0cnd  8319  c0ex  8320  addlid  8465  00id  8467  cnegexlem2  8502  negcl  8526  subid  8545  subid1  8546  neg0  8572  negid  8573  negsub  8574  subneg  8575  negneg  8576  negeq0  8580  negsubdi  8582  renegcl  8587  mul02  8714  mul01  8716  mulneg1  8722  ixi  8911  negap0  8958  muleqadd  8998  divvalap  9004  div0ap  9032  recgt0  9180  0m0e0  9416  2muline0  9530  elznn0  9659  ser0  10970  0exp0e1  10981  expeq0  11007  0exp  11011  sq0  11067  bcval5  11201  shftval3  11592  shftidt2  11597  cjap0  11673  cjne0  11674  abs0  11824  abs2dif  11872  clim0  12051  climz  12058  serclim0  12071  sumrbdclem  12144  fsum3cvg  12145  summodclem3  12147  summodclem2a  12148  fisumss  12159  fsumrelem  12238  ef0  12439  eftlub  12457  sin0  12496  tan0  12498  4sqlem11  13180  cncrng  14906  cnfld0  14908  cnbl0  15635  cnblcld  15636  dvconst  15795  dvconstre  15797  dvconstss  15799  dvcnp2cntop  15800  dvrecap  15814  dveflem  15827  plyun0  15837  plycjlemc  15861  plycj  15862  dvply2g  15867  sinhalfpilem  15892  sin2kpi  15912  cos2kpi  15913  sinkpi  15948  1sgm2ppw  16109  dcapnconst  17111