Theorem recnd 8354

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   CCcc 8177   RRcr 8178

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8271

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  readdcan  8467  ltadd2  8748  ltadd1  8758  leadd2  8760  ltsubadd  8761  ltsubadd2  8762  lesubadd  8763  lesubadd2  8764  ltaddsub  8765  leaddsub  8767  lesub1  8785  lesub2  8786  ltsub1  8787  ltsub2  8788  ltnegcon1  8792  ltnegcon2  8793  add20  8803  subge0  8804  suble0  8805  lesub0  8808  eqord2  8813  lesub3d  8892  possumd  8899  sublt0d  8900  rimul  8915  rereim  8916  apreap  8917  ltmul1a  8921  ltmul1  8922  reapmul1  8925  remulext2  8930  cru  8932  apreim  8933  mulreim  8934  apadd1  8938  apneg  8941  mulext1  8942  ltapd  8968  aprcl  8976  aptap  8980  rerecclap  9062  redivclap  9063  recgt0  9182  prodgt0gt0  9183  prodgt0  9184  prodge0  9186  lemul1a  9190  ltdiv1  9200  ltmuldiv  9206  ledivmul  9209  lt2mul2div  9211  ltrec  9215  lt2msq  9218  ltdiv2  9219  ltrec1  9220  lerec2  9221  ledivdiv  9222  lediv2  9223  ltdiv23  9224  lediv23  9225  lediv12a  9226  recp1lt1  9231  recreclt  9232  ledivp1  9235  mulle0r  9276  negiso  9287  avglt1  9548  avglt2  9549  div4p1lem1div2  9563  nn0cnd  9626  zcn  9653  peano2z  9684  zaddcllemneg  9687  ztri3or  9691  zeo  9755  zcnd  9773  eluzmn  9937  eluzelcn  9942  infrenegsupex  10003  supinfneg  10004  infsupneg  10005  supminfex  10006  irraddap  10056  irrmulap  10058  cnref1o  10061  rpcn  10073  rpcnd  10109  ltaddrp2d  10142  mul2lt0rlt0  10170  mul2lt0rgt0  10171  mul2lt0llt0  10172  mul2lt0lgt0  10173  mul2lt0np  10174  mul2lt0pn  10175  xpncan  10283  icoshftf1o  10403  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  infssuzcldc  10678  qbtwnrelemcalc  10700  flhalf  10750  intfracq  10770  flqdiv  10771  modqid  10799  modqid0  10800  mulqaddmodid  10814  seqf1oglem1  10969  ser3le  10987  expcl2lemap  11001  expnegzap  11023  expaddzaplem  11032  expaddzap  11033  expmulzap  11035  ltexp2a  11041  leexp2a  11042  leexp2r  11043  exple1  11045  expubnd  11046  sq11  11062  resq01  11108  bernneq2  11112  expnbnd  11114  nn0ltexp2  11161  nn0opthlem2d  11173  faclbnd  11193  bcp1nk  11214  bcm1n  11221  remim  11639  reim0b  11641  rereb  11642  mulreap  11643  cjreb  11645  recj  11646  reneg  11647  readd  11648  resub  11649  remullem  11650  remul2  11652  redivap  11653  imcj  11654  imneg  11655  imadd  11656  imsub  11657  immul2  11659  imdivap  11660  cjcj  11662  cjadd  11663  ipcnval  11665  cjmulval  11667  cjneg  11669  imval2  11673  sq01  11674  cjreim2  11684  cjap  11686  cnrecnv  11690  caucvgrelemrec  11759  cvg1nlemres  11765  recvguniqlem  11774  recvguniq  11775  resqrexlemover  11790  resqrexlemcalc1  11794  resqrexlemcalc2  11795  resqrexlemcalc3  11796  resqrexlemnmsq  11797  resqrexlemnm  11798  resqrexlemgt0  11800  resqrexlemoverl  11801  resqrexlemglsq  11802  remsqsqrt  11812  sqrtmul  11815  sqrtdiv  11822  sqrtmsq  11825  abs00ap  11842  absext  11843  abs00  11844  absdivap  11850  absid  11851  absexp  11860  absexpzap  11861  absimle  11865  abslt  11869  absle  11870  abssubap0  11871  abssubne0  11872  releabs  11877  recvalap  11878  abstri  11885  abs2difabs  11889  amgm2  11899  icodiamlt  11961  maxabsle  11985  maxabslemab  11987  maxabslemlub  11988  maxabslemval  11989  maxcl  11991  maxltsup  11999  max0addsup  12000  minmax  12011  minabs  12017  minclpr  12018  bdtrilem  12021  bdtri  12022  mul0inf  12023  mingeb  12024  climabs0  12089  reccn2ap  12095  climrecl  12106  climge0  12107  climle  12116  climsqz  12117  climsqz2  12118  climlec2  12123  climrecvg1n  12130  climcvg1nlem  12131  isumrecl  12212  isumge0  12213  fsumlessfi  12243  fsumge1  12244  fsum00  12245  fsumle  12246  fsumlt  12247  fsumabs  12248  iserabs  12258  isumrpcl  12277  isumle  12278  isumlessdc  12279  trireciplem  12283  trirecip  12284  expcnvre  12286  expcnv  12287  explecnv  12288  absltap  12292  geo2sum  12297  cvgratnnlembern  12306  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  cvgratnnlemabsle  12310  cvgratnnlemsumlt  12311  cvgratnnlemfm  12312  cvgratnnlemrate  12313  cvgratz  12315  mertenslemi1  12318  mertenslem2  12319  fprodabs  12399  fprodle  12423  efcllemp  12441  ege2le3  12454  efaddlem  12457  efgt0  12467  reeftlcl  12472  eftlub  12473  effsumlt  12475  efltim  12481  eflegeo  12484  resin4p  12501  recos4p  12502  efeul  12517  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  cos12dec  12551  absefi  12552  absef  12553  absefib  12554  efieq1re  12555  eirraplem  12560  dvdsaddre2b  12624  dvdslelemd  12626  odd2np1  12656  divalglemnqt  12703  bitsp1o  12736  bitsfzo  12738  bitscmp  12741  nn0seqcvgd  12835  sqnprm  12931  isprm5lem  12936  nn0sqdcq  13004  odzdvds  13044  pythagtriplem14  13076  pcid  13123  fldivp1  13147  pockthlem  13155  4sqlem5  13181  4sqlem10  13186  mul4sqlem  13192  4sqlem15  13204  4sqlem16  13205  ballotfilemsi  13307  mulgneg  13992  ghmmulg  14108  rege0subm  14970  metrtri  15527  bl2in  15553  blhalf  15558  blssps  15577  blss  15578  maxcncf  15765  mincncf  15766  dedekindeu  15773  dedekindicclemicc  15782  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthinc  15793  ivthdec  15794  ivthreinc  15795  dvconstre  15846  dvidre  15847  dvcjbr  15858  dvfre  15860  dveflem  15876  plyrecj  15913  reeff1olem  15921  reeff1oleme  15922  eflt  15925  efap1p  15929  sin0pilem1  15932  sin0pilem2  15933  pilem3  15934  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  sinq34lt0t  15982  cosq14gt0  15983  cosq23lt0  15984  coseq0q4123  15985  coseq0negpitopi  15987  tanrpcl  15988  tangtx  15989  coskpi  15999  cosordlem  16000  cosq34lt1  16001  cos11  16004  reexplog  16023  relogexp  16024  logdivlti  16033  logdivlt  16046  logfac  16048  rpcxpef  16049  rpcncxpcl  16057  cxpap0  16059  rpcxpadd  16060  rpmulcxp  16064  cxpmul  16067  abscxp  16070  cxplt  16071  cxplt3  16075  logsqrt  16078  apcxp2  16094  rpabscxpbnd  16095  rplogbid1  16102  rplogb1  16103  rpelogb  16104  rplogbchbase  16105  rplogbreexp  16108  rprelogbmul  16110  rprelogbdiv  16112  rplogbcxp  16118  rpcxplogb  16119  logbgcd1irraplemexp  16123  logbgcd1irraplemap  16124  zprmlogbaplem2  16135  log2tlbndlog2  16139  log2ublem2  16141  birthdaylem2  16145  birthdaylem3  16146  pellexlem2  16149  ppiqub  16194  mersenne  16195  bcmax  16203  bcp1ctr  16204  bposlem1  16209  lgsvalmod  16236  lgsdilem  16244  lgsne0  16255  gausslemma2dlem1a  16275  gausslemma2dlem6  16284  lgseisenlem1  16287  lgseisenlem2  16288  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  2sqlem1  16331  mul2sq  16333  2sqlem3  16334  2sqlem8  16340  dichmul0orlem1  16851  dichmul0orlem4  16854  dichmul0orlem5  16855  dichmul0orlem6  16856  dichmul0orlem7  16857  qdencn  17170  refeq  17171  repiecele0  17173  repiecege0  17174  cvgcmp2nlemabs  17179  cvgcmp2n  17180  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  trirec0  17191  apdifflemf  17193  apdifflemr  17194  apdiff  17195  qdiff  17196  redc0  17205  reap0  17206  cndcap  17207  nconstwlpolem0  17211  nconstwlpolemgt0  17212  neap0mkv  17217  ltlenmkv  17218