ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0cn GIF version

Theorem 0cn 7765
Description: 0 is a complex number. (Contributed by NM, 19-Feb-2005.)
Assertion
Ref Expression
0cn 0 ∈ ℂ

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 7732 . 2 ((i · i) + 1) = 0
2 ax-icn 7722 . . . 4 i ∈ ℂ
3 mulcl 7754 . . . 4 ((i ∈ ℂ ∧ i ∈ ℂ) → (i · i) ∈ ℂ)
42, 2, 3mp2an 422 . . 3 (i · i) ∈ ℂ
5 ax-1cn 7720 . . 3 1 ∈ ℂ
6 addcl 7752 . . 3 (((i · i) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · i) + 1) ∈ ℂ)
74, 5, 6mp2an 422 . 2 ((i · i) + 1) ∈ ℂ
81, 7eqeltrri 2213 1 0 ∈ ℂ
Colors of variables: wff set class
Syntax hints:  wcel 1480  (class class class)co 5774  cc 7625  0cc0 7627  1c1 7628  ici 7629   + caddc 7630   · cmul 7632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7720  ax-icn 7722  ax-addcl 7723  ax-mulcl 7725  ax-i2m1 7732
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  0cnd  7766  c0ex  7767  addid2  7908  00id  7910  cnegexlem2  7945  negcl  7969  subid  7988  subid1  7989  neg0  8015  negid  8016  negsub  8017  subneg  8018  negneg  8019  negeq0  8023  negsubdi  8025  renegcl  8030  mul02  8156  mul01  8158  mulneg1  8164  ixi  8352  negap0  8399  muleqadd  8436  divvalap  8441  div0ap  8469  recgt0  8615  0m0e0  8839  2muline0  8952  elznn0  9076  ser0  10294  0exp0e1  10305  expeq0  10331  0exp  10335  sq0  10390  bcval5  10516  shftval3  10606  shftidt2  10611  cjap0  10686  cjne0  10687  abs0  10837  abs2dif  10885  clim0  11061  climz  11068  serclim0  11081  sumrbdclem  11153  fsum3cvg  11154  summodclem3  11156  summodclem2a  11157  fisumss  11168  fsumrelem  11247  ef0  11385  eftlub  11403  sin0  11442  tan0  11444  cnbl0  12712  cnblcld  12713  dvconst  12839  dvcnp2cntop  12841  dvrecap  12855  dveflem  12864  sinhalfpilem  12888  sin2kpi  12908  cos2kpi  12909  sinkpi  12944
  Copyright terms: Public domain W3C validator