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  8466  00id  8468  cnegexlem2  8503  negcl  8527  subid  8546  subid1  8547  neg0  8573  negid  8574  negsub  8575  subneg  8576  negneg  8577  negeq0  8581  negsubdi  8583  renegcl  8588  mul02  8715  mul01  8717  mulneg1  8723  ixi  8913  negap0  8960  muleqadd  9000  divvalap  9006  div0ap  9034  recgt0  9182  0m0e0  9418  2muline0  9534  elznn0  9663  ser0  10983  0exp0e1  10994  expeq0  11020  0exp  11024  sq0  11080  bcval5  11215  shftval3  11606  shftidt2  11611  cjap0  11687  cjne0  11688  abs0  11838  abs2dif  11887  clim0  12067  climz  12074  serclim0  12087  sumrbdclem  12160  fsum3cvg  12161  summodclem3  12163  summodclem2a  12164  fisumss  12175  fsumrelem  12254  ef0  12455  eftlub  12473  sin0  12512  tan0  12514  4sqlem11  13200  cncrng  14955  cnfld0  14957  cnbl0  15684  cnblcld  15685  dvconst  15844  dvconstre  15846  dvconstss  15848  dvcnp2cntop  15849  dvrecap  15863  dveflem  15876  plyun0  15886  plycjlemc  15910  plycj  15911  dvply2g  15916  sinhalfpilem  15942  sin2kpi  15962  cos2kpi  15963  sinkpi  15998  1sgm2ppw  16190  dcapnconst  17209