Theorem recnd 8207

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8029   RRcr 8030

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8123

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  readdcan  8318  ltadd2  8598  ltadd1  8608  leadd2  8610  ltsubadd  8611  ltsubadd2  8612  lesubadd  8613  lesubadd2  8614  ltaddsub  8615  leaddsub  8617  lesub1  8635  lesub2  8636  ltsub1  8637  ltsub2  8638  ltnegcon1  8642  ltnegcon2  8643  add20  8653  subge0  8654  suble0  8655  lesub0  8658  eqord2  8663  possumd  8748  sublt0d  8749  rimul  8764  rereim  8765  apreap  8766  ltmul1a  8770  ltmul1  8771  reapmul1  8774  remulext2  8779  cru  8781  apreim  8782  mulreim  8783  apadd1  8787  apneg  8790  mulext1  8791  ltapd  8817  aprcl  8825  aptap  8829  rerecclap  8909  redivclap  8910  recgt0  9029  prodgt0gt0  9030  prodgt0  9031  prodge0  9033  lemul1a  9037  ltdiv1  9047  ltmuldiv  9053  ledivmul  9056  lt2mul2div  9058  ltrec  9062  lt2msq  9065  ltdiv2  9066  ltrec1  9067  lerec2  9068  ledivdiv  9069  lediv2  9070  ltdiv23  9071  lediv23  9072  lediv12a  9073  recp1lt1  9078  recreclt  9079  ledivp1  9082  mulle0r  9123  negiso  9134  avglt1  9382  avglt2  9383  div4p1lem1div2  9397  nn0cnd  9456  zcn  9483  peano2z  9514  zaddcllemneg  9517  ztri3or  9521  zeo  9584  zcnd  9602  eluzmn  9761  eluzelcn  9766  infrenegsupex  9827  supinfneg  9828  infsupneg  9829  supminfex  9830  irrmulap  9881  cnref1o  9884  rpcn  9896  rpcnd  9932  ltaddrp2d  9965  mul2lt0rlt0  9993  mul2lt0rgt0  9994  mul2lt0llt0  9995  mul2lt0lgt0  9996  mul2lt0np  9997  mul2lt0pn  9998  xpncan  10105  icoshftf1o  10225  lincmb01cmp  10237  iccf1o  10238  infssuzcldc  10494  qbtwnrelemcalc  10514  flhalf  10561  intfracq  10581  flqdiv  10582  modqid  10610  modqid0  10611  mulqaddmodid  10625  seqf1oglem1  10780  ser3le  10798  expcl2lemap  10812  expnegzap  10834  expaddzaplem  10843  expaddzap  10844  expmulzap  10846  ltexp2a  10852  leexp2a  10853  leexp2r  10854  exple1  10856  expubnd  10857  sq11  10873  bernneq2  10922  expnbnd  10924  nn0ltexp2  10970  nn0opthlem2d  10982  faclbnd  11002  bcp1nk  11023  remim  11420  reim0b  11422  rereb  11423  mulreap  11424  cjreb  11426  recj  11427  reneg  11428  readd  11429  resub  11430  remullem  11431  remul2  11433  redivap  11434  imcj  11435  imneg  11436  imadd  11437  imsub  11438  immul2  11440  imdivap  11441  cjcj  11443  cjadd  11444  ipcnval  11446  cjmulval  11448  cjneg  11450  imval2  11454  cjreim2  11464  cjap  11466  cnrecnv  11470  caucvgrelemrec  11539  cvg1nlemres  11545  recvguniqlem  11554  recvguniq  11555  resqrexlemover  11570  resqrexlemcalc1  11574  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemnmsq  11577  resqrexlemnm  11578  resqrexlemgt0  11580  resqrexlemoverl  11581  resqrexlemglsq  11582  remsqsqrt  11592  sqrtmul  11595  sqrtdiv  11602  sqrtmsq  11605  abs00ap  11622  absext  11623  abs00  11624  absdivap  11630  absid  11631  absexp  11639  absexpzap  11640  absimle  11644  abslt  11648  absle  11649  abssubap0  11650  abssubne0  11651  releabs  11656  recvalap  11657  abstri  11664  abs2difabs  11668  amgm2  11678  icodiamlt  11740  maxabsle  11764  maxabslemab  11766  maxabslemlub  11767  maxabslemval  11768  maxcl  11770  maxltsup  11778  max0addsup  11779  minmax  11790  minabs  11796  minclpr  11797  bdtrilem  11799  bdtri  11800  mul0inf  11801  mingeb  11802  climabs0  11867  reccn2ap  11873  climrecl  11884  climge0  11885  climle  11894  climsqz  11895  climsqz2  11896  climlec2  11901  climrecvg1n  11908  climcvg1nlem  11909  isumrecl  11989  isumge0  11990  fsumlessfi  12020  fsumge1  12021  fsum00  12022  fsumle  12023  fsumlt  12024  fsumabs  12025  iserabs  12035  isumrpcl  12054  isumle  12055  isumlessdc  12056  trireciplem  12060  trirecip  12061  expcnvre  12063  expcnv  12064  explecnv  12065  absltap  12069  geo2sum  12074  cvgratnnlembern  12083  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  cvgratnnlemabsle  12087  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratz  12092  mertenslemi1  12095  mertenslem2  12096  fprodabs  12176  fprodle  12200  efcllemp  12218  ege2le3  12231  efaddlem  12234  efgt0  12244  reeftlcl  12249  eftlub  12250  effsumlt  12252  efltim  12258  eflegeo  12261  resin4p  12278  recos4p  12279  efeul  12294  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  cos12dec  12328  absefi  12329  absef  12330  absefib  12331  efieq1re  12332  eirraplem  12337  dvdsaddre2b  12401  dvdslelemd  12403  odd2np1  12433  divalglemnqt  12480  bitsp1o  12513  bitsfzo  12515  bitscmp  12518  nn0seqcvgd  12612  sqnprm  12707  isprm5lem  12712  odzdvds  12817  pythagtriplem14  12849  pcid  12896  fldivp1  12920  pockthlem  12928  4sqlem5  12954  4sqlem10  12959  mul4sqlem  12965  4sqlem15  12977  4sqlem16  12978  mulgneg  13726  ghmmulg  13842  rege0subm  14597  metrtri  15100  bl2in  15126  blhalf  15131  blssps  15150  blss  15151  maxcncf  15338  mincncf  15339  dedekindeu  15346  dedekindicclemicc  15355  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthinc  15366  ivthdec  15367  ivthreinc  15368  dvconstre  15419  dvidre  15420  dvcjbr  15431  dvfre  15433  dveflem  15449  plyrecj  15486  reeff1olem  15494  reeff1oleme  15495  eflt  15498  sin0pilem1  15504  sin0pilem2  15505  pilem3  15506  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  sinq34lt0t  15554  cosq14gt0  15555  cosq23lt0  15556  coseq0q4123  15557  coseq0negpitopi  15559  tanrpcl  15560  tangtx  15561  coskpi  15571  cosordlem  15572  cosq34lt1  15573  cos11  15576  reexplog  15594  relogexp  15595  logdivlti  15604  rpcxpef  15617  rpcncxpcl  15625  cxpap0  15627  rpcxpadd  15628  rpmulcxp  15632  cxpmul  15635  abscxp  15638  cxplt  15639  cxplt3  15643  logsqrt  15646  apcxp2  15662  rpabscxpbnd  15663  rplogbid1  15670  rplogb1  15671  rpelogb  15672  rplogbchbase  15673  rplogbreexp  15676  rprelogbmul  15678  rprelogbdiv  15680  rplogbcxp  15686  rpcxplogb  15687  logbgcd1irraplemexp  15691  logbgcd1irraplemap  15692  mersenne  15720  lgsvalmod  15747  lgsdilem  15755  lgsne0  15766  gausslemma2dlem1a  15786  gausslemma2dlem6  15795  lgseisenlem1  15798  lgseisenlem2  15799  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  2sqlem1  15842  mul2sq  15844  2sqlem3  15845  2sqlem8  15851  qdencn  16631  refeq  16632  cvgcmp2nlemabs  16636  cvgcmp2n  16637  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trirec0  16648  apdifflemf  16650  apdifflemr  16651  apdiff  16652  redc0  16661  reap0  16662  cndcap  16663  nconstwlpolem0  16667  nconstwlpolemgt0  16668  neap0mkv  16673  ltlenmkv  16674