Theorem recnd 8208

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 8165	. 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 8030   RRcr 8031

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 8124

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  8319  ltadd2  8599  ltadd1  8609  leadd2  8611  ltsubadd  8612  ltsubadd2  8613  lesubadd  8614  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  ltnegcon1  8643  ltnegcon2  8644  add20  8654  subge0  8655  suble0  8656  lesub0  8659  eqord2  8664  possumd  8749  sublt0d  8750  rimul  8765  rereim  8766  apreap  8767  ltmul1a  8771  ltmul1  8772  reapmul1  8775  remulext2  8780  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  mulext1  8792  ltapd  8818  aprcl  8826  aptap  8830  rerecclap  8910  redivclap  8911  recgt0  9030  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemul1a  9038  ltdiv1  9048  ltmuldiv  9054  ledivmul  9057  lt2mul2div  9059  ltrec  9063  lt2msq  9066  ltdiv2  9067  ltrec1  9068  lerec2  9069  ledivdiv  9070  lediv2  9071  ltdiv23  9072  lediv23  9073  lediv12a  9074  recp1lt1  9079  recreclt  9080  ledivp1  9083  mulle0r  9124  negiso  9135  avglt1  9383  avglt2  9384  div4p1lem1div2  9398  nn0cnd  9457  zcn  9484  peano2z  9515  zaddcllemneg  9518  ztri3or  9522  zeo  9585  zcnd  9603  eluzmn  9762  eluzelcn  9767  infrenegsupex  9828  supinfneg  9829  infsupneg  9830  supminfex  9831  irrmulap  9882  cnref1o  9885  rpcn  9897  rpcnd  9933  ltaddrp2d  9966  mul2lt0rlt0  9994  mul2lt0rgt0  9995  mul2lt0llt0  9996  mul2lt0lgt0  9997  mul2lt0np  9998  mul2lt0pn  9999  xpncan  10106  icoshftf1o  10226  lincmb01cmp  10238  iccf1o  10239  infssuzcldc  10496  qbtwnrelemcalc  10516  flhalf  10563  intfracq  10583  flqdiv  10584  modqid  10612  modqid0  10613  mulqaddmodid  10627  seqf1oglem1  10782  ser3le  10800  expcl2lemap  10814  expnegzap  10836  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  ltexp2a  10854  leexp2a  10855  leexp2r  10856  exple1  10858  expubnd  10859  sq11  10875  bernneq2  10924  expnbnd  10926  nn0ltexp2  10972  nn0opthlem2d  10984  faclbnd  11004  bcp1nk  11025  remim  11438  reim0b  11440  rereb  11441  mulreap  11442  cjreb  11444  recj  11445  reneg  11446  readd  11447  resub  11448  remullem  11449  remul2  11451  redivap  11452  imcj  11453  imneg  11454  imadd  11455  imsub  11456  immul2  11458  imdivap  11459  cjcj  11461  cjadd  11462  ipcnval  11464  cjmulval  11466  cjneg  11468  imval2  11472  cjreim2  11482  cjap  11484  cnrecnv  11488  caucvgrelemrec  11557  cvg1nlemres  11563  recvguniqlem  11572  recvguniq  11573  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemnmsq  11595  resqrexlemnm  11596  resqrexlemgt0  11598  resqrexlemoverl  11599  resqrexlemglsq  11600  remsqsqrt  11610  sqrtmul  11613  sqrtdiv  11620  sqrtmsq  11623  abs00ap  11640  absext  11641  abs00  11642  absdivap  11648  absid  11649  absexp  11657  absexpzap  11658  absimle  11662  abslt  11666  absle  11667  abssubap0  11668  abssubne0  11669  releabs  11674  recvalap  11675  abstri  11682  abs2difabs  11686  amgm2  11696  icodiamlt  11758  maxabsle  11782  maxabslemab  11784  maxabslemlub  11785  maxabslemval  11786  maxcl  11788  maxltsup  11796  max0addsup  11797  minmax  11808  minabs  11814  minclpr  11815  bdtrilem  11817  bdtri  11818  mul0inf  11819  mingeb  11820  climabs0  11885  reccn2ap  11891  climrecl  11902  climge0  11903  climle  11912  climsqz  11913  climsqz2  11914  climlec2  11919  climrecvg1n  11926  climcvg1nlem  11927  isumrecl  12008  isumge0  12009  fsumlessfi  12039  fsumge1  12040  fsum00  12041  fsumle  12042  fsumlt  12043  fsumabs  12044  iserabs  12054  isumrpcl  12073  isumle  12074  isumlessdc  12075  trireciplem  12079  trirecip  12080  expcnvre  12082  expcnv  12083  explecnv  12084  absltap  12088  geo2sum  12093  cvgratnnlembern  12102  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  cvgratnnlemabsle  12106  cvgratnnlemsumlt  12107  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratz  12111  mertenslemi1  12114  mertenslem2  12115  fprodabs  12195  fprodle  12219  efcllemp  12237  ege2le3  12250  efaddlem  12253  efgt0  12263  reeftlcl  12268  eftlub  12269  effsumlt  12271  efltim  12277  eflegeo  12280  resin4p  12297  recos4p  12298  efeul  12313  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  cos12dec  12347  absefi  12348  absef  12349  absefib  12350  efieq1re  12351  eirraplem  12356  dvdsaddre2b  12420  dvdslelemd  12422  odd2np1  12452  divalglemnqt  12499  bitsp1o  12532  bitsfzo  12534  bitscmp  12537  nn0seqcvgd  12631  sqnprm  12726  isprm5lem  12731  odzdvds  12836  pythagtriplem14  12868  pcid  12915  fldivp1  12939  pockthlem  12947  4sqlem5  12973  4sqlem10  12978  mul4sqlem  12984  4sqlem15  12996  4sqlem16  12997  mulgneg  13745  ghmmulg  13861  rege0subm  14617  metrtri  15120  bl2in  15146  blhalf  15151  blssps  15170  blss  15171  maxcncf  15358  mincncf  15359  dedekindeu  15366  dedekindicclemicc  15375  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthinc  15386  ivthdec  15387  ivthreinc  15388  dvconstre  15439  dvidre  15440  dvcjbr  15451  dvfre  15453  dveflem  15469  plyrecj  15506  reeff1olem  15514  reeff1oleme  15515  eflt  15518  sin0pilem1  15524  sin0pilem2  15525  pilem3  15526  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  sinq12gt0  15573  sinq34lt0t  15574  cosq14gt0  15575  cosq23lt0  15576  coseq0q4123  15577  coseq0negpitopi  15579  tanrpcl  15580  tangtx  15581  coskpi  15591  cosordlem  15592  cosq34lt1  15593  cos11  15596  reexplog  15614  relogexp  15615  logdivlti  15624  rpcxpef  15637  rpcncxpcl  15645  cxpap0  15647  rpcxpadd  15648  rpmulcxp  15652  cxpmul  15655  abscxp  15658  cxplt  15659  cxplt3  15663  logsqrt  15666  apcxp2  15682  rpabscxpbnd  15683  rplogbid1  15690  rplogb1  15691  rpelogb  15692  rplogbchbase  15693  rplogbreexp  15696  rprelogbmul  15698  rprelogbdiv  15700  rplogbcxp  15706  rpcxplogb  15707  logbgcd1irraplemexp  15711  logbgcd1irraplemap  15712  mersenne  15740  lgsvalmod  15767  lgsdilem  15775  lgsne0  15786  gausslemma2dlem1a  15806  gausslemma2dlem6  15815  lgseisenlem1  15818  lgseisenlem2  15819  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  2sqlem1  15862  mul2sq  15864  2sqlem3  15865  2sqlem8  15871  qdencn  16682  refeq  16683  cvgcmp2nlemabs  16687  cvgcmp2n  16688  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  trirec0  16699  apdifflemf  16701  apdifflemr  16702  apdiff  16703  qdiff  16704  redc0  16713  reap0  16714  cndcap  16715  nconstwlpolem0  16719  nconstwlpolemgt0  16720  neap0mkv  16725  ltlenmkv  16726