Theorem 0cn 7019

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 6989	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 6979	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7008	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 402	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 6977	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7006	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 402	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2111	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 1393  (class class class)co 5512  ℂcc 6887  0cc0 6889  1c1 6890  ici 6891   + caddc 6892   · cmul 6894

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-1cn 6977  ax-icn 6979  ax-addcl 6980  ax-mulcl 6982  ax-i2m1 6989

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036

This theorem is referenced by:  0cnd  7020  c0ex  7021  addid2  7152  00id  7154  cnegexlem2  7187  negcl  7211  subid  7230  subid1  7231  neg0  7257  negid  7258  negsub  7259  subneg  7260  negneg  7261  negeq0  7265  negsubdi  7267  renegcl  7272  mul02  7384  mul01  7386  mulneg1  7392  ixi  7574  negap0  7620  muleqadd  7649  divvalap  7653  div0ap  7679  recgt0  7816  0m0e0  8029  2muline0  8150  elznn0  8260  iser0  9250  0exp0e1  9260  expeq0  9286  0exp  9290  sq0  9344  shftval3  9428  shftidt2  9433  cjap0  9507  cjne0  9508  abs0  9656  abs00  9662  abs2dif  9702  clim0  9806  climz  9813  iserclim0  9826