Theorem recnd 7794

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

Step	Hyp	Ref	Expression
1		recnd.1	. 2 |- ( ph -> A e. RR )
2		recn 7753	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 14	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 1480   CCcc 7618   RRcr 7619

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 7712

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  7902  ltadd2  8181  ltadd1  8191  leadd2  8193  ltsubadd  8194  ltsubadd2  8195  lesubadd  8196  lesubadd2  8197  ltaddsub  8198  leaddsub  8200  lesub1  8218  lesub2  8219  ltsub1  8220  ltsub2  8221  ltnegcon1  8225  ltnegcon2  8226  add20  8236  subge0  8237  suble0  8238  lesub0  8241  eqord2  8246  possumd  8331  sublt0d  8332  rimul  8347  rereim  8348  apreap  8349  ltmul1a  8353  ltmul1  8354  reapmul1  8357  remulext2  8362  cru  8364  apreim  8365  mulreim  8366  apadd1  8370  apneg  8373  mulext1  8374  ltapd  8400  aprcl  8408  rerecclap  8490  redivclap  8491  recgt0  8608  prodgt0gt0  8609  prodgt0  8610  prodge0  8612  lemul1a  8616  ltdiv1  8626  ltmuldiv  8632  ledivmul  8635  lt2mul2div  8637  ltrec  8641  lt2msq  8644  ltdiv2  8645  ltrec1  8646  lerec2  8647  ledivdiv  8648  lediv2  8649  ltdiv23  8650  lediv23  8651  lediv12a  8652  recp1lt1  8657  recreclt  8658  ledivp1  8661  mulle0r  8702  negiso  8713  avglt1  8958  avglt2  8959  div4p1lem1div2  8973  nn0cnd  9032  zcn  9059  peano2z  9090  zaddcllemneg  9093  ztri3or  9097  zeo  9156  zcnd  9174  eluzelcn  9337  infrenegsupex  9389  supinfneg  9390  infsupneg  9391  supminfex  9392  cnref1o  9440  rpcn  9450  rpcnd  9485  ltaddrp2d  9518  mul2lt0rlt0  9546  mul2lt0rgt0  9547  mul2lt0llt0  9548  mul2lt0lgt0  9549  mul2lt0np  9550  mul2lt0pn  9551  xpncan  9654  icoshftf1o  9774  lincmb01cmp  9786  iccf1o  9787  qbtwnrelemcalc  10033  flhalf  10075  intfracq  10093  flqdiv  10094  modqid  10122  modqid0  10123  mulqaddmodid  10137  ser3le  10291  expcl2lemap  10305  expnegzap  10327  expaddzaplem  10336  expaddzap  10337  expmulzap  10339  ltexp2a  10345  leexp2a  10346  leexp2r  10347  exple1  10349  expubnd  10350  sq11  10365  bernneq2  10413  expnbnd  10415  nn0opthlem2d  10467  faclbnd  10487  bcp1nk  10508  remim  10632  reim0b  10634  rereb  10635  mulreap  10636  cjreb  10638  recj  10639  reneg  10640  readd  10641  resub  10642  remullem  10643  remul2  10645  redivap  10646  imcj  10647  imneg  10648  imadd  10649  imsub  10650  immul2  10652  imdivap  10653  cjcj  10655  cjadd  10656  ipcnval  10658  cjmulval  10660  cjneg  10662  imval2  10666  cjreim2  10676  cjap  10678  cnrecnv  10682  caucvgrelemrec  10751  cvg1nlemres  10757  recvguniqlem  10766  recvguniq  10767  resqrexlemover  10782  resqrexlemcalc1  10786  resqrexlemcalc2  10787  resqrexlemcalc3  10788  resqrexlemnmsq  10789  resqrexlemnm  10790  resqrexlemgt0  10792  resqrexlemoverl  10793  resqrexlemglsq  10794  remsqsqrt  10804  sqrtmul  10807  sqrtdiv  10814  sqrtmsq  10817  abs00ap  10834  absext  10835  abs00  10836  absdivap  10842  absid  10843  absexp  10851  absexpzap  10852  absimle  10856  abslt  10860  absle  10861  abssubap0  10862  abssubne0  10863  releabs  10868  recvalap  10869  abstri  10876  abs2difabs  10880  amgm2  10890  icodiamlt  10952  maxabsle  10976  maxabslemab  10978  maxabslemlub  10979  maxabslemval  10980  maxcl  10982  maxltsup  10990  max0addsup  10991  minmax  11001  minabs  11007  minclpr  11008  bdtrilem  11010  bdtri  11011  mul0inf  11012  climabs0  11076  reccn2ap  11082  climrecl  11093  climge0  11094  climle  11103  climsqz  11104  climsqz2  11105  climlec2  11110  climrecvg1n  11117  climcvg1nlem  11118  isumrecl  11198  isumge0  11199  fsumlessfi  11229  fsumge1  11230  fsum00  11231  fsumle  11232  fsumlt  11233  fsumabs  11234  iserabs  11244  isumrpcl  11263  isumle  11264  isumlessdc  11265  trireciplem  11269  trirecip  11270  expcnvre  11272  expcnv  11273  explecnv  11274  absltap  11278  geo2sum  11283  cvgratnnlembern  11292  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratnnlemabsle  11296  cvgratnnlemsumlt  11297  cvgratnnlemfm  11298  cvgratnnlemrate  11299  cvgratz  11301  mertenslemi1  11304  mertenslem2  11305  efcllemp  11364  ege2le3  11377  efaddlem  11380  efgt0  11390  reeftlcl  11395  eftlub  11396  effsumlt  11398  efltim  11404  eflegeo  11408  resin4p  11425  recos4p  11426  efeul  11441  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  cos12dec  11474  absefi  11475  absef  11476  absefib  11477  efieq1re  11478  eirraplem  11483  dvdslelemd  11541  odd2np1  11570  divalglemnqt  11617  infssuzcldc  11644  nn0seqcvgd  11722  sqnprm  11816  metrtri  12546  bl2in  12572  blhalf  12577  blssps  12596  blss  12597  dedekindeu  12770  dedekindicclemicc  12779  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthinc  12790  ivthdec  12791  dvcjbr  12841  dvfre  12843  dveflem  12855  sin0pilem1  12862  sin0pilem2  12863  pilem3  12864  sincosq2sgn  12908  sincosq3sgn  12909  sincosq4sgn  12910  sinq12gt0  12911  sinq34lt0t  12912  cosq14gt0  12913  cosq23lt0  12914  coseq0q4123  12915  coseq0negpitopi  12917  tanrpcl  12918  tangtx  12919  coskpi  12929  cosordlem  12930  cosq34lt1  12931  qdencn  13222  refeq  13223  cvgcmp2nlemabs  13227  cvgcmp2n  13228  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234