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

Theorem recnd 7801
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 7760 . 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 1480   CCcc 7625   RRcr 7626
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-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-resscn 7719
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  readdcan  7909  ltadd2  8188  ltadd1  8198  leadd2  8200  ltsubadd  8201  ltsubadd2  8202  lesubadd  8203  lesubadd2  8204  ltaddsub  8205  leaddsub  8207  lesub1  8225  lesub2  8226  ltsub1  8227  ltsub2  8228  ltnegcon1  8232  ltnegcon2  8233  add20  8243  subge0  8244  suble0  8245  lesub0  8248  eqord2  8253  possumd  8338  sublt0d  8339  rimul  8354  rereim  8355  apreap  8356  ltmul1a  8360  ltmul1  8361  reapmul1  8364  remulext2  8369  cru  8371  apreim  8372  mulreim  8373  apadd1  8377  apneg  8380  mulext1  8381  ltapd  8407  aprcl  8415  rerecclap  8497  redivclap  8498  recgt0  8615  prodgt0gt0  8616  prodgt0  8617  prodge0  8619  lemul1a  8623  ltdiv1  8633  ltmuldiv  8639  ledivmul  8642  lt2mul2div  8644  ltrec  8648  lt2msq  8651  ltdiv2  8652  ltrec1  8653  lerec2  8654  ledivdiv  8655  lediv2  8656  ltdiv23  8657  lediv23  8658  lediv12a  8659  recp1lt1  8664  recreclt  8665  ledivp1  8668  mulle0r  8709  negiso  8720  avglt1  8965  avglt2  8966  div4p1lem1div2  8980  nn0cnd  9039  zcn  9066  peano2z  9097  zaddcllemneg  9100  ztri3or  9104  zeo  9163  zcnd  9181  eluzelcn  9344  infrenegsupex  9396  supinfneg  9397  infsupneg  9398  supminfex  9399  cnref1o  9447  rpcn  9457  rpcnd  9492  ltaddrp2d  9525  mul2lt0rlt0  9553  mul2lt0rgt0  9554  mul2lt0llt0  9555  mul2lt0lgt0  9556  mul2lt0np  9557  mul2lt0pn  9558  xpncan  9661  icoshftf1o  9781  lincmb01cmp  9793  iccf1o  9794  qbtwnrelemcalc  10040  flhalf  10082  intfracq  10100  flqdiv  10101  modqid  10129  modqid0  10130  mulqaddmodid  10144  ser3le  10298  expcl2lemap  10312  expnegzap  10334  expaddzaplem  10343  expaddzap  10344  expmulzap  10346  ltexp2a  10352  leexp2a  10353  leexp2r  10354  exple1  10356  expubnd  10357  sq11  10372  bernneq2  10420  expnbnd  10422  nn0opthlem2d  10474  faclbnd  10494  bcp1nk  10515  remim  10639  reim0b  10641  rereb  10642  mulreap  10643  cjreb  10645  recj  10646  reneg  10647  readd  10648  resub  10649  remullem  10650  remul2  10652  redivap  10653  imcj  10654  imneg  10655  imadd  10656  imsub  10657  immul2  10659  imdivap  10660  cjcj  10662  cjadd  10663  ipcnval  10665  cjmulval  10667  cjneg  10669  imval2  10673  cjreim2  10683  cjap  10685  cnrecnv  10689  caucvgrelemrec  10758  cvg1nlemres  10764  recvguniqlem  10773  recvguniq  10774  resqrexlemover  10789  resqrexlemcalc1  10793  resqrexlemcalc2  10794  resqrexlemcalc3  10795  resqrexlemnmsq  10796  resqrexlemnm  10797  resqrexlemgt0  10799  resqrexlemoverl  10800  resqrexlemglsq  10801  remsqsqrt  10811  sqrtmul  10814  sqrtdiv  10821  sqrtmsq  10824  abs00ap  10841  absext  10842  abs00  10843  absdivap  10849  absid  10850  absexp  10858  absexpzap  10859  absimle  10863  abslt  10867  absle  10868  abssubap0  10869  abssubne0  10870  releabs  10875  recvalap  10876  abstri  10883  abs2difabs  10887  amgm2  10897  icodiamlt  10959  maxabsle  10983  maxabslemab  10985  maxabslemlub  10986  maxabslemval  10987  maxcl  10989  maxltsup  10997  max0addsup  10998  minmax  11008  minabs  11014  minclpr  11015  bdtrilem  11017  bdtri  11018  mul0inf  11019  climabs0  11083  reccn2ap  11089  climrecl  11100  climge0  11101  climle  11110  climsqz  11111  climsqz2  11112  climlec2  11117  climrecvg1n  11124  climcvg1nlem  11125  isumrecl  11205  isumge0  11206  fsumlessfi  11236  fsumge1  11237  fsum00  11238  fsumle  11239  fsumlt  11240  fsumabs  11241  iserabs  11251  isumrpcl  11270  isumle  11271  isumlessdc  11272  trireciplem  11276  trirecip  11277  expcnvre  11279  expcnv  11280  explecnv  11281  absltap  11285  geo2sum  11290  cvgratnnlembern  11299  cvgratnnlemnexp  11300  cvgratnnlemmn  11301  cvgratnnlemabsle  11303  cvgratnnlemsumlt  11304  cvgratnnlemfm  11305  cvgratnnlemrate  11306  cvgratz  11308  mertenslemi1  11311  mertenslem2  11312  efcllemp  11371  ege2le3  11384  efaddlem  11387  efgt0  11397  reeftlcl  11402  eftlub  11403  effsumlt  11405  efltim  11411  eflegeo  11415  resin4p  11432  recos4p  11433  efeul  11448  ef01bndlem  11470  sin01bnd  11471  cos01bnd  11472  sin01gt0  11475  cos01gt0  11476  sin02gt0  11477  cos12dec  11481  absefi  11482  absef  11483  absefib  11484  efieq1re  11485  eirraplem  11490  dvdslelemd  11548  odd2np1  11577  divalglemnqt  11624  infssuzcldc  11651  nn0seqcvgd  11729  sqnprm  11823  metrtri  12556  bl2in  12582  blhalf  12587  blssps  12606  blss  12607  dedekindeu  12780  dedekindicclemicc  12789  ivthinclemlopn  12793  ivthinclemuopn  12795  ivthinc  12800  ivthdec  12801  dvcjbr  12851  dvfre  12853  dveflem  12865  sin0pilem1  12872  sin0pilem2  12873  pilem3  12874  sincosq2sgn  12918  sincosq3sgn  12919  sincosq4sgn  12920  sinq12gt0  12921  sinq34lt0t  12922  cosq14gt0  12923  cosq23lt0  12924  coseq0q4123  12925  coseq0negpitopi  12927  tanrpcl  12928  tangtx  12929  coskpi  12939  cosordlem  12940  cosq34lt1  12941  cos11  12944  qdencn  13236  refeq  13237  cvgcmp2nlemabs  13241  cvgcmp2n  13242  trilpolemisumle  13245  trilpolemeq1  13247  trilpolemlt1  13248
  Copyright terms: Public domain W3C validator