Theorem recnd 8302

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

Syntax hints:   -> wi 4   e. wcel 2203   CCcc 8125   RRcr 8126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-resscn 8219

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  readdcan  8413  ltadd2  8693  ltadd1  8703  leadd2  8705  ltsubadd  8706  ltsubadd2  8707  lesubadd  8708  lesubadd2  8709  ltaddsub  8710  leaddsub  8712  lesub1  8730  lesub2  8731  ltsub1  8732  ltsub2  8733  ltnegcon1  8737  ltnegcon2  8738  add20  8748  subge0  8749  suble0  8750  lesub0  8753  eqord2  8758  possumd  8843  sublt0d  8844  rimul  8859  rereim  8860  apreap  8861  ltmul1a  8865  ltmul1  8866  reapmul1  8869  remulext2  8874  cru  8876  apreim  8877  mulreim  8878  apadd1  8882  apneg  8885  mulext1  8886  ltapd  8912  aprcl  8920  aptap  8924  rerecclap  9004  redivclap  9005  recgt0  9124  prodgt0gt0  9125  prodgt0  9126  prodge0  9128  lemul1a  9132  ltdiv1  9142  ltmuldiv  9148  ledivmul  9151  lt2mul2div  9153  ltrec  9157  lt2msq  9160  ltdiv2  9161  ltrec1  9162  lerec2  9163  ledivdiv  9164  lediv2  9165  ltdiv23  9166  lediv23  9167  lediv12a  9168  recp1lt1  9173  recreclt  9174  ledivp1  9177  mulle0r  9218  negiso  9229  avglt1  9477  avglt2  9478  div4p1lem1div2  9492  nn0cnd  9555  zcn  9582  peano2z  9613  zaddcllemneg  9616  ztri3or  9620  zeo  9683  zcnd  9701  eluzmn  9860  eluzelcn  9865  infrenegsupex  9926  supinfneg  9927  infsupneg  9928  supminfex  9929  irrmulap  9980  cnref1o  9983  rpcn  9995  rpcnd  10031  ltaddrp2d  10064  mul2lt0rlt0  10092  mul2lt0rgt0  10093  mul2lt0llt0  10094  mul2lt0lgt0  10095  mul2lt0np  10096  mul2lt0pn  10097  xpncan  10204  icoshftf1o  10324  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  infssuzcldc  10595  qbtwnrelemcalc  10615  flhalf  10662  intfracq  10682  flqdiv  10683  modqid  10711  modqid0  10712  mulqaddmodid  10726  seqf1oglem1  10881  ser3le  10899  expcl2lemap  10913  expnegzap  10935  expaddzaplem  10944  expaddzap  10945  expmulzap  10947  ltexp2a  10953  leexp2a  10954  leexp2r  10955  exple1  10957  expubnd  10958  sq11  10974  bernneq2  11023  expnbnd  11025  nn0ltexp2  11071  nn0opthlem2d  11083  faclbnd  11103  bcp1nk  11124  bcm1n  11131  remim  11545  reim0b  11547  rereb  11548  mulreap  11549  cjreb  11551  recj  11552  reneg  11553  readd  11554  resub  11555  remullem  11556  remul2  11558  redivap  11559  imcj  11560  imneg  11561  imadd  11562  imsub  11563  immul2  11565  imdivap  11566  cjcj  11568  cjadd  11569  ipcnval  11571  cjmulval  11573  cjneg  11575  imval2  11579  cjreim2  11589  cjap  11591  cnrecnv  11595  caucvgrelemrec  11664  cvg1nlemres  11670  recvguniqlem  11679  recvguniq  11680  resqrexlemover  11695  resqrexlemcalc1  11699  resqrexlemcalc2  11700  resqrexlemcalc3  11701  resqrexlemnmsq  11702  resqrexlemnm  11703  resqrexlemgt0  11705  resqrexlemoverl  11706  resqrexlemglsq  11707  remsqsqrt  11717  sqrtmul  11720  sqrtdiv  11727  sqrtmsq  11730  abs00ap  11747  absext  11748  abs00  11749  absdivap  11755  absid  11756  absexp  11764  absexpzap  11765  absimle  11769  abslt  11773  absle  11774  abssubap0  11775  abssubne0  11776  releabs  11781  recvalap  11782  abstri  11789  abs2difabs  11793  amgm2  11803  icodiamlt  11865  maxabsle  11889  maxabslemab  11891  maxabslemlub  11892  maxabslemval  11893  maxcl  11895  maxltsup  11903  max0addsup  11904  minmax  11915  minabs  11921  minclpr  11922  bdtrilem  11924  bdtri  11925  mul0inf  11926  mingeb  11927  climabs0  11992  reccn2ap  11998  climrecl  12009  climge0  12010  climle  12019  climsqz  12020  climsqz2  12021  climlec2  12026  climrecvg1n  12033  climcvg1nlem  12034  isumrecl  12115  isumge0  12116  fsumlessfi  12146  fsumge1  12147  fsum00  12148  fsumle  12149  fsumlt  12150  fsumabs  12151  iserabs  12161  isumrpcl  12180  isumle  12181  isumlessdc  12182  trireciplem  12186  trirecip  12187  expcnvre  12189  expcnv  12190  explecnv  12191  absltap  12195  geo2sum  12200  cvgratnnlembern  12209  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  cvgratnnlemabsle  12213  cvgratnnlemsumlt  12214  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratz  12218  mertenslemi1  12221  mertenslem2  12222  fprodabs  12302  fprodle  12326  efcllemp  12344  ege2le3  12357  efaddlem  12360  efgt0  12370  reeftlcl  12375  eftlub  12376  effsumlt  12378  efltim  12384  eflegeo  12387  resin4p  12404  recos4p  12405  efeul  12420  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  cos12dec  12454  absefi  12455  absef  12456  absefib  12457  efieq1re  12458  eirraplem  12463  dvdsaddre2b  12527  dvdslelemd  12529  odd2np1  12559  divalglemnqt  12606  bitsp1o  12639  bitsfzo  12641  bitscmp  12644  nn0seqcvgd  12738  sqnprm  12833  isprm5lem  12838  odzdvds  12943  pythagtriplem14  12975  pcid  13022  fldivp1  13046  pockthlem  13054  4sqlem5  13080  4sqlem10  13085  mul4sqlem  13091  4sqlem15  13103  4sqlem16  13104  mulgneg  13857  ghmmulg  13973  rege0subm  14732  metrtri  15242  bl2in  15268  blhalf  15273  blssps  15292  blss  15293  maxcncf  15480  mincncf  15481  dedekindeu  15488  dedekindicclemicc  15497  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthinc  15508  ivthdec  15509  ivthreinc  15510  dvconstre  15561  dvidre  15562  dvcjbr  15573  dvfre  15575  dveflem  15591  plyrecj  15628  reeff1olem  15636  reeff1oleme  15637  eflt  15640  sin0pilem1  15646  sin0pilem2  15647  pilem3  15648  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  sinq34lt0t  15696  cosq14gt0  15697  cosq23lt0  15698  coseq0q4123  15699  coseq0negpitopi  15701  tanrpcl  15702  tangtx  15703  coskpi  15713  cosordlem  15714  cosq34lt1  15715  cos11  15718  reexplog  15736  relogexp  15737  logdivlti  15746  rpcxpef  15759  rpcncxpcl  15767  cxpap0  15769  rpcxpadd  15770  rpmulcxp  15774  cxpmul  15777  abscxp  15780  cxplt  15781  cxplt3  15785  logsqrt  15788  apcxp2  15804  rpabscxpbnd  15805  rplogbid1  15812  rplogb1  15813  rpelogb  15814  rplogbchbase  15815  rplogbreexp  15818  rprelogbmul  15820  rprelogbdiv  15822  rplogbcxp  15828  rpcxplogb  15829  logbgcd1irraplemexp  15833  logbgcd1irraplemap  15834  pellexlem2  15846  mersenne  15865  lgsvalmod  15892  lgsdilem  15900  lgsne0  15911  gausslemma2dlem1a  15931  gausslemma2dlem6  15940  lgseisenlem1  15943  lgseisenlem2  15944  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  2sqlem1  15987  mul2sq  15989  2sqlem3  15990  2sqlem8  15996  qdencn  16807  refeq  16808  repiecele0  16810  repiecege0  16811  cvgcmp2nlemabs  16816  cvgcmp2n  16817  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  trirec0  16828  apdifflemf  16830  apdifflemr  16831  apdiff  16832  qdiff  16833  redc0  16842  reap0  16843  cndcap  16844  nconstwlpolem0  16849  nconstwlpolemgt0  16850  neap0mkv  16855  ltlenmkv  16856