Theorem recnd 8360

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 8318	. 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 8183   RRcr 8184

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 8277

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  8473  ltadd2  8754  ltadd1  8764  leadd2  8766  ltsubadd  8767  ltsubadd2  8768  lesubadd  8769  lesubadd2  8770  ltaddsub  8771  leaddsub  8773  lesub1  8791  lesub2  8792  ltsub1  8793  ltsub2  8794  ltnegcon1  8798  ltnegcon2  8799  add20  8809  subge0  8810  suble0  8811  lesub0  8814  eqord2  8819  lesub3d  8898  possumd  8905  sublt0d  8906  rimul  8921  rereim  8922  apreap  8923  ltmul1a  8927  ltmul1  8928  reapmul1  8931  remulext2  8936  cru  8938  apreim  8939  mulreim  8940  apadd1  8944  apneg  8947  mulext1  8948  ltapd  8974  aprcl  8982  aptap  8986  rerecclap  9068  redivclap  9069  recgt0  9188  prodgt0gt0  9189  prodgt0  9190  prodge0  9192  lemul1a  9196  ltdiv1  9206  ltmuldiv  9212  ledivmul  9215  lt2mul2div  9217  ltrec  9221  lt2msq  9224  ltdiv2  9225  ltrec1  9226  lerec2  9227  ledivdiv  9228  lediv2  9229  ltdiv23  9230  lediv23  9231  lediv12a  9232  recp1lt1  9237  recreclt  9238  ledivp1  9241  mulle0r  9282  negiso  9293  avglt1  9555  avglt2  9556  div4p1lem1div2  9570  nn0cnd  9631  zcn  9658  peano2z  9689  zaddcllemneg  9692  ztri3or  9696  zeo  9761  zcnd  9779  eluzmn  9943  eluzelcn  9948  infrenegsupex  10009  supinfneg  10010  infsupneg  10011  supminfex  10012  irraddap  10062  irrmulap  10064  cnref1o  10067  rpcn  10079  rpcnd  10115  ltaddrp2d  10148  mul2lt0rlt0  10176  mul2lt0rgt0  10177  mul2lt0llt0  10178  mul2lt0lgt0  10179  mul2lt0np  10180  mul2lt0pn  10181  xpncan  10289  icoshftf1o  10409  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  infssuzcldc  10684  qbtwnrelemcalc  10706  flhalf  10757  intfracq  10777  flqdiv  10778  modqid  10806  modqid0  10807  mulqaddmodid  10821  seqf1oglem1  10976  ser3le  10994  expcl2lemap  11008  expnegzap  11030  expaddzaplem  11039  expaddzap  11040  expmulzap  11042  ltexp2a  11048  leexp2a  11049  leexp2r  11050  exple1  11052  expubnd  11053  sq11  11069  resq01  11115  bernneq2  11119  expnbnd  11121  nn0ltexp2  11168  nn0opthlem2d  11180  faclbnd  11200  bcp1nk  11221  bcm1n  11228  remim  11646  reim0b  11648  rereb  11649  mulreap  11650  cjreb  11652  recj  11653  reneg  11654  readd  11655  resub  11656  remullem  11657  remul2  11659  redivap  11660  imcj  11661  imneg  11662  imadd  11663  imsub  11664  immul2  11666  imdivap  11667  cjcj  11669  cjadd  11670  ipcnval  11672  cjmulval  11674  cjneg  11676  imval2  11680  sq01  11681  cjreim2  11691  cjap  11693  cnrecnv  11697  caucvgrelemrec  11766  cvg1nlemres  11772  recvguniqlem  11781  recvguniq  11782  resqrexlemover  11797  resqrexlemcalc1  11801  resqrexlemcalc2  11802  resqrexlemcalc3  11803  resqrexlemnmsq  11804  resqrexlemnm  11805  resqrexlemgt0  11807  resqrexlemoverl  11808  resqrexlemglsq  11809  remsqsqrt  11819  sqrtmul  11822  sqrtdiv  11829  sqrtmsq  11832  abs00ap  11849  absext  11850  abs00  11851  absdivap  11857  absid  11858  absexp  11867  absexpzap  11868  absimle  11872  abslt  11876  absle  11877  abssubap0  11878  abssubne0  11879  releabs  11884  recvalap  11885  abstri  11892  abs2difabs  11896  amgm2  11906  icodiamlt  11968  maxabsle  11992  maxabslemab  11994  maxabslemlub  11995  maxabslemval  11996  maxcl  11998  maxltsup  12006  max0addsup  12007  minmax  12019  minabs  12025  minclpr  12026  bdtrilem  12029  bdtri  12030  mul0inf  12031  mingeb  12032  climabs0  12097  reccn2ap  12103  climrecl  12114  climge0  12115  climle  12124  climsqz  12125  climsqz2  12126  climlec2  12131  climrecvg1n  12138  climcvg1nlem  12139  isumrecl  12220  isumge0  12221  fsumlessfi  12251  fsumge1  12252  fsum00  12253  fsumle  12254  fsumlt  12255  fsumabs  12256  iserabs  12266  isumrpcl  12285  isumle  12286  isumlessdc  12287  trireciplem  12291  trirecip  12292  expcnvre  12294  expcnv  12295  explecnv  12296  absltap  12300  geo2sum  12305  cvgratnnlembern  12314  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  cvgratnnlemabsle  12318  cvgratnnlemsumlt  12319  cvgratnnlemfm  12320  cvgratnnlemrate  12321  cvgratz  12323  mertenslemi1  12326  mertenslem2  12327  fprodabs  12407  fprodle  12431  efcllemp  12449  ege2le3  12462  efaddlem  12465  efgt0  12475  reeftlcl  12480  eftlub  12481  effsumlt  12483  efltim  12489  eflegeo  12492  resin4p  12509  recos4p  12510  efeul  12525  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  cos12dec  12559  absefi  12560  absef  12561  absefib  12562  efieq1re  12563  eirraplem  12568  dvdsaddre2b  12632  dvdslelemd  12634  odd2np1  12664  divalglemnqt  12711  bitsp1o  12744  bitsfzo  12746  bitscmp  12749  nn0seqcvgd  12843  sqnprm  12939  isprm5lem  12944  nn0sqdcq  13012  odzdvds  13052  pythagtriplem14  13084  pcid  13131  fldivp1  13155  pockthlem  13163  4sqlem5  13189  4sqlem10  13194  mul4sqlem  13200  4sqlem15  13212  4sqlem16  13213  ballotfilemsi  13315  mulgneg  14001  ghmmulg  14117  rege0subm  15029  metrtri  15620  bl2in  15646  blhalf  15651  blssps  15670  blss  15671  maxcncf  15858  mincncf  15859  dedekindeu  15866  dedekindicclemicc  15875  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthinc  15886  ivthdec  15887  ivthreinc  15888  dvconstre  15939  dvidre  15940  dvcjbr  15951  dvfre  15953  dveflem  15969  plyrecj  16006  reeff1olem  16014  reeff1oleme  16015  eflt  16018  efap1p  16022  sin0pilem1  16025  sin0pilem2  16026  pilem3  16027  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  sinq34lt0t  16075  cosq14gt0  16076  cosq23lt0  16077  coseq0q4123  16078  coseq0negpitopi  16080  tanrpcl  16081  tangtx  16082  coskpi  16092  cosordlem  16094  cosq34lt1  16095  cos11  16098  reexplog  16118  relogexp  16119  logdivlti  16128  logdivlt  16141  logfac  16143  rpcxpef  16144  rpcncxpcl  16152  cxpap0  16154  rpcxpadd  16155  rpmulcxp  16159  cxpmul  16162  rpcxpmul2z  16165  abscxp  16167  cxplt  16168  cxplt3  16172  logsqrt  16175  apcxp2  16191  rpabscxpbnd  16192  rplogbid1  16200  rplogb1  16201  rpelogb  16202  rplogbchbase  16203  rplogbreexp  16206  rprelogbmul  16208  rprelogbdiv  16210  rplogbcxp  16216  rpcxplogb  16217  logbgcd1irraplemexp  16221  logbgcd1irraplemap  16222  zprmlogbaplem2  16233  log2tlbndlog2  16237  log2ublem2  16239  birthdaylem2  16243  birthdaylem3  16244  pellexlem2  16247  efnnfsumcl  16256  chtprm  16278  chtdif  16281  efchtqdvds  16282  prmorcht  16299  ppiqub  16310  chtqleppi  16311  chtublem  16312  chtqub  16313  mersenne  16314  bcmax  16322  bcp1ctr  16323  bposlem1  16328  bposlem9  16336  lgsvalmod  16360  lgsdilem  16368  lgsne0  16379  gausslemma2dlem1a  16399  gausslemma2dlem6  16408  lgseisenlem1  16411  lgseisenlem2  16412  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  2sqlem1  16455  mul2sq  16457  2sqlem3  16458  2sqlem8  16464  dichmul0orlem1  16975  dichmul0orlem4  16978  dichmul0orlem5  16979  dichmul0orlem6  16980  dichmul0orlem7  16981  qdencn  17295  refeq  17296  repiecele0  17298  repiecege0  17299  cvgcmp2nlemabs  17304  cvgcmp2n  17305  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  trirec0  17317  apdifflemf  17319  apdifflemr  17320  apdiff  17321  qdiff  17322  redc0  17331  reap0  17332  cndcap  17333  nconstwlpolem0  17337  nconstwlpolemgt0  17338  neap0mkv  17343  ltlenmkv  17344