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

Theorem 0cn 7979
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 7946 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 7936 . . . 4  |-  _i  e.  CC
3 mulcl 7968 . . . 4  |-  ( ( _i  e.  CC  /\  _i  e.  CC )  -> 
( _i  x.  _i )  e.  CC )
42, 2, 3mp2an 426 . . 3  |-  ( _i  x.  _i )  e.  CC
5 ax-1cn 7934 . . 3  |-  1  e.  CC
6 addcl 7966 . . 3  |-  ( ( ( _i  x.  _i )  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  _i )  +  1 )  e.  CC )
74, 5, 6mp2an 426 . 2  |-  ( ( _i  x.  _i )  +  1 )  e.  CC
81, 7eqeltrri 2263 1  |-  0  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 2160  (class class class)co 5896   CCcc 7839   0cc0 7841   1c1 7842   _ici 7843    + caddc 7844    x. cmul 7846
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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2171  ax-1cn 7934  ax-icn 7936  ax-addcl 7937  ax-mulcl 7939  ax-i2m1 7946
This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-clel 2185
This theorem is referenced by:  0cnd  7980  c0ex  7981  addlid  8126  00id  8128  cnegexlem2  8163  negcl  8187  subid  8206  subid1  8207  neg0  8233  negid  8234  negsub  8235  subneg  8236  negneg  8237  negeq0  8241  negsubdi  8243  renegcl  8248  mul02  8374  mul01  8376  mulneg1  8382  ixi  8570  negap0  8617  muleqadd  8655  divvalap  8661  div0ap  8689  recgt0  8837  0m0e0  9061  2muline0  9174  elznn0  9298  ser0  10545  0exp0e1  10556  expeq0  10582  0exp  10586  sq0  10642  bcval5  10775  shftval3  10868  shftidt2  10873  cjap0  10948  cjne0  10949  abs0  11099  abs2dif  11147  clim0  11325  climz  11332  serclim0  11345  sumrbdclem  11417  fsum3cvg  11418  summodclem3  11420  summodclem2a  11421  fisumss  11432  fsumrelem  11511  ef0  11712  eftlub  11730  sin0  11769  tan0  11771  4sqlem11  12433  cncrng  13872  cnfld0  13874  cnbl0  14491  cnblcld  14492  dvconst  14618  dvcnp2cntop  14620  dvrecap  14634  dveflem  14644  sinhalfpilem  14669  sin2kpi  14689  cos2kpi  14690  sinkpi  14725  dcapnconst  15268
  Copyright terms: Public domain W3C validator