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

Theorem recnd 7495
Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
recnd.1  |-  ( ph  ->  A  e.  RR )
Assertion
Ref Expression
recnd  |-  ( ph  ->  A  e.  CC )

Proof of Theorem recnd
StepHypRef Expression
1 recnd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 recn 7454 . 2  |-  ( A  e.  RR  ->  A  e.  CC )
31, 2syl 14 1  |-  ( ph  ->  A  e.  CC )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   CCcc 7327   RRcr 7328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-resscn 7416
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3003  df-ss 3010
This theorem is referenced by:  readdcan  7601  ltadd2  7876  ltadd1  7886  leadd2  7888  ltsubadd  7889  ltsubadd2  7890  lesubadd  7891  lesubadd2  7892  ltaddsub  7893  leaddsub  7895  lesub1  7913  lesub2  7914  ltsub1  7915  ltsub2  7916  ltnegcon1  7920  ltnegcon2  7921  add20  7931  subge0  7932  suble0  7933  lesub0  7936  possumd  8022  sublt0d  8023  rimul  8038  rereim  8039  apreap  8040  ltmul1a  8044  ltmul1  8045  reapmul1  8048  remulext2  8053  cru  8055  apreim  8056  mulreim  8057  apadd1  8061  apneg  8064  mulext1  8065  ltapd  8089  rerecclap  8171  redivclap  8172  recgt0  8283  prodgt0gt0  8284  prodgt0  8285  prodge0  8287  lemul1a  8291  ltdiv1  8301  ltmuldiv  8307  ledivmul  8310  lt2mul2div  8312  ltrec  8316  lt2msq  8319  ltdiv2  8320  ltrec1  8321  lerec2  8322  ledivdiv  8323  lediv2  8324  ltdiv23  8325  lediv23  8326  lediv12a  8327  recp1lt1  8332  recreclt  8333  ledivp1  8336  mulle0r  8377  negiso  8388  avglt1  8624  avglt2  8625  div4p1lem1div2  8639  nn0cnd  8698  zcn  8725  peano2z  8756  zaddcllemneg  8759  ztri3or  8763  zeo  8821  zcnd  8839  eluzelcn  8999  infrenegsupex  9051  supinfneg  9052  infsupneg  9053  supminfex  9054  cnref1o  9102  rpcn  9111  rpcnd  9144  ltaddrp2d  9177  icoshftf1o  9377  lincmb01cmp  9389  iccf1o  9390  qbtwnrelemcalc  9632  flhalf  9674  intfracq  9692  flqdiv  9693  modqid  9721  modqid0  9722  mulqaddmodid  9736  ser3le  9918  expcl2lemap  9932  expnegzap  9954  expaddzaplem  9963  expaddzap  9964  expmulzap  9966  ltexp2a  9972  leexp2a  9973  leexp2r  9974  exple1  9976  expubnd  9977  sq11  9992  bernneq2  10040  expnbnd  10042  nn0opthlem2d  10094  faclbnd  10114  bcp1nk  10135  remim  10259  reim0b  10261  rereb  10262  mulreap  10263  cjreb  10265  recj  10266  reneg  10267  readd  10268  resub  10269  remullem  10270  remul2  10272  redivap  10273  imcj  10274  imneg  10275  imadd  10276  imsub  10277  immul2  10279  imdivap  10280  cjcj  10282  cjadd  10283  ipcnval  10285  cjmulval  10287  cjneg  10289  imval2  10293  cjreim2  10303  cjap  10305  cnrecnv  10309  caucvgrelemrec  10377  cvg1nlemres  10383  recvguniqlem  10392  recvguniq  10393  resqrexlemover  10408  resqrexlemcalc1  10412  resqrexlemcalc2  10413  resqrexlemcalc3  10414  resqrexlemnmsq  10415  resqrexlemnm  10416  resqrexlemgt0  10418  resqrexlemoverl  10419  resqrexlemglsq  10420  remsqsqrt  10430  sqrtmul  10433  sqrtdiv  10440  sqrtmsq  10443  abs00ap  10460  absext  10461  abs00  10462  absdivap  10468  absid  10469  absexp  10477  absexpzap  10478  absimle  10482  abslt  10486  absle  10487  abssubap0  10488  abssubne0  10489  releabs  10494  recvalap  10495  abstri  10502  abs2difabs  10506  amgm2  10516  icodiamlt  10578  maxabsle  10602  maxabslemab  10604  maxabslemlub  10605  maxabslemval  10606  maxcl  10608  maxltsup  10616  max0addsup  10617  minmax  10625  climabs0  10660  climrecl  10676  climge0  10677  climle  10686  climsqz  10687  climsqz2  10688  climlec2  10694  climrecvg1n  10701  climcvg1nlem  10702  isumrecl  10786  isumge0  10787  fsumlessfi  10817  fsumge1  10818  fsum00  10819  fsumle  10820  fsumlt  10821  fsumabs  10822  isumrpcl  10850  isumle  10851  trireciplem  10855  trirecip  10856  expcnvre  10858  expcnv  10859  explecnv  10860  absltap  10864  geo2sum  10869  dvdslelemd  10926  odd2np1  10955  divalglemnqt  11002  infssuzcldc  11029  nn0seqcvgd  11105  sqnprm  11199  qdencn  11561
  Copyright terms: Public domain W3C validator