Theorem 0cn 8134

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 8100	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8090	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8122	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8088	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8120	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2303	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2200  (class class class)co 6000  ℂcc 7993  0cc0 7995  1c1 7996  ici 7997   + caddc 7998   · cmul 8000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1cn 8088  ax-icn 8090  ax-addcl 8091  ax-mulcl 8093  ax-i2m1 8100

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  0cnd  8135  c0ex  8136  addlid  8281  00id  8283  cnegexlem2  8318  negcl  8342  subid  8361  subid1  8362  neg0  8388  negid  8389  negsub  8390  subneg  8391  negneg  8392  negeq0  8396  negsubdi  8398  renegcl  8403  mul02  8529  mul01  8531  mulneg1  8537  ixi  8726  negap0  8773  muleqadd  8811  divvalap  8817  div0ap  8845  recgt0  8993  0m0e0  9218  2muline0  9332  elznn0  9457  ser0  10750  0exp0e1  10761  expeq0  10787  0exp  10791  sq0  10847  bcval5  10980  shftval3  11333  shftidt2  11338  cjap0  11413  cjne0  11414  abs0  11564  abs2dif  11612  clim0  11791  climz  11798  serclim0  11811  sumrbdclem  11883  fsum3cvg  11884  summodclem3  11886  summodclem2a  11887  fisumss  11898  fsumrelem  11977  ef0  12178  eftlub  12196  sin0  12235  tan0  12237  4sqlem11  12919  cncrng  14527  cnfld0  14529  cnbl0  15202  cnblcld  15203  dvconst  15362  dvconstre  15364  dvconstss  15366  dvcnp2cntop  15367  dvrecap  15381  dveflem  15394  plyun0  15404  plycjlemc  15428  plycj  15429  dvply2g  15434  sinhalfpilem  15459  sin2kpi  15479  cos2kpi  15480  sinkpi  15515  1sgm2ppw  15663  dcapnconst  16388