Theorem 0cn 8084

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 8050	. 2 ⊢ ((i · i) + 1) = 0
2		ax-icn 8040	. . . 4 ⊢ i ∈ ℂ
3		mulcl 8072	. . . 4 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
4	2, 2, 3	mp2an 426	. . 3 ⊢ (i · i) ∈ ℂ
5		ax-1cn 8038	. . 3 ⊢ 1 ∈ ℂ
6		addcl 8070	. . 3 ⊢ (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
7	4, 5, 6	mp2an 426	. 2 ⊢ ((i · i) + 1) ∈ ℂ
8	1, 7	eqeltrri 2280	1 ⊢ 0 ∈ ℂ

Syntax hints:   ∈ wcel 2177  (class class class)co 5957  ℂcc 7943  0cc0 7945  1c1 7946  ici 7947   + caddc 7948   · cmul 7950

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188  ax-1cn 8038  ax-icn 8040  ax-addcl 8041  ax-mulcl 8043  ax-i2m1 8050

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  0cnd  8085  c0ex  8086  addlid  8231  00id  8233  cnegexlem2  8268  negcl  8292  subid  8311  subid1  8312  neg0  8338  negid  8339  negsub  8340  subneg  8341  negneg  8342  negeq0  8346  negsubdi  8348  renegcl  8353  mul02  8479  mul01  8481  mulneg1  8487  ixi  8676  negap0  8723  muleqadd  8761  divvalap  8767  div0ap  8795  recgt0  8943  0m0e0  9168  2muline0  9282  elznn0  9407  ser0  10700  0exp0e1  10711  expeq0  10737  0exp  10741  sq0  10797  bcval5  10930  shftval3  11213  shftidt2  11218  cjap0  11293  cjne0  11294  abs0  11444  abs2dif  11492  clim0  11671  climz  11678  serclim0  11691  sumrbdclem  11763  fsum3cvg  11764  summodclem3  11766  summodclem2a  11767  fisumss  11778  fsumrelem  11857  ef0  12058  eftlub  12076  sin0  12115  tan0  12117  4sqlem11  12799  cncrng  14406  cnfld0  14408  cnbl0  15081  cnblcld  15082  dvconst  15241  dvconstre  15243  dvconstss  15245  dvcnp2cntop  15246  dvrecap  15260  dveflem  15273  plyun0  15283  plycjlemc  15307  plycj  15308  dvply2g  15313  sinhalfpilem  15338  sin2kpi  15358  cos2kpi  15359  sinkpi  15394  1sgm2ppw  15542  dcapnconst  16141