Theorem 0cn 7173

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 7143	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 7133	. . . 4 ⊢ i ∈ ℂ
3		mulcl 7162	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 417	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 7131	. . 3 ⊢ 1 ∈ ℂ
6		addcl 7160	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 417	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2153	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 1434  (class class class)co 5543  ℂcc 7041  0cc0 7043  1c1 7044  ici 7045   + caddc 7046   · cmul 7048

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1cn 7131  ax-icn 7133  ax-addcl 7134  ax-mulcl 7136  ax-i2m1 7143

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078

This theorem is referenced by:  0cnd  7174  c0ex  7175  addid2  7314  00id  7316  cnegexlem2  7351  negcl  7375  subid  7394  subid1  7395  neg0  7421  negid  7422  negsub  7423  subneg  7424  negneg  7425  negeq0  7429  negsubdi  7431  renegcl  7436  mul02  7558  mul01  7560  mulneg1  7566  ixi  7750  negap0  7796  muleqadd  7825  divvalap  7829  div0ap  7857  recgt0  7995  0m0e0  8218  2muline0  8323  elznn0  8447  iser0  9568  0exp0e1  9578  expeq0  9604  0exp  9608  sq0  9663  ibcval5  9787  shftval3  9853  shftidt2  9858  cjap0  9932  cjne0  9933  abs0  10082  abs00  10088  abs2dif  10130  clim0  10262  climz  10269  iserclim0  10282  isumrblem  10337  fisumcvg  10338