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

Theorem 0cn 7770
Description: 0 is a complex number. (Contributed by NM, 19-Feb-2005.)
Assertion
Ref Expression
0cn  |-  0  e.  CC

Proof of Theorem 0cn
StepHypRef Expression
1 ax-i2m1 7737 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 7727 . . . 4  |-  _i  e.  CC
3 mulcl 7759 . . . 4  |-  ( ( _i  e.  CC  /\  _i  e.  CC )  -> 
( _i  x.  _i )  e.  CC )
42, 2, 3mp2an 422 . . 3  |-  ( _i  x.  _i )  e.  CC
5 ax-1cn 7725 . . 3  |-  1  e.  CC
6 addcl 7757 . . 3  |-  ( ( ( _i  x.  _i )  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  _i )  +  1 )  e.  CC )
74, 5, 6mp2an 422 . 2  |-  ( ( _i  x.  _i )  +  1 )  e.  CC
81, 7eqeltrri 2213 1  |-  0  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1480  (class class class)co 5774   CCcc 7630   0cc0 7632   1c1 7633   _ici 7634    + caddc 7635    x. cmul 7637
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 7725  ax-icn 7727  ax-addcl 7728  ax-mulcl 7730  ax-i2m1 7737
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  0cnd  7771  c0ex  7772  addid2  7913  00id  7915  cnegexlem2  7950  negcl  7974  subid  7993  subid1  7994  neg0  8020  negid  8021  negsub  8022  subneg  8023  negneg  8024  negeq0  8028  negsubdi  8030  renegcl  8035  mul02  8161  mul01  8163  mulneg1  8169  ixi  8357  negap0  8404  muleqadd  8441  divvalap  8446  div0ap  8474  recgt0  8620  0m0e0  8844  2muline0  8957  elznn0  9081  ser0  10299  0exp0e1  10310  expeq0  10336  0exp  10340  sq0  10395  bcval5  10521  shftval3  10611  shftidt2  10616  cjap0  10691  cjne0  10692  abs0  10842  abs2dif  10890  clim0  11066  climz  11073  serclim0  11086  sumrbdclem  11158  fsum3cvg  11159  summodclem3  11161  summodclem2a  11162  fisumss  11173  fsumrelem  11252  ef0  11390  eftlub  11408  sin0  11447  tan0  11449  cnbl0  12717  cnblcld  12718  dvconst  12844  dvcnp2cntop  12846  dvrecap  12860  dveflem  12870  sinhalfpilem  12894  sin2kpi  12914  cos2kpi  12915  sinkpi  12950
  Copyright terms: Public domain W3C validator