Theorem recnd 8344

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

Syntax hints:   -> wi 4   e. wcel 2209   CCcc 8167   RRcr 8168

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 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 8261

This theorem 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 referenced by:  readdcan  8456  ltadd2  8737  ltadd1  8747  leadd2  8749  ltsubadd  8750  ltsubadd2  8751  lesubadd  8752  lesubadd2  8753  ltaddsub  8754  leaddsub  8756  lesub1  8774  lesub2  8775  ltsub1  8776  ltsub2  8777  ltnegcon1  8781  ltnegcon2  8782  add20  8792  subge0  8793  suble0  8794  lesub0  8797  eqord2  8802  possumd  8887  sublt0d  8888  rimul  8903  rereim  8904  apreap  8905  ltmul1a  8909  ltmul1  8910  reapmul1  8913  remulext2  8918  cru  8920  apreim  8921  mulreim  8922  apadd1  8926  apneg  8929  mulext1  8930  ltapd  8956  aprcl  8964  aptap  8968  rerecclap  9050  redivclap  9051  recgt0  9170  prodgt0gt0  9171  prodgt0  9172  prodge0  9174  lemul1a  9178  ltdiv1  9188  ltmuldiv  9194  ledivmul  9197  lt2mul2div  9199  ltrec  9203  lt2msq  9206  ltdiv2  9207  ltrec1  9208  lerec2  9209  ledivdiv  9210  lediv2  9211  ltdiv23  9212  lediv23  9213  lediv12a  9214  recp1lt1  9219  recreclt  9220  ledivp1  9223  mulle0r  9264  negiso  9275  avglt1  9523  avglt2  9524  div4p1lem1div2  9538  nn0cnd  9601  zcn  9628  peano2z  9659  zaddcllemneg  9662  ztri3or  9666  zeo  9730  zcnd  9748  eluzmn  9907  eluzelcn  9912  infrenegsupex  9973  supinfneg  9974  infsupneg  9975  supminfex  9976  irrmulap  10027  cnref1o  10030  rpcn  10042  rpcnd  10078  ltaddrp2d  10111  mul2lt0rlt0  10139  mul2lt0rgt0  10140  mul2lt0llt0  10141  mul2lt0lgt0  10142  mul2lt0np  10143  mul2lt0pn  10144  xpncan  10252  icoshftf1o  10372  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  infssuzcldc  10646  qbtwnrelemcalc  10668  flhalf  10715  intfracq  10735  flqdiv  10736  modqid  10764  modqid0  10765  mulqaddmodid  10779  seqf1oglem1  10934  ser3le  10952  expcl2lemap  10966  expnegzap  10988  expaddzaplem  10997  expaddzap  10998  expmulzap  11000  ltexp2a  11006  leexp2a  11007  leexp2r  11008  exple1  11010  expubnd  11011  sq11  11027  resq01  11073  bernneq2  11077  expnbnd  11079  nn0ltexp2  11125  nn0opthlem2d  11137  faclbnd  11157  bcp1nk  11178  bcm1n  11185  remim  11603  reim0b  11605  rereb  11606  mulreap  11607  cjreb  11609  recj  11610  reneg  11611  readd  11612  resub  11613  remullem  11614  remul2  11616  redivap  11617  imcj  11618  imneg  11619  imadd  11620  imsub  11621  immul2  11623  imdivap  11624  cjcj  11626  cjadd  11627  ipcnval  11629  cjmulval  11631  cjneg  11633  imval2  11637  sq01  11638  cjreim2  11648  cjap  11650  cnrecnv  11654  caucvgrelemrec  11723  cvg1nlemres  11729  recvguniqlem  11738  recvguniq  11739  resqrexlemover  11754  resqrexlemcalc1  11758  resqrexlemcalc2  11759  resqrexlemcalc3  11760  resqrexlemnmsq  11761  resqrexlemnm  11762  resqrexlemgt0  11764  resqrexlemoverl  11765  resqrexlemglsq  11766  remsqsqrt  11776  sqrtmul  11779  sqrtdiv  11786  sqrtmsq  11789  abs00ap  11806  absext  11807  abs00  11808  absdivap  11814  absid  11815  absexp  11823  absexpzap  11824  absimle  11828  abslt  11832  absle  11833  abssubap0  11834  abssubne0  11835  releabs  11840  recvalap  11841  abstri  11848  abs2difabs  11852  amgm2  11862  icodiamlt  11924  maxabsle  11948  maxabslemab  11950  maxabslemlub  11951  maxabslemval  11952  maxcl  11954  maxltsup  11962  max0addsup  11963  minmax  11974  minabs  11980  minclpr  11981  bdtrilem  11983  bdtri  11984  mul0inf  11985  mingeb  11986  climabs0  12051  reccn2ap  12057  climrecl  12068  climge0  12069  climle  12078  climsqz  12079  climsqz2  12080  climlec2  12085  climrecvg1n  12092  climcvg1nlem  12093  isumrecl  12174  isumge0  12175  fsumlessfi  12205  fsumge1  12206  fsum00  12207  fsumle  12208  fsumlt  12209  fsumabs  12210  iserabs  12220  isumrpcl  12239  isumle  12240  isumlessdc  12241  trireciplem  12245  trirecip  12246  expcnvre  12248  expcnv  12249  explecnv  12250  absltap  12254  geo2sum  12259  cvgratnnlembern  12268  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  cvgratnnlemabsle  12272  cvgratnnlemsumlt  12273  cvgratnnlemfm  12274  cvgratnnlemrate  12275  cvgratz  12277  mertenslemi1  12280  mertenslem2  12281  fprodabs  12361  fprodle  12385  efcllemp  12403  ege2le3  12416  efaddlem  12419  efgt0  12429  reeftlcl  12434  eftlub  12435  effsumlt  12437  efltim  12443  eflegeo  12446  resin4p  12463  recos4p  12464  efeul  12479  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  cos12dec  12513  absefi  12514  absef  12515  absefib  12516  efieq1re  12517  eirraplem  12522  dvdsaddre2b  12586  dvdslelemd  12588  odd2np1  12618  divalglemnqt  12665  bitsp1o  12698  bitsfzo  12700  bitscmp  12703  nn0seqcvgd  12797  sqnprm  12892  isprm5lem  12897  odzdvds  13002  pythagtriplem14  13034  pcid  13081  fldivp1  13105  pockthlem  13113  4sqlem5  13139  4sqlem10  13144  mul4sqlem  13150  4sqlem15  13162  4sqlem16  13163  ballotfilemsi  13236  mulgneg  13920  ghmmulg  14036  rege0subm  14893  metrtri  15401  bl2in  15427  blhalf  15432  blssps  15451  blss  15452  maxcncf  15639  mincncf  15640  dedekindeu  15647  dedekindicclemicc  15656  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthinc  15667  ivthdec  15668  ivthreinc  15669  dvconstre  15720  dvidre  15721  dvcjbr  15732  dvfre  15734  dveflem  15750  plyrecj  15787  reeff1olem  15795  reeff1oleme  15796  eflt  15799  sin0pilem1  15805  sin0pilem2  15806  pilem3  15807  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  sinq34lt0t  15855  cosq14gt0  15856  cosq23lt0  15857  coseq0q4123  15858  coseq0negpitopi  15860  tanrpcl  15861  tangtx  15862  coskpi  15872  cosordlem  15873  cosq34lt1  15874  cos11  15877  reexplog  15895  relogexp  15896  logdivlti  15905  logfac  15918  rpcxpef  15919  rpcncxpcl  15927  cxpap0  15929  rpcxpadd  15930  rpmulcxp  15934  cxpmul  15937  abscxp  15940  cxplt  15941  cxplt3  15945  logsqrt  15948  apcxp2  15964  rpabscxpbnd  15965  rplogbid1  15972  rplogb1  15973  rpelogb  15974  rplogbchbase  15975  rplogbreexp  15978  rprelogbmul  15980  rprelogbdiv  15982  rplogbcxp  15988  rpcxplogb  15989  logbgcd1irraplemexp  15993  logbgcd1irraplemap  15994  pellexlem2  16006  mersenne  16025  lgsvalmod  16052  lgsdilem  16060  lgsne0  16071  gausslemma2dlem1a  16091  gausslemma2dlem6  16100  lgseisenlem1  16103  lgseisenlem2  16104  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  2sqlem1  16147  mul2sq  16149  2sqlem3  16150  2sqlem8  16156  dichmul0orlem1  16667  dichmul0orlem4  16670  dichmul0orlem5  16671  dichmul0orlem6  16672  dichmul0orlem7  16673  qdencn  16977  refeq  16978  repiecele0  16980  repiecege0  16981  cvgcmp2nlemabs  16986  cvgcmp2n  16987  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  trirec0  16998  apdifflemf  17000  apdifflemr  17001  apdiff  17002  qdiff  17003  redc0  17012  reap0  17013  cndcap  17014  nconstwlpolem0  17018  nconstwlpolemgt0  17019  neap0mkv  17024  ltlenmkv  17025