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

Theorem 0cn 7927
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 7894 . 2  |-  ( ( _i  x.  _i )  +  1 )  =  0
2 ax-icn 7884 . . . 4  |-  _i  e.  CC
3 mulcl 7916 . . . 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 7882 . . 3  |-  1  e.  CC
6 addcl 7914 . . 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 2251 1  |-  0  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 2148  (class class class)co 5868   CCcc 7787   0cc0 7789   1c1 7790   _ici 7791    + caddc 7792    x. cmul 7794
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159  ax-1cn 7882  ax-icn 7884  ax-addcl 7885  ax-mulcl 7887  ax-i2m1 7894
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173
This theorem is referenced by:  0cnd  7928  c0ex  7929  addid2  8073  00id  8075  cnegexlem2  8110  negcl  8134  subid  8153  subid1  8154  neg0  8180  negid  8181  negsub  8182  subneg  8183  negneg  8184  negeq0  8188  negsubdi  8190  renegcl  8195  mul02  8321  mul01  8323  mulneg1  8329  ixi  8517  negap0  8564  muleqadd  8601  divvalap  8607  div0ap  8635  recgt0  8783  0m0e0  9007  2muline0  9120  elznn0  9244  ser0  10487  0exp0e1  10498  expeq0  10524  0exp  10528  sq0  10583  bcval5  10714  shftval3  10807  shftidt2  10812  cjap0  10887  cjne0  10888  abs0  11038  abs2dif  11086  clim0  11264  climz  11271  serclim0  11284  sumrbdclem  11356  fsum3cvg  11357  summodclem3  11359  summodclem2a  11360  fisumss  11371  fsumrelem  11450  ef0  11651  eftlub  11669  sin0  11708  tan0  11710  cnbl0  13667  cnblcld  13668  dvconst  13794  dvcnp2cntop  13796  dvrecap  13810  dveflem  13820  sinhalfpilem  13845  sin2kpi  13865  cos2kpi  13866  sinkpi  13901  dcapnconst  14431
  Copyright terms: Public domain W3C validator