Theorem recnd 7986

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

Syntax hints:   -> wi 4   e. wcel 2148   CCcc 7809   RRcr 7810

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-resscn 7903

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  readdcan  8097  ltadd2  8376  ltadd1  8386  leadd2  8388  ltsubadd  8389  ltsubadd2  8390  lesubadd  8391  lesubadd2  8392  ltaddsub  8393  leaddsub  8395  lesub1  8413  lesub2  8414  ltsub1  8415  ltsub2  8416  ltnegcon1  8420  ltnegcon2  8421  add20  8431  subge0  8432  suble0  8433  lesub0  8436  eqord2  8441  possumd  8526  sublt0d  8527  rimul  8542  rereim  8543  apreap  8544  ltmul1a  8548  ltmul1  8549  reapmul1  8552  remulext2  8557  cru  8559  apreim  8560  mulreim  8561  apadd1  8565  apneg  8568  mulext1  8569  ltapd  8595  aprcl  8603  aptap  8607  rerecclap  8687  redivclap  8688  recgt0  8807  prodgt0gt0  8808  prodgt0  8809  prodge0  8811  lemul1a  8815  ltdiv1  8825  ltmuldiv  8831  ledivmul  8834  lt2mul2div  8836  ltrec  8840  lt2msq  8843  ltdiv2  8844  ltrec1  8845  lerec2  8846  ledivdiv  8847  lediv2  8848  ltdiv23  8849  lediv23  8850  lediv12a  8851  recp1lt1  8856  recreclt  8857  ledivp1  8860  mulle0r  8901  negiso  8912  avglt1  9157  avglt2  9158  div4p1lem1div2  9172  nn0cnd  9231  zcn  9258  peano2z  9289  zaddcllemneg  9292  ztri3or  9296  zeo  9358  zcnd  9376  eluzelcn  9539  infrenegsupex  9594  supinfneg  9595  infsupneg  9596  supminfex  9597  cnref1o  9650  rpcn  9662  rpcnd  9698  ltaddrp2d  9731  mul2lt0rlt0  9759  mul2lt0rgt0  9760  mul2lt0llt0  9761  mul2lt0lgt0  9762  mul2lt0np  9763  mul2lt0pn  9764  xpncan  9871  icoshftf1o  9991  lincmb01cmp  10003  iccf1o  10004  qbtwnrelemcalc  10256  flhalf  10302  intfracq  10320  flqdiv  10321  modqid  10349  modqid0  10350  mulqaddmodid  10364  ser3le  10518  expcl2lemap  10532  expnegzap  10554  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  ltexp2a  10572  leexp2a  10573  leexp2r  10574  exple1  10576  expubnd  10577  sq11  10593  bernneq2  10642  expnbnd  10644  nn0ltexp2  10689  nn0opthlem2d  10701  faclbnd  10721  bcp1nk  10742  remim  10869  reim0b  10871  rereb  10872  mulreap  10873  cjreb  10875  recj  10876  reneg  10877  readd  10878  resub  10879  remullem  10880  remul2  10882  redivap  10883  imcj  10884  imneg  10885  imadd  10886  imsub  10887  immul2  10889  imdivap  10890  cjcj  10892  cjadd  10893  ipcnval  10895  cjmulval  10897  cjneg  10899  imval2  10903  cjreim2  10913  cjap  10915  cnrecnv  10919  caucvgrelemrec  10988  cvg1nlemres  10994  recvguniqlem  11003  recvguniq  11004  resqrexlemover  11019  resqrexlemcalc1  11023  resqrexlemcalc2  11024  resqrexlemcalc3  11025  resqrexlemnmsq  11026  resqrexlemnm  11027  resqrexlemgt0  11029  resqrexlemoverl  11030  resqrexlemglsq  11031  remsqsqrt  11041  sqrtmul  11044  sqrtdiv  11051  sqrtmsq  11054  abs00ap  11071  absext  11072  abs00  11073  absdivap  11079  absid  11080  absexp  11088  absexpzap  11089  absimle  11093  abslt  11097  absle  11098  abssubap0  11099  abssubne0  11100  releabs  11105  recvalap  11106  abstri  11113  abs2difabs  11117  amgm2  11127  icodiamlt  11189  maxabsle  11213  maxabslemab  11215  maxabslemlub  11216  maxabslemval  11217  maxcl  11219  maxltsup  11227  max0addsup  11228  minmax  11238  minabs  11244  minclpr  11245  bdtrilem  11247  bdtri  11248  mul0inf  11249  mingeb  11250  climabs0  11315  reccn2ap  11321  climrecl  11332  climge0  11333  climle  11342  climsqz  11343  climsqz2  11344  climlec2  11349  climrecvg1n  11356  climcvg1nlem  11357  isumrecl  11437  isumge0  11438  fsumlessfi  11468  fsumge1  11469  fsum00  11470  fsumle  11471  fsumlt  11472  fsumabs  11473  iserabs  11483  isumrpcl  11502  isumle  11503  isumlessdc  11504  trireciplem  11508  trirecip  11509  expcnvre  11511  expcnv  11512  explecnv  11513  absltap  11517  geo2sum  11522  cvgratnnlembern  11531  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratnnlemabsle  11535  cvgratnnlemsumlt  11536  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratz  11540  mertenslemi1  11543  mertenslem2  11544  fprodabs  11624  fprodle  11648  efcllemp  11666  ege2le3  11679  efaddlem  11682  efgt0  11692  reeftlcl  11697  eftlub  11698  effsumlt  11700  efltim  11706  eflegeo  11709  resin4p  11726  recos4p  11727  efeul  11742  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  cos12dec  11775  absefi  11776  absef  11777  absefib  11778  efieq1re  11779  eirraplem  11784  dvdsaddre2b  11848  dvdslelemd  11849  odd2np1  11878  divalglemnqt  11925  infssuzcldc  11952  nn0seqcvgd  12041  sqnprm  12136  isprm5lem  12141  odzdvds  12245  pythagtriplem14  12277  pcid  12323  fldivp1  12346  pockthlem  12354  4sqlem5  12380  4sqlem10  12385  mul4sqlem  12391  mulgneg  13001  rege0subm  13481  metrtri  13880  bl2in  13906  blhalf  13911  blssps  13930  blss  13931  dedekindeu  14104  dedekindicclemicc  14113  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthinc  14124  ivthdec  14125  dvcjbr  14175  dvfre  14177  dveflem  14190  reeff1olem  14195  reeff1oleme  14196  eflt  14199  sin0pilem1  14205  sin0pilem2  14206  pilem3  14207  sincosq2sgn  14251  sincosq3sgn  14252  sincosq4sgn  14253  sinq12gt0  14254  sinq34lt0t  14255  cosq14gt0  14256  cosq23lt0  14257  coseq0q4123  14258  coseq0negpitopi  14260  tanrpcl  14261  tangtx  14262  coskpi  14272  cosordlem  14273  cosq34lt1  14274  cos11  14277  reexplog  14295  relogexp  14296  logdivlti  14305  rpcxpef  14318  rpcncxpcl  14326  cxpap0  14328  rpcxpadd  14329  rpmulcxp  14333  cxpmul  14336  abscxp  14338  cxplt  14339  cxplt3  14343  logsqrt  14346  apcxp2  14361  rpabscxpbnd  14362  rplogbid1  14368  rplogb1  14369  rpelogb  14370  rplogbchbase  14371  rplogbreexp  14374  rprelogbmul  14376  rprelogbdiv  14378  rplogbcxp  14384  rpcxplogb  14385  logbgcd1irraplemexp  14389  logbgcd1irraplemap  14390  lgsvalmod  14423  lgsdilem  14431  lgsne0  14442  lgseisenlem1  14453  lgseisenlem2  14454  2sqlem1  14464  mul2sq  14466  2sqlem3  14467  2sqlem8  14473  qdencn  14778  refeq  14779  cvgcmp2nlemabs  14783  cvgcmp2n  14784  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  trirec0  14795  apdifflemf  14797  apdifflemr  14798  apdiff  14799  redc0  14808  reap0  14809  nconstwlpolem0  14813  nconstwlpolemgt0  14814  neap0mkv  14819  ltlenmkv  14820