Theorem 0cn 7899

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 7866	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 7856	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7888	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 424	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 7854	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7886	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 424	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2244	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2141  (class class class)co 5850  ℂcc 7759  0cc0 7761  1c1 7762  ici 7763   + caddc 7764   · cmul 7766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7854  ax-icn 7856  ax-addcl 7857  ax-mulcl 7859  ax-i2m1 7866

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  0cnd  7900  c0ex  7901  addid2  8045  00id  8047  cnegexlem2  8082  negcl  8106  subid  8125  subid1  8126  neg0  8152  negid  8153  negsub  8154  subneg  8155  negneg  8156  negeq0  8160  negsubdi  8162  renegcl  8167  mul02  8293  mul01  8295  mulneg1  8301  ixi  8489  negap0  8536  muleqadd  8573  divvalap  8578  div0ap  8606  recgt0  8753  0m0e0  8977  2muline0  9090  elznn0  9214  ser0  10457  0exp0e1  10468  expeq0  10494  0exp  10498  sq0  10553  bcval5  10684  shftval3  10778  shftidt2  10783  cjap0  10858  cjne0  10859  abs0  11009  abs2dif  11057  clim0  11235  climz  11242  serclim0  11255  sumrbdclem  11327  fsum3cvg  11328  summodclem3  11330  summodclem2a  11331  fisumss  11342  fsumrelem  11421  ef0  11622  eftlub  11640  sin0  11679  tan0  11681  cnbl0  13287  cnblcld  13288  dvconst  13414  dvcnp2cntop  13416  dvrecap  13430  dveflem  13440  sinhalfpilem  13465  sin2kpi  13485  cos2kpi  13486  sinkpi  13521  dcapnconst  14052