Theorem recnd 7923

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 7882	. 2 |- ( A e. RR -> A e. CC )
3	1, 2	syl 14	1 |- ( ph -> A e. CC )

Syntax hints:   -> wi 4   e. wcel 2136   CCcc 7747   RRcr 7748

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3121  df-ss 3128

This theorem is referenced by:  readdcan  8034  ltadd2  8313  ltadd1  8323  leadd2  8325  ltsubadd  8326  ltsubadd2  8327  lesubadd  8328  lesubadd2  8329  ltaddsub  8330  leaddsub  8332  lesub1  8350  lesub2  8351  ltsub1  8352  ltsub2  8353  ltnegcon1  8357  ltnegcon2  8358  add20  8368  subge0  8369  suble0  8370  lesub0  8373  eqord2  8378  possumd  8463  sublt0d  8464  rimul  8479  rereim  8480  apreap  8481  ltmul1a  8485  ltmul1  8486  reapmul1  8489  remulext2  8494  cru  8496  apreim  8497  mulreim  8498  apadd1  8502  apneg  8505  mulext1  8506  ltapd  8532  aprcl  8540  rerecclap  8622  redivclap  8623  recgt0  8741  prodgt0gt0  8742  prodgt0  8743  prodge0  8745  lemul1a  8749  ltdiv1  8759  ltmuldiv  8765  ledivmul  8768  lt2mul2div  8770  ltrec  8774  lt2msq  8777  ltdiv2  8778  ltrec1  8779  lerec2  8780  ledivdiv  8781  lediv2  8782  ltdiv23  8783  lediv23  8784  lediv12a  8785  recp1lt1  8790  recreclt  8791  ledivp1  8794  mulle0r  8835  negiso  8846  avglt1  9091  avglt2  9092  div4p1lem1div2  9106  nn0cnd  9165  zcn  9192  peano2z  9223  zaddcllemneg  9226  ztri3or  9230  zeo  9292  zcnd  9310  eluzelcn  9473  infrenegsupex  9528  supinfneg  9529  infsupneg  9530  supminfex  9531  cnref1o  9584  rpcn  9594  rpcnd  9630  ltaddrp2d  9663  mul2lt0rlt0  9691  mul2lt0rgt0  9692  mul2lt0llt0  9693  mul2lt0lgt0  9694  mul2lt0np  9695  mul2lt0pn  9696  xpncan  9803  icoshftf1o  9923  lincmb01cmp  9935  iccf1o  9936  qbtwnrelemcalc  10187  flhalf  10233  intfracq  10251  flqdiv  10252  modqid  10280  modqid0  10281  mulqaddmodid  10295  ser3le  10449  expcl2lemap  10463  expnegzap  10485  expaddzaplem  10494  expaddzap  10495  expmulzap  10497  ltexp2a  10503  leexp2a  10504  leexp2r  10505  exple1  10507  expubnd  10508  sq11  10523  bernneq2  10572  expnbnd  10574  nn0ltexp2  10619  nn0opthlem2d  10630  faclbnd  10650  bcp1nk  10671  remim  10798  reim0b  10800  rereb  10801  mulreap  10802  cjreb  10804  recj  10805  reneg  10806  readd  10807  resub  10808  remullem  10809  remul2  10811  redivap  10812  imcj  10813  imneg  10814  imadd  10815  imsub  10816  immul2  10818  imdivap  10819  cjcj  10821  cjadd  10822  ipcnval  10824  cjmulval  10826  cjneg  10828  imval2  10832  cjreim2  10842  cjap  10844  cnrecnv  10848  caucvgrelemrec  10917  cvg1nlemres  10923  recvguniqlem  10932  recvguniq  10933  resqrexlemover  10948  resqrexlemcalc1  10952  resqrexlemcalc2  10953  resqrexlemcalc3  10954  resqrexlemnmsq  10955  resqrexlemnm  10956  resqrexlemgt0  10958  resqrexlemoverl  10959  resqrexlemglsq  10960  remsqsqrt  10970  sqrtmul  10973  sqrtdiv  10980  sqrtmsq  10983  abs00ap  11000  absext  11001  abs00  11002  absdivap  11008  absid  11009  absexp  11017  absexpzap  11018  absimle  11022  abslt  11026  absle  11027  abssubap0  11028  abssubne0  11029  releabs  11034  recvalap  11035  abstri  11042  abs2difabs  11046  amgm2  11056  icodiamlt  11118  maxabsle  11142  maxabslemab  11144  maxabslemlub  11145  maxabslemval  11146  maxcl  11148  maxltsup  11156  max0addsup  11157  minmax  11167  minabs  11173  minclpr  11174  bdtrilem  11176  bdtri  11177  mul0inf  11178  mingeb  11179  climabs0  11244  reccn2ap  11250  climrecl  11261  climge0  11262  climle  11271  climsqz  11272  climsqz2  11273  climlec2  11278  climrecvg1n  11285  climcvg1nlem  11286  isumrecl  11366  isumge0  11367  fsumlessfi  11397  fsumge1  11398  fsum00  11399  fsumle  11400  fsumlt  11401  fsumabs  11402  iserabs  11412  isumrpcl  11431  isumle  11432  isumlessdc  11433  trireciplem  11437  trirecip  11438  expcnvre  11440  expcnv  11441  explecnv  11442  absltap  11446  geo2sum  11451  cvgratnnlembern  11460  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  cvgratnnlemabsle  11464  cvgratnnlemsumlt  11465  cvgratnnlemfm  11466  cvgratnnlemrate  11467  cvgratz  11469  mertenslemi1  11472  mertenslem2  11473  fprodabs  11553  fprodle  11577  efcllemp  11595  ege2le3  11608  efaddlem  11611  efgt0  11621  reeftlcl  11626  eftlub  11627  effsumlt  11629  efltim  11635  eflegeo  11638  resin4p  11655  recos4p  11656  efeul  11671  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  cos01gt0  11699  sin02gt0  11700  cos12dec  11704  absefi  11705  absef  11706  absefib  11707  efieq1re  11708  eirraplem  11713  dvdslelemd  11777  odd2np1  11806  divalglemnqt  11853  infssuzcldc  11880  nn0seqcvgd  11969  sqnprm  12064  isprm5lem  12069  odzdvds  12173  pythagtriplem14  12205  pcid  12251  fldivp1  12274  pockthlem  12282  4sqlem5  12308  4sqlem10  12313  mul4sqlem  12319  metrtri  12977  bl2in  13003  blhalf  13008  blssps  13027  blss  13028  dedekindeu  13201  dedekindicclemicc  13210  ivthinclemlopn  13214  ivthinclemuopn  13216  ivthinc  13221  ivthdec  13222  dvcjbr  13272  dvfre  13274  dveflem  13287  reeff1olem  13292  reeff1oleme  13293  eflt  13296  sin0pilem1  13302  sin0pilem2  13303  pilem3  13304  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  sinq34lt0t  13352  cosq14gt0  13353  cosq23lt0  13354  coseq0q4123  13355  coseq0negpitopi  13357  tanrpcl  13358  tangtx  13359  coskpi  13369  cosordlem  13370  cosq34lt1  13371  cos11  13374  reexplog  13392  relogexp  13393  logdivlti  13402  rpcxpef  13415  rpcncxpcl  13423  cxpap0  13425  rpcxpadd  13426  rpmulcxp  13430  cxpmul  13433  abscxp  13435  cxplt  13436  cxplt3  13440  logsqrt  13443  apcxp2  13458  rpabscxpbnd  13459  rplogbid1  13465  rplogb1  13466  rpelogb  13467  rplogbchbase  13468  rplogbreexp  13471  rprelogbmul  13473  rprelogbdiv  13475  rplogbcxp  13481  rpcxplogb  13482  logbgcd1irraplemexp  13486  logbgcd1irraplemap  13487  lgsvalmod  13520  lgsdilem  13528  lgsne0  13539  2sqlem1  13550  mul2sq  13552  2sqlem3  13553  2sqlem8  13559  qdencn  13866  refeq  13867  cvgcmp2nlemabs  13871  cvgcmp2n  13872  trilpolemisumle  13877  trilpolemeq1  13879  trilpolemlt1  13880  trirec0  13883  apdifflemf  13885  apdifflemr  13886  apdiff  13887  redc0  13896  reap0  13897  nconstwlpolem0  13901  nconstwlpolemgt0  13902