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

Theorem 0cn 7077
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 7047 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 7037 . . . 4  |-  _i  e.  CC
3 mulcl 7066 . . . 4  |-  ( ( _i  e.  CC  /\  _i  e.  CC )  -> 
( _i  x.  _i )  e.  CC )
42, 2, 3mp2an 410 . . 3  |-  ( _i  x.  _i )  e.  CC
5 ax-1cn 7035 . . 3  |-  1  e.  CC
6 addcl 7064 . . 3  |-  ( ( ( _i  x.  _i )  e.  CC  /\  1  e.  CC )  ->  (
( _i  x.  _i )  +  1 )  e.  CC )
74, 5, 6mp2an 410 . 2  |-  ( ( _i  x.  _i )  +  1 )  e.  CC
81, 7eqeltrri 2127 1  |-  0  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1409  (class class class)co 5540   CCcc 6945   0cc0 6947   1c1 6948   _ici 6949    + caddc 6950    x. cmul 6952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038  ax-1cn 7035  ax-icn 7037  ax-addcl 7038  ax-mulcl 7040  ax-i2m1 7047
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  0cnd  7078  c0ex  7079  addid2  7213  00id  7215  cnegexlem2  7250  negcl  7274  subid  7293  subid1  7294  neg0  7320  negid  7321  negsub  7322  subneg  7323  negneg  7324  negeq0  7328  negsubdi  7330  renegcl  7335  mul02  7456  mul01  7458  mulneg1  7464  ixi  7648  negap0  7694  muleqadd  7723  divvalap  7727  div0ap  7753  recgt0  7891  0m0e0  8102  2muline0  8207  elznn0  8317  iser0  9415  0exp0e1  9425  expeq0  9451  0exp  9455  sq0  9510  ibcval5  9631  shftval3  9656  shftidt2  9661  cjap0  9735  cjne0  9736  abs0  9885  abs00  9891  abs2dif  9933  clim0  10037  climz  10044  iserclim0  10057
  Copyright terms: Public domain W3C validator