Theorem 0cn 8324

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 8290	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8280	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8312	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 430	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8278	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8310	. . 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 6088  ℂcc 8183  0cc0 8185  1c1 8186  ici 8187   + caddc 8188   · cmul 8190

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 8278  ax-icn 8280  ax-addcl 8281  ax-mulcl 8283  ax-i2m1 8290

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

This theorem is used by:  0cnd  8325  c0ex  8326  addlid  8472  00id  8474  cnegexlem2  8509  negcl  8533  subid  8552  subid1  8553  neg0  8579  negid  8580  negsub  8581  subneg  8582  negneg  8583  negeq0  8587  negsubdi  8589  renegcl  8594  mul02  8721  mul01  8723  mulneg1  8729  ixi  8919  negap0  8966  muleqadd  9006  divvalap  9012  div0ap  9040  recgt0  9188  0m0e0  9425  2muline0  9541  elznn0  9668  ser0  10990  0exp0e1  11001  expeq0  11027  0exp  11031  sq0  11087  bcval5  11222  shftval3  11613  shftidt2  11618  cjap0  11694  cjne0  11695  abs0  11845  abs2dif  11894  clim0  12075  climz  12082  serclim0  12095  sumrbdclem  12168  fsum3cvg  12169  summodclem3  12171  summodclem2a  12172  fisumss  12183  fsumrelem  12262  ef0  12463  eftlub  12481  sin0  12520  tan0  12522  4sqlem11  13208  cncrng  15014  cnfld0  15016  cnbl0  15777  cnblcld  15778  dvconst  15937  dvconstre  15939  dvconstss  15941  dvcnp2cntop  15942  dvrecap  15956  dveflem  15969  plyun0  15979  plycjlemc  16003  plycj  16004  dvply2g  16009  sinhalfpilem  16035  sin2kpi  16055  cos2kpi  16056  sinkpi  16091  1sgm2ppw  16306  dcapnconst  17335