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

Theorem recnd 7762
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 7721 . 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 1465   CCcc 7586   RRcr 7587
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-resscn 7680
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  readdcan  7870  ltadd2  8149  ltadd1  8159  leadd2  8161  ltsubadd  8162  ltsubadd2  8163  lesubadd  8164  lesubadd2  8165  ltaddsub  8166  leaddsub  8168  lesub1  8186  lesub2  8187  ltsub1  8188  ltsub2  8189  ltnegcon1  8193  ltnegcon2  8194  add20  8204  subge0  8205  suble0  8206  lesub0  8209  eqord2  8214  possumd  8298  sublt0d  8299  rimul  8314  rereim  8315  apreap  8316  ltmul1a  8320  ltmul1  8321  reapmul1  8324  remulext2  8329  cru  8331  apreim  8332  mulreim  8333  apadd1  8337  apneg  8340  mulext1  8341  ltapd  8367  aprcl  8375  rerecclap  8457  redivclap  8458  recgt0  8572  prodgt0gt0  8573  prodgt0  8574  prodge0  8576  lemul1a  8580  ltdiv1  8590  ltmuldiv  8596  ledivmul  8599  lt2mul2div  8601  ltrec  8605  lt2msq  8608  ltdiv2  8609  ltrec1  8610  lerec2  8611  ledivdiv  8612  lediv2  8613  ltdiv23  8614  lediv23  8615  lediv12a  8616  recp1lt1  8621  recreclt  8622  ledivp1  8625  mulle0r  8666  negiso  8677  avglt1  8916  avglt2  8917  div4p1lem1div2  8931  nn0cnd  8990  zcn  9017  peano2z  9048  zaddcllemneg  9051  ztri3or  9055  zeo  9114  zcnd  9132  eluzelcn  9293  infrenegsupex  9345  supinfneg  9346  infsupneg  9347  supminfex  9348  cnref1o  9396  rpcn  9405  rpcnd  9440  ltaddrp2d  9473  mul2lt0rlt0  9501  mul2lt0rgt0  9502  mul2lt0llt0  9503  mul2lt0lgt0  9504  mul2lt0np  9505  mul2lt0pn  9506  xpncan  9609  icoshftf1o  9729  lincmb01cmp  9741  iccf1o  9742  qbtwnrelemcalc  9988  flhalf  10030  intfracq  10048  flqdiv  10049  modqid  10077  modqid0  10078  mulqaddmodid  10092  ser3le  10246  expcl2lemap  10260  expnegzap  10282  expaddzaplem  10291  expaddzap  10292  expmulzap  10294  ltexp2a  10300  leexp2a  10301  leexp2r  10302  exple1  10304  expubnd  10305  sq11  10320  bernneq2  10368  expnbnd  10370  nn0opthlem2d  10422  faclbnd  10442  bcp1nk  10463  remim  10587  reim0b  10589  rereb  10590  mulreap  10591  cjreb  10593  recj  10594  reneg  10595  readd  10596  resub  10597  remullem  10598  remul2  10600  redivap  10601  imcj  10602  imneg  10603  imadd  10604  imsub  10605  immul2  10607  imdivap  10608  cjcj  10610  cjadd  10611  ipcnval  10613  cjmulval  10615  cjneg  10617  imval2  10621  cjreim2  10631  cjap  10633  cnrecnv  10637  caucvgrelemrec  10706  cvg1nlemres  10712  recvguniqlem  10721  recvguniq  10722  resqrexlemover  10737  resqrexlemcalc1  10741  resqrexlemcalc2  10742  resqrexlemcalc3  10743  resqrexlemnmsq  10744  resqrexlemnm  10745  resqrexlemgt0  10747  resqrexlemoverl  10748  resqrexlemglsq  10749  remsqsqrt  10759  sqrtmul  10762  sqrtdiv  10769  sqrtmsq  10772  abs00ap  10789  absext  10790  abs00  10791  absdivap  10797  absid  10798  absexp  10806  absexpzap  10807  absimle  10811  abslt  10815  absle  10816  abssubap0  10817  abssubne0  10818  releabs  10823  recvalap  10824  abstri  10831  abs2difabs  10835  amgm2  10845  icodiamlt  10907  maxabsle  10931  maxabslemab  10933  maxabslemlub  10934  maxabslemval  10935  maxcl  10937  maxltsup  10945  max0addsup  10946  minmax  10956  minabs  10962  minclpr  10963  bdtrilem  10965  bdtri  10966  mul0inf  10967  climabs0  11031  reccn2ap  11037  climrecl  11048  climge0  11049  climle  11058  climsqz  11059  climsqz2  11060  climlec2  11065  climrecvg1n  11072  climcvg1nlem  11073  isumrecl  11153  isumge0  11154  fsumlessfi  11184  fsumge1  11185  fsum00  11186  fsumle  11187  fsumlt  11188  fsumabs  11189  iserabs  11199  isumrpcl  11218  isumle  11219  isumlessdc  11220  trireciplem  11224  trirecip  11225  expcnvre  11227  expcnv  11228  explecnv  11229  absltap  11233  geo2sum  11238  cvgratnnlembern  11247  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratnnlemabsle  11251  cvgratnnlemsumlt  11252  cvgratnnlemfm  11253  cvgratnnlemrate  11254  cvgratz  11256  mertenslemi1  11259  mertenslem2  11260  efcllemp  11278  ege2le3  11291  efaddlem  11294  efgt0  11304  reeftlcl  11309  eftlub  11310  effsumlt  11312  efltim  11318  eflegeo  11322  resin4p  11339  recos4p  11340  efeul  11355  ef01bndlem  11377  sin01bnd  11378  cos01bnd  11379  sin01gt0  11382  cos01gt0  11383  sin02gt0  11384  cos12dec  11388  absefi  11389  absef  11390  absefib  11391  efieq1re  11392  eirraplem  11395  dvdslelemd  11453  odd2np1  11482  divalglemnqt  11529  infssuzcldc  11556  nn0seqcvgd  11634  sqnprm  11728  metrtri  12457  bl2in  12483  blhalf  12488  blssps  12507  blss  12508  dedekindeu  12681  dedekindicclemicc  12690  ivthinclemlopn  12694  ivthinclemuopn  12696  ivthinc  12701  ivthdec  12702  dvcjbr  12752  dvfre  12754  dveflem  12766  sin0pilem1  12773  sin0pilem2  12774  pilem3  12775  sincosq2sgn  12819  sincosq3sgn  12820  sincosq4sgn  12821  sinq12gt0  12822  sinq34lt0t  12823  cosq14gt0  12824  cosq23lt0  12825  coseq0q4123  12826  coseq0negpitopi  12828  qdencn  13118  refeq  13119  cvgcmp2nlemabs  13123  cvgcmp2n  13124  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator