Theorem 0cn 7577

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 7547	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 7537	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7566	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 418	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 7535	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7564	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 418	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2168	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 1445  (class class class)co 5690  ℂcc 7445  0cc0 7447  1c1 7448  ici 7449   + caddc 7450   · cmul 7452

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077  ax-1cn 7535  ax-icn 7537  ax-addcl 7538  ax-mulcl 7540  ax-i2m1 7547

This theorem depends on definitions:  df-bi 116  df-cleq 2088  df-clel 2091

This theorem is referenced by:  0cnd  7578  c0ex  7579  addid2  7718  00id  7720  cnegexlem2  7755  negcl  7779  subid  7798  subid1  7799  neg0  7825  negid  7826  negsub  7827  subneg  7828  negneg  7829  negeq0  7833  negsubdi  7835  renegcl  7840  mul02  7962  mul01  7964  mulneg1  7970  ixi  8157  negap0  8203  muleqadd  8234  divvalap  8238  div0ap  8266  recgt0  8408  0m0e0  8632  2muline0  8739  elznn0  8863  ser0  10064  0exp0e1  10075  expeq0  10101  0exp  10105  sq0  10160  bcval5  10286  shftval3  10376  shftidt2  10381  cjap0  10456  cjne0  10457  abs0  10606  abs00  10612  abs2dif  10654  clim0  10828  climz  10835  serclim0  10848  sumrbdclem  10919  fsum3cvg  10920  summodclem3  10923  summodclem2a  10924  fisumss  10935  fsumrelem  11014  ef0  11111  eftlub  11129  sin0  11169  tan0  11171  cnbl0  12311  cnblcld  12312