Theorem recnd 8101

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

Syntax hints:   -> wi 4   e. wcel 2176   CCcc 7923   RRcr 7924

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-resscn 8017

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  readdcan  8212  ltadd2  8492  ltadd1  8502  leadd2  8504  ltsubadd  8505  ltsubadd2  8506  lesubadd  8507  lesubadd2  8508  ltaddsub  8509  leaddsub  8511  lesub1  8529  lesub2  8530  ltsub1  8531  ltsub2  8532  ltnegcon1  8536  ltnegcon2  8537  add20  8547  subge0  8548  suble0  8549  lesub0  8552  eqord2  8557  possumd  8642  sublt0d  8643  rimul  8658  rereim  8659  apreap  8660  ltmul1a  8664  ltmul1  8665  reapmul1  8668  remulext2  8673  cru  8675  apreim  8676  mulreim  8677  apadd1  8681  apneg  8684  mulext1  8685  ltapd  8711  aprcl  8719  aptap  8723  rerecclap  8803  redivclap  8804  recgt0  8923  prodgt0gt0  8924  prodgt0  8925  prodge0  8927  lemul1a  8931  ltdiv1  8941  ltmuldiv  8947  ledivmul  8950  lt2mul2div  8952  ltrec  8956  lt2msq  8959  ltdiv2  8960  ltrec1  8961  lerec2  8962  ledivdiv  8963  lediv2  8964  ltdiv23  8965  lediv23  8966  lediv12a  8967  recp1lt1  8972  recreclt  8973  ledivp1  8976  mulle0r  9017  negiso  9028  avglt1  9276  avglt2  9277  div4p1lem1div2  9291  nn0cnd  9350  zcn  9377  peano2z  9408  zaddcllemneg  9411  ztri3or  9415  zeo  9478  zcnd  9496  eluzelcn  9659  infrenegsupex  9715  supinfneg  9716  infsupneg  9717  supminfex  9718  irrmulap  9769  cnref1o  9772  rpcn  9784  rpcnd  9820  ltaddrp2d  9853  mul2lt0rlt0  9881  mul2lt0rgt0  9882  mul2lt0llt0  9883  mul2lt0lgt0  9884  mul2lt0np  9885  mul2lt0pn  9886  xpncan  9993  icoshftf1o  10113  lincmb01cmp  10125  iccf1o  10126  infssuzcldc  10378  qbtwnrelemcalc  10398  flhalf  10445  intfracq  10465  flqdiv  10466  modqid  10494  modqid0  10495  mulqaddmodid  10509  seqf1oglem1  10664  ser3le  10682  expcl2lemap  10696  expnegzap  10718  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  ltexp2a  10736  leexp2a  10737  leexp2r  10738  exple1  10740  expubnd  10741  sq11  10757  bernneq2  10806  expnbnd  10808  nn0ltexp2  10854  nn0opthlem2d  10866  faclbnd  10886  bcp1nk  10907  remim  11171  reim0b  11173  rereb  11174  mulreap  11175  cjreb  11177  recj  11178  reneg  11179  readd  11180  resub  11181  remullem  11182  remul2  11184  redivap  11185  imcj  11186  imneg  11187  imadd  11188  imsub  11189  immul2  11191  imdivap  11192  cjcj  11194  cjadd  11195  ipcnval  11197  cjmulval  11199  cjneg  11201  imval2  11205  cjreim2  11215  cjap  11217  cnrecnv  11221  caucvgrelemrec  11290  cvg1nlemres  11296  recvguniqlem  11305  recvguniq  11306  resqrexlemover  11321  resqrexlemcalc1  11325  resqrexlemcalc2  11326  resqrexlemcalc3  11327  resqrexlemnmsq  11328  resqrexlemnm  11329  resqrexlemgt0  11331  resqrexlemoverl  11332  resqrexlemglsq  11333  remsqsqrt  11343  sqrtmul  11346  sqrtdiv  11353  sqrtmsq  11356  abs00ap  11373  absext  11374  abs00  11375  absdivap  11381  absid  11382  absexp  11390  absexpzap  11391  absimle  11395  abslt  11399  absle  11400  abssubap0  11401  abssubne0  11402  releabs  11407  recvalap  11408  abstri  11415  abs2difabs  11419  amgm2  11429  icodiamlt  11491  maxabsle  11515  maxabslemab  11517  maxabslemlub  11518  maxabslemval  11519  maxcl  11521  maxltsup  11529  max0addsup  11530  minmax  11541  minabs  11547  minclpr  11548  bdtrilem  11550  bdtri  11551  mul0inf  11552  mingeb  11553  climabs0  11618  reccn2ap  11624  climrecl  11635  climge0  11636  climle  11645  climsqz  11646  climsqz2  11647  climlec2  11652  climrecvg1n  11659  climcvg1nlem  11660  isumrecl  11740  isumge0  11741  fsumlessfi  11771  fsumge1  11772  fsum00  11773  fsumle  11774  fsumlt  11775  fsumabs  11776  iserabs  11786  isumrpcl  11805  isumle  11806  isumlessdc  11807  trireciplem  11811  trirecip  11812  expcnvre  11814  expcnv  11815  explecnv  11816  absltap  11820  geo2sum  11825  cvgratnnlembern  11834  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  cvgratnnlemabsle  11838  cvgratnnlemsumlt  11839  cvgratnnlemfm  11840  cvgratnnlemrate  11841  cvgratz  11843  mertenslemi1  11846  mertenslem2  11847  fprodabs  11927  fprodle  11951  efcllemp  11969  ege2le3  11982  efaddlem  11985  efgt0  11995  reeftlcl  12000  eftlub  12001  effsumlt  12003  efltim  12009  eflegeo  12012  resin4p  12029  recos4p  12030  efeul  12045  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  sin01gt0  12073  cos01gt0  12074  sin02gt0  12075  cos12dec  12079  absefi  12080  absef  12081  absefib  12082  efieq1re  12083  eirraplem  12088  dvdsaddre2b  12152  dvdslelemd  12154  odd2np1  12184  divalglemnqt  12231  bitsp1o  12264  bitsfzo  12266  bitscmp  12269  nn0seqcvgd  12363  sqnprm  12458  isprm5lem  12463  odzdvds  12568  pythagtriplem14  12600  pcid  12647  fldivp1  12671  pockthlem  12679  4sqlem5  12705  4sqlem10  12710  mul4sqlem  12716  4sqlem15  12728  4sqlem16  12729  mulgneg  13476  ghmmulg  13592  rege0subm  14346  metrtri  14849  bl2in  14875  blhalf  14880  blssps  14899  blss  14900  maxcncf  15087  mincncf  15088  dedekindeu  15095  dedekindicclemicc  15104  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthinc  15115  ivthdec  15116  ivthreinc  15117  dvconstre  15168  dvidre  15169  dvcjbr  15180  dvfre  15182  dveflem  15198  plyrecj  15235  reeff1olem  15243  reeff1oleme  15244  eflt  15247  sin0pilem1  15253  sin0pilem2  15254  pilem3  15255  sincosq2sgn  15299  sincosq3sgn  15300  sincosq4sgn  15301  sinq12gt0  15302  sinq34lt0t  15303  cosq14gt0  15304  cosq23lt0  15305  coseq0q4123  15306  coseq0negpitopi  15308  tanrpcl  15309  tangtx  15310  coskpi  15320  cosordlem  15321  cosq34lt1  15322  cos11  15325  reexplog  15343  relogexp  15344  logdivlti  15353  rpcxpef  15366  rpcncxpcl  15374  cxpap0  15376  rpcxpadd  15377  rpmulcxp  15381  cxpmul  15384  abscxp  15387  cxplt  15388  cxplt3  15392  logsqrt  15395  apcxp2  15411  rpabscxpbnd  15412  rplogbid1  15419  rplogb1  15420  rpelogb  15421  rplogbchbase  15422  rplogbreexp  15425  rprelogbmul  15427  rprelogbdiv  15429  rplogbcxp  15435  rpcxplogb  15436  logbgcd1irraplemexp  15440  logbgcd1irraplemap  15441  mersenne  15469  lgsvalmod  15496  lgsdilem  15504  lgsne0  15515  gausslemma2dlem1a  15535  gausslemma2dlem6  15544  lgseisenlem1  15547  lgseisenlem2  15548  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  2sqlem1  15591  mul2sq  15593  2sqlem3  15594  2sqlem8  15600  qdencn  15966  refeq  15967  cvgcmp2nlemabs  15971  cvgcmp2n  15972  trilpolemisumle  15977  trilpolemeq1  15979  trilpolemlt1  15980  trirec0  15983  apdifflemf  15985  apdifflemr  15986  apdiff  15987  redc0  15996  reap0  15997  cndcap  15998  nconstwlpolem0  16002  nconstwlpolemgt0  16003  neap0mkv  16008  ltlenmkv  16009