Theorem 0cn 8319

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 8285	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8275	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8307	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 430	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8273	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8305	. . 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 8178  0cc0 8180  1c1 8181  ici 8182   + caddc 8183   · cmul 8185

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 8273  ax-icn 8275  ax-addcl 8276  ax-mulcl 8278  ax-i2m1 8285

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

This theorem is used by:  0cnd  8320  c0ex  8321  addlid  8467  00id  8469  cnegexlem2  8504  negcl  8528  subid  8547  subid1  8548  neg0  8574  negid  8575  negsub  8576  subneg  8577  negneg  8578  negeq0  8582  negsubdi  8584  renegcl  8589  mul02  8716  mul01  8718  mulneg1  8724  ixi  8914  negap0  8961  muleqadd  9001  divvalap  9007  div0ap  9035  recgt0  9183  0m0e0  9419  2muline0  9535  elznn0  9664  ser0  10985  0exp0e1  10996  expeq0  11022  0exp  11026  sq0  11082  bcval5  11217  shftval3  11608  shftidt2  11613  cjap0  11689  cjne0  11690  abs0  11840  abs2dif  11889  clim0  12070  climz  12077  serclim0  12090  sumrbdclem  12163  fsum3cvg  12164  summodclem3  12166  summodclem2a  12167  fisumss  12178  fsumrelem  12257  ef0  12458  eftlub  12476  sin0  12515  tan0  12517  4sqlem11  13203  cncrng  14990  cnfld0  14992  cnbl0  15726  cnblcld  15727  dvconst  15886  dvconstre  15888  dvconstss  15890  dvcnp2cntop  15891  dvrecap  15905  dveflem  15918  plyun0  15928  plycjlemc  15952  plycj  15953  dvply2g  15958  sinhalfpilem  15984  sin2kpi  16004  cos2kpi  16005  sinkpi  16040  1sgm2ppw  16250  dcapnconst  17278