Theorem recnd 8004

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

Syntax hints:   -> wi 4   e. wcel 2160   CCcc 7827   RRcr 7828

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-resscn 7921

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  readdcan  8115  ltadd2  8394  ltadd1  8404  leadd2  8406  ltsubadd  8407  ltsubadd2  8408  lesubadd  8409  lesubadd2  8410  ltaddsub  8411  leaddsub  8413  lesub1  8431  lesub2  8432  ltsub1  8433  ltsub2  8434  ltnegcon1  8438  ltnegcon2  8439  add20  8449  subge0  8450  suble0  8451  lesub0  8454  eqord2  8459  possumd  8544  sublt0d  8545  rimul  8560  rereim  8561  apreap  8562  ltmul1a  8566  ltmul1  8567  reapmul1  8570  remulext2  8575  cru  8577  apreim  8578  mulreim  8579  apadd1  8583  apneg  8586  mulext1  8587  ltapd  8613  aprcl  8621  aptap  8625  rerecclap  8705  redivclap  8706  recgt0  8825  prodgt0gt0  8826  prodgt0  8827  prodge0  8829  lemul1a  8833  ltdiv1  8843  ltmuldiv  8849  ledivmul  8852  lt2mul2div  8854  ltrec  8858  lt2msq  8861  ltdiv2  8862  ltrec1  8863  lerec2  8864  ledivdiv  8865  lediv2  8866  ltdiv23  8867  lediv23  8868  lediv12a  8869  recp1lt1  8874  recreclt  8875  ledivp1  8878  mulle0r  8919  negiso  8930  avglt1  9175  avglt2  9176  div4p1lem1div2  9190  nn0cnd  9249  zcn  9276  peano2z  9307  zaddcllemneg  9310  ztri3or  9314  zeo  9376  zcnd  9394  eluzelcn  9557  infrenegsupex  9612  supinfneg  9613  infsupneg  9614  supminfex  9615  cnref1o  9668  rpcn  9680  rpcnd  9716  ltaddrp2d  9749  mul2lt0rlt0  9777  mul2lt0rgt0  9778  mul2lt0llt0  9779  mul2lt0lgt0  9780  mul2lt0np  9781  mul2lt0pn  9782  xpncan  9889  icoshftf1o  10009  lincmb01cmp  10021  iccf1o  10022  qbtwnrelemcalc  10274  flhalf  10320  intfracq  10338  flqdiv  10339  modqid  10367  modqid0  10368  mulqaddmodid  10382  ser3le  10536  expcl2lemap  10550  expnegzap  10572  expaddzaplem  10581  expaddzap  10582  expmulzap  10584  ltexp2a  10590  leexp2a  10591  leexp2r  10592  exple1  10594  expubnd  10595  sq11  10611  bernneq2  10660  expnbnd  10662  nn0ltexp2  10707  nn0opthlem2d  10719  faclbnd  10739  bcp1nk  10760  remim  10887  reim0b  10889  rereb  10890  mulreap  10891  cjreb  10893  recj  10894  reneg  10895  readd  10896  resub  10897  remullem  10898  remul2  10900  redivap  10901  imcj  10902  imneg  10903  imadd  10904  imsub  10905  immul2  10907  imdivap  10908  cjcj  10910  cjadd  10911  ipcnval  10913  cjmulval  10915  cjneg  10917  imval2  10921  cjreim2  10931  cjap  10933  cnrecnv  10937  caucvgrelemrec  11006  cvg1nlemres  11012  recvguniqlem  11021  recvguniq  11022  resqrexlemover  11037  resqrexlemcalc1  11041  resqrexlemcalc2  11042  resqrexlemcalc3  11043  resqrexlemnmsq  11044  resqrexlemnm  11045  resqrexlemgt0  11047  resqrexlemoverl  11048  resqrexlemglsq  11049  remsqsqrt  11059  sqrtmul  11062  sqrtdiv  11069  sqrtmsq  11072  abs00ap  11089  absext  11090  abs00  11091  absdivap  11097  absid  11098  absexp  11106  absexpzap  11107  absimle  11111  abslt  11115  absle  11116  abssubap0  11117  abssubne0  11118  releabs  11123  recvalap  11124  abstri  11131  abs2difabs  11135  amgm2  11145  icodiamlt  11207  maxabsle  11231  maxabslemab  11233  maxabslemlub  11234  maxabslemval  11235  maxcl  11237  maxltsup  11245  max0addsup  11246  minmax  11256  minabs  11262  minclpr  11263  bdtrilem  11265  bdtri  11266  mul0inf  11267  mingeb  11268  climabs0  11333  reccn2ap  11339  climrecl  11350  climge0  11351  climle  11360  climsqz  11361  climsqz2  11362  climlec2  11367  climrecvg1n  11374  climcvg1nlem  11375  isumrecl  11455  isumge0  11456  fsumlessfi  11486  fsumge1  11487  fsum00  11488  fsumle  11489  fsumlt  11490  fsumabs  11491  iserabs  11501  isumrpcl  11520  isumle  11521  isumlessdc  11522  trireciplem  11526  trirecip  11527  expcnvre  11529  expcnv  11530  explecnv  11531  absltap  11535  geo2sum  11540  cvgratnnlembern  11549  cvgratnnlemnexp  11550  cvgratnnlemmn  11551  cvgratnnlemabsle  11553  cvgratnnlemsumlt  11554  cvgratnnlemfm  11555  cvgratnnlemrate  11556  cvgratz  11558  mertenslemi1  11561  mertenslem2  11562  fprodabs  11642  fprodle  11666  efcllemp  11684  ege2le3  11697  efaddlem  11700  efgt0  11710  reeftlcl  11715  eftlub  11716  effsumlt  11718  efltim  11724  eflegeo  11727  resin4p  11744  recos4p  11745  efeul  11760  ef01bndlem  11782  sin01bnd  11783  cos01bnd  11784  sin01gt0  11787  cos01gt0  11788  sin02gt0  11789  cos12dec  11793  absefi  11794  absef  11795  absefib  11796  efieq1re  11797  eirraplem  11802  dvdsaddre2b  11866  dvdslelemd  11867  odd2np1  11896  divalglemnqt  11943  infssuzcldc  11970  nn0seqcvgd  12059  sqnprm  12154  isprm5lem  12159  odzdvds  12263  pythagtriplem14  12295  pcid  12341  fldivp1  12364  pockthlem  12372  4sqlem5  12398  4sqlem10  12403  mul4sqlem  12409  mulgneg  13046  ghmmulg  13156  rege0subm  13848  metrtri  14274  bl2in  14300  blhalf  14305  blssps  14324  blss  14325  dedekindeu  14498  dedekindicclemicc  14507  ivthinclemlopn  14511  ivthinclemuopn  14513  ivthinc  14518  ivthdec  14519  dvcjbr  14569  dvfre  14571  dveflem  14584  reeff1olem  14589  reeff1oleme  14590  eflt  14593  sin0pilem1  14599  sin0pilem2  14600  pilem3  14601  sincosq2sgn  14645  sincosq3sgn  14646  sincosq4sgn  14647  sinq12gt0  14648  sinq34lt0t  14649  cosq14gt0  14650  cosq23lt0  14651  coseq0q4123  14652  coseq0negpitopi  14654  tanrpcl  14655  tangtx  14656  coskpi  14666  cosordlem  14667  cosq34lt1  14668  cos11  14671  reexplog  14689  relogexp  14690  logdivlti  14699  rpcxpef  14712  rpcncxpcl  14720  cxpap0  14722  rpcxpadd  14723  rpmulcxp  14727  cxpmul  14730  abscxp  14732  cxplt  14733  cxplt3  14737  logsqrt  14740  apcxp2  14755  rpabscxpbnd  14756  rplogbid1  14762  rplogb1  14763  rpelogb  14764  rplogbchbase  14765  rplogbreexp  14768  rprelogbmul  14770  rprelogbdiv  14772  rplogbcxp  14778  rpcxplogb  14779  logbgcd1irraplemexp  14783  logbgcd1irraplemap  14784  lgsvalmod  14817  lgsdilem  14825  lgsne0  14836  lgseisenlem1  14847  lgseisenlem2  14848  2sqlem1  14858  mul2sq  14860  2sqlem3  14861  2sqlem8  14867  qdencn  15173  refeq  15174  cvgcmp2nlemabs  15178  cvgcmp2n  15179  trilpolemisumle  15184  trilpolemeq1  15186  trilpolemlt1  15187  trirec0  15190  apdifflemf  15192  apdifflemr  15193  apdiff  15194  redc0  15203  reap0  15204  cndcap  15205  nconstwlpolem0  15209  nconstwlpolemgt0  15210  neap0mkv  15215  ltlenmkv  15216