Theorem recnd 7818

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

Syntax hints:   -> wi 4   e. wcel 1481   CCcc 7642   RRcr 7643

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7736

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  readdcan  7926  ltadd2  8205  ltadd1  8215  leadd2  8217  ltsubadd  8218  ltsubadd2  8219  lesubadd  8220  lesubadd2  8221  ltaddsub  8222  leaddsub  8224  lesub1  8242  lesub2  8243  ltsub1  8244  ltsub2  8245  ltnegcon1  8249  ltnegcon2  8250  add20  8260  subge0  8261  suble0  8262  lesub0  8265  eqord2  8270  possumd  8355  sublt0d  8356  rimul  8371  rereim  8372  apreap  8373  ltmul1a  8377  ltmul1  8378  reapmul1  8381  remulext2  8386  cru  8388  apreim  8389  mulreim  8390  apadd1  8394  apneg  8397  mulext1  8398  ltapd  8424  aprcl  8432  rerecclap  8514  redivclap  8515  recgt0  8632  prodgt0gt0  8633  prodgt0  8634  prodge0  8636  lemul1a  8640  ltdiv1  8650  ltmuldiv  8656  ledivmul  8659  lt2mul2div  8661  ltrec  8665  lt2msq  8668  ltdiv2  8669  ltrec1  8670  lerec2  8671  ledivdiv  8672  lediv2  8673  ltdiv23  8674  lediv23  8675  lediv12a  8676  recp1lt1  8681  recreclt  8682  ledivp1  8685  mulle0r  8726  negiso  8737  avglt1  8982  avglt2  8983  div4p1lem1div2  8997  nn0cnd  9056  zcn  9083  peano2z  9114  zaddcllemneg  9117  ztri3or  9121  zeo  9180  zcnd  9198  eluzelcn  9361  infrenegsupex  9416  supinfneg  9417  infsupneg  9418  supminfex  9419  cnref1o  9469  rpcn  9479  rpcnd  9515  ltaddrp2d  9548  mul2lt0rlt0  9576  mul2lt0rgt0  9577  mul2lt0llt0  9578  mul2lt0lgt0  9579  mul2lt0np  9580  mul2lt0pn  9581  xpncan  9684  icoshftf1o  9804  lincmb01cmp  9816  iccf1o  9817  qbtwnrelemcalc  10064  flhalf  10106  intfracq  10124  flqdiv  10125  modqid  10153  modqid0  10154  mulqaddmodid  10168  ser3le  10322  expcl2lemap  10336  expnegzap  10358  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  ltexp2a  10376  leexp2a  10377  leexp2r  10378  exple1  10380  expubnd  10381  sq11  10396  bernneq2  10444  expnbnd  10446  nn0opthlem2d  10499  faclbnd  10519  bcp1nk  10540  remim  10664  reim0b  10666  rereb  10667  mulreap  10668  cjreb  10670  recj  10671  reneg  10672  readd  10673  resub  10674  remullem  10675  remul2  10677  redivap  10678  imcj  10679  imneg  10680  imadd  10681  imsub  10682  immul2  10684  imdivap  10685  cjcj  10687  cjadd  10688  ipcnval  10690  cjmulval  10692  cjneg  10694  imval2  10698  cjreim2  10708  cjap  10710  cnrecnv  10714  caucvgrelemrec  10783  cvg1nlemres  10789  recvguniqlem  10798  recvguniq  10799  resqrexlemover  10814  resqrexlemcalc1  10818  resqrexlemcalc2  10819  resqrexlemcalc3  10820  resqrexlemnmsq  10821  resqrexlemnm  10822  resqrexlemgt0  10824  resqrexlemoverl  10825  resqrexlemglsq  10826  remsqsqrt  10836  sqrtmul  10839  sqrtdiv  10846  sqrtmsq  10849  abs00ap  10866  absext  10867  abs00  10868  absdivap  10874  absid  10875  absexp  10883  absexpzap  10884  absimle  10888  abslt  10892  absle  10893  abssubap0  10894  abssubne0  10895  releabs  10900  recvalap  10901  abstri  10908  abs2difabs  10912  amgm2  10922  icodiamlt  10984  maxabsle  11008  maxabslemab  11010  maxabslemlub  11011  maxabslemval  11012  maxcl  11014  maxltsup  11022  max0addsup  11023  minmax  11033  minabs  11039  minclpr  11040  bdtrilem  11042  bdtri  11043  mul0inf  11044  climabs0  11108  reccn2ap  11114  climrecl  11125  climge0  11126  climle  11135  climsqz  11136  climsqz2  11137  climlec2  11142  climrecvg1n  11149  climcvg1nlem  11150  isumrecl  11230  isumge0  11231  fsumlessfi  11261  fsumge1  11262  fsum00  11263  fsumle  11264  fsumlt  11265  fsumabs  11266  iserabs  11276  isumrpcl  11295  isumle  11296  isumlessdc  11297  trireciplem  11301  trirecip  11302  expcnvre  11304  expcnv  11305  explecnv  11306  absltap  11310  geo2sum  11315  cvgratnnlembern  11324  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  cvgratnnlemabsle  11328  cvgratnnlemsumlt  11329  cvgratnnlemfm  11330  cvgratnnlemrate  11331  cvgratz  11333  mertenslemi1  11336  mertenslem2  11337  efcllemp  11401  ege2le3  11414  efaddlem  11417  efgt0  11427  reeftlcl  11432  eftlub  11433  effsumlt  11435  efltim  11441  eflegeo  11444  resin4p  11461  recos4p  11462  efeul  11477  ef01bndlem  11499  sin01bnd  11500  cos01bnd  11501  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  cos12dec  11510  absefi  11511  absef  11512  absefib  11513  efieq1re  11514  eirraplem  11519  dvdslelemd  11577  odd2np1  11606  divalglemnqt  11653  infssuzcldc  11680  nn0seqcvgd  11758  sqnprm  11852  metrtri  12585  bl2in  12611  blhalf  12616  blssps  12635  blss  12636  dedekindeu  12809  dedekindicclemicc  12818  ivthinclemlopn  12822  ivthinclemuopn  12824  ivthinc  12829  ivthdec  12830  dvcjbr  12880  dvfre  12882  dveflem  12895  reeff1olem  12900  reeff1oleme  12901  eflt  12904  sin0pilem1  12910  sin0pilem2  12911  pilem3  12912  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  sinq34lt0t  12960  cosq14gt0  12961  cosq23lt0  12962  coseq0q4123  12963  coseq0negpitopi  12965  tanrpcl  12966  tangtx  12967  coskpi  12977  cosordlem  12978  cosq34lt1  12979  cos11  12982  reexplog  13000  relogexp  13001  logdivlti  13010  rpcxpef  13023  rpcncxpcl  13031  cxpap0  13033  rpcxpadd  13034  rpmulcxp  13038  cxpmul  13041  abscxp  13043  cxplt  13044  cxplt3  13048  logsqrt  13051  apcxp2  13066  rpabscxpbnd  13067  rplogbid1  13072  rplogb1  13073  rpelogb  13074  rplogbchbase  13075  rplogbreexp  13078  rprelogbmul  13080  rprelogbdiv  13082  rplogbcxp  13088  rpcxplogb  13089  logbgcd1irraplemexp  13093  logbgcd1irraplemap  13094  qdencn  13397  refeq  13398  cvgcmp2nlemabs  13402  cvgcmp2n  13403  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trirec0  13412  apdifflemf  13414  apdifflemr  13415  apdiff  13416