Theorem recnd 8318

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

Syntax hints:   -> wi 4   e. wcel 2205   CCcc 8141   RRcr 8142

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  readdcan  8429  ltadd2  8710  ltadd1  8720  leadd2  8722  ltsubadd  8723  ltsubadd2  8724  lesubadd  8725  lesubadd2  8726  ltaddsub  8727  leaddsub  8729  lesub1  8747  lesub2  8748  ltsub1  8749  ltsub2  8750  ltnegcon1  8754  ltnegcon2  8755  add20  8765  subge0  8766  suble0  8767  lesub0  8770  eqord2  8775  possumd  8860  sublt0d  8861  rimul  8876  rereim  8877  apreap  8878  ltmul1a  8882  ltmul1  8883  reapmul1  8886  remulext2  8891  cru  8893  apreim  8894  mulreim  8895  apadd1  8899  apneg  8902  mulext1  8903  ltapd  8929  aprcl  8937  aptap  8941  rerecclap  9021  redivclap  9022  recgt0  9141  prodgt0gt0  9142  prodgt0  9143  prodge0  9145  lemul1a  9149  ltdiv1  9159  ltmuldiv  9165  ledivmul  9168  lt2mul2div  9170  ltrec  9174  lt2msq  9177  ltdiv2  9178  ltrec1  9179  lerec2  9180  ledivdiv  9181  lediv2  9182  ltdiv23  9183  lediv23  9184  lediv12a  9185  recp1lt1  9190  recreclt  9191  ledivp1  9194  mulle0r  9235  negiso  9246  avglt1  9494  avglt2  9495  div4p1lem1div2  9509  nn0cnd  9572  zcn  9599  peano2z  9630  zaddcllemneg  9633  ztri3or  9637  zeo  9701  zcnd  9719  eluzmn  9878  eluzelcn  9883  infrenegsupex  9944  supinfneg  9945  infsupneg  9946  supminfex  9947  irrmulap  9998  cnref1o  10001  rpcn  10013  rpcnd  10049  ltaddrp2d  10082  mul2lt0rlt0  10110  mul2lt0rgt0  10111  mul2lt0llt0  10112  mul2lt0lgt0  10113  mul2lt0np  10114  mul2lt0pn  10115  xpncan  10223  icoshftf1o  10343  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  infssuzcldc  10617  qbtwnrelemcalc  10639  flhalf  10686  intfracq  10706  flqdiv  10707  modqid  10735  modqid0  10736  mulqaddmodid  10750  seqf1oglem1  10905  ser3le  10923  expcl2lemap  10937  expnegzap  10959  expaddzaplem  10968  expaddzap  10969  expmulzap  10971  ltexp2a  10977  leexp2a  10978  leexp2r  10979  exple1  10981  expubnd  10982  sq11  10998  resq01  11044  bernneq2  11048  expnbnd  11050  nn0ltexp2  11096  nn0opthlem2d  11108  faclbnd  11128  bcp1nk  11149  bcm1n  11156  remim  11570  reim0b  11572  rereb  11573  mulreap  11574  cjreb  11576  recj  11577  reneg  11578  readd  11579  resub  11580  remullem  11581  remul2  11583  redivap  11584  imcj  11585  imneg  11586  imadd  11587  imsub  11588  immul2  11590  imdivap  11591  cjcj  11593  cjadd  11594  ipcnval  11596  cjmulval  11598  cjneg  11600  imval2  11604  cjreim2  11614  cjap  11616  cnrecnv  11620  caucvgrelemrec  11689  cvg1nlemres  11695  recvguniqlem  11704  recvguniq  11705  resqrexlemover  11720  resqrexlemcalc1  11724  resqrexlemcalc2  11725  resqrexlemcalc3  11726  resqrexlemnmsq  11727  resqrexlemnm  11728  resqrexlemgt0  11730  resqrexlemoverl  11731  resqrexlemglsq  11732  remsqsqrt  11742  sqrtmul  11745  sqrtdiv  11752  sqrtmsq  11755  abs00ap  11772  absext  11773  abs00  11774  absdivap  11780  absid  11781  absexp  11789  absexpzap  11790  absimle  11794  abslt  11798  absle  11799  abssubap0  11800  abssubne0  11801  releabs  11806  recvalap  11807  abstri  11814  abs2difabs  11818  amgm2  11828  icodiamlt  11890  maxabsle  11914  maxabslemab  11916  maxabslemlub  11917  maxabslemval  11918  maxcl  11920  maxltsup  11928  max0addsup  11929  minmax  11940  minabs  11946  minclpr  11947  bdtrilem  11949  bdtri  11950  mul0inf  11951  mingeb  11952  climabs0  12017  reccn2ap  12023  climrecl  12034  climge0  12035  climle  12044  climsqz  12045  climsqz2  12046  climlec2  12051  climrecvg1n  12058  climcvg1nlem  12059  isumrecl  12140  isumge0  12141  fsumlessfi  12171  fsumge1  12172  fsum00  12173  fsumle  12174  fsumlt  12175  fsumabs  12176  iserabs  12186  isumrpcl  12205  isumle  12206  isumlessdc  12207  trireciplem  12211  trirecip  12212  expcnvre  12214  expcnv  12215  explecnv  12216  absltap  12220  geo2sum  12225  cvgratnnlembern  12234  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  cvgratnnlemabsle  12238  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  fprodabs  12327  fprodle  12351  efcllemp  12369  ege2le3  12382  efaddlem  12385  efgt0  12395  reeftlcl  12400  eftlub  12401  effsumlt  12403  efltim  12409  eflegeo  12412  resin4p  12429  recos4p  12430  efeul  12445  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  cos12dec  12479  absefi  12480  absef  12481  absefib  12482  efieq1re  12483  eirraplem  12488  dvdsaddre2b  12552  dvdslelemd  12554  odd2np1  12584  divalglemnqt  12631  bitsp1o  12664  bitsfzo  12666  bitscmp  12669  nn0seqcvgd  12763  sqnprm  12858  isprm5lem  12863  odzdvds  12968  pythagtriplem14  13000  pcid  13047  fldivp1  13071  pockthlem  13079  4sqlem5  13105  4sqlem10  13110  mul4sqlem  13116  4sqlem15  13128  4sqlem16  13129  ballotfilemsi  13202  mulgneg  13893  ghmmulg  14009  rege0subm  14858  metrtri  15368  bl2in  15394  blhalf  15399  blssps  15418  blss  15419  maxcncf  15606  mincncf  15607  dedekindeu  15614  dedekindicclemicc  15623  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthinc  15634  ivthdec  15635  ivthreinc  15636  dvconstre  15687  dvidre  15688  dvcjbr  15699  dvfre  15701  dveflem  15717  plyrecj  15754  reeff1olem  15762  reeff1oleme  15763  eflt  15766  sin0pilem1  15772  sin0pilem2  15773  pilem3  15774  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  sinq34lt0t  15822  cosq14gt0  15823  cosq23lt0  15824  coseq0q4123  15825  coseq0negpitopi  15827  tanrpcl  15828  tangtx  15829  coskpi  15839  cosordlem  15840  cosq34lt1  15841  cos11  15844  reexplog  15862  relogexp  15863  logdivlti  15872  rpcxpef  15885  rpcncxpcl  15893  cxpap0  15895  rpcxpadd  15896  rpmulcxp  15900  cxpmul  15903  abscxp  15906  cxplt  15907  cxplt3  15911  logsqrt  15914  apcxp2  15930  rpabscxpbnd  15931  rplogbid1  15938  rplogb1  15939  rpelogb  15940  rplogbchbase  15941  rplogbreexp  15944  rprelogbmul  15946  rprelogbdiv  15948  rplogbcxp  15954  rpcxplogb  15955  logbgcd1irraplemexp  15959  logbgcd1irraplemap  15960  pellexlem2  15972  mersenne  15991  lgsvalmod  16018  lgsdilem  16026  lgsne0  16037  gausslemma2dlem1a  16057  gausslemma2dlem6  16066  lgseisenlem1  16069  lgseisenlem2  16070  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  2sqlem1  16113  mul2sq  16115  2sqlem3  16116  2sqlem8  16122  qdencn  16933  refeq  16934  repiecele0  16936  repiecege0  16937  cvgcmp2nlemabs  16942  cvgcmp2n  16943  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  trirec0  16954  apdifflemf  16956  apdifflemr  16957  apdiff  16958  qdiff  16959  redc0  16968  reap0  16969  cndcap  16970  nconstwlpolem0  16975  nconstwlpolemgt0  16976  neap0mkv  16981  ltlenmkv  16982