Theorem 0cn 8154

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 8120	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8110	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8142	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8108	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8140	. . 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 6010  ℂcc 8013  0cc0 8015  1c1 8016  ici 8017   + caddc 8018   · cmul 8020

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 8108  ax-icn 8110  ax-addcl 8111  ax-mulcl 8113  ax-i2m1 8120

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

This theorem is referenced by:  0cnd  8155  c0ex  8156  addlid  8301  00id  8303  cnegexlem2  8338  negcl  8362  subid  8381  subid1  8382  neg0  8408  negid  8409  negsub  8410  subneg  8411  negneg  8412  negeq0  8416  negsubdi  8418  renegcl  8423  mul02  8549  mul01  8551  mulneg1  8557  ixi  8746  negap0  8793  muleqadd  8831  divvalap  8837  div0ap  8865  recgt0  9013  0m0e0  9238  2muline0  9352  elznn0  9477  ser0  10772  0exp0e1  10783  expeq0  10809  0exp  10813  sq0  10869  bcval5  11002  shftval3  11359  shftidt2  11364  cjap0  11439  cjne0  11440  abs0  11590  abs2dif  11638  clim0  11817  climz  11824  serclim0  11837  sumrbdclem  11909  fsum3cvg  11910  summodclem3  11912  summodclem2a  11913  fisumss  11924  fsumrelem  12003  ef0  12204  eftlub  12222  sin0  12261  tan0  12263  4sqlem11  12945  cncrng  14554  cnfld0  14556  cnbl0  15229  cnblcld  15230  dvconst  15389  dvconstre  15391  dvconstss  15393  dvcnp2cntop  15394  dvrecap  15408  dveflem  15421  plyun0  15431  plycjlemc  15455  plycj  15456  dvply2g  15461  sinhalfpilem  15486  sin2kpi  15506  cos2kpi  15507  sinkpi  15542  1sgm2ppw  15690  dcapnconst  16543