Theorem recnd 8250

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

Syntax hints:   -> wi 4   e. wcel 2202   CCcc 8073   RRcr 8074

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 2213  ax-resscn 8167

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  readdcan  8361  ltadd2  8641  ltadd1  8651  leadd2  8653  ltsubadd  8654  ltsubadd2  8655  lesubadd  8656  lesubadd2  8657  ltaddsub  8658  leaddsub  8660  lesub1  8678  lesub2  8679  ltsub1  8680  ltsub2  8681  ltnegcon1  8685  ltnegcon2  8686  add20  8696  subge0  8697  suble0  8698  lesub0  8701  eqord2  8706  possumd  8791  sublt0d  8792  rimul  8807  rereim  8808  apreap  8809  ltmul1a  8813  ltmul1  8814  reapmul1  8817  remulext2  8822  cru  8824  apreim  8825  mulreim  8826  apadd1  8830  apneg  8833  mulext1  8834  ltapd  8860  aprcl  8868  aptap  8872  rerecclap  8952  redivclap  8953  recgt0  9072  prodgt0gt0  9073  prodgt0  9074  prodge0  9076  lemul1a  9080  ltdiv1  9090  ltmuldiv  9096  ledivmul  9099  lt2mul2div  9101  ltrec  9105  lt2msq  9108  ltdiv2  9109  ltrec1  9110  lerec2  9111  ledivdiv  9112  lediv2  9113  ltdiv23  9114  lediv23  9115  lediv12a  9116  recp1lt1  9121  recreclt  9122  ledivp1  9125  mulle0r  9166  negiso  9177  avglt1  9425  avglt2  9426  div4p1lem1div2  9440  nn0cnd  9501  zcn  9528  peano2z  9559  zaddcllemneg  9562  ztri3or  9566  zeo  9629  zcnd  9647  eluzmn  9806  eluzelcn  9811  infrenegsupex  9872  supinfneg  9873  infsupneg  9874  supminfex  9875  irrmulap  9926  cnref1o  9929  rpcn  9941  rpcnd  9977  ltaddrp2d  10010  mul2lt0rlt0  10038  mul2lt0rgt0  10039  mul2lt0llt0  10040  mul2lt0lgt0  10041  mul2lt0np  10042  mul2lt0pn  10043  xpncan  10150  icoshftf1o  10270  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  infssuzcldc  10541  qbtwnrelemcalc  10561  flhalf  10608  intfracq  10628  flqdiv  10629  modqid  10657  modqid0  10658  mulqaddmodid  10672  seqf1oglem1  10827  ser3le  10845  expcl2lemap  10859  expnegzap  10881  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  ltexp2a  10899  leexp2a  10900  leexp2r  10901  exple1  10903  expubnd  10904  sq11  10920  bernneq2  10969  expnbnd  10971  nn0ltexp2  11017  nn0opthlem2d  11029  faclbnd  11049  bcp1nk  11070  remim  11483  reim0b  11485  rereb  11486  mulreap  11487  cjreb  11489  recj  11490  reneg  11491  readd  11492  resub  11493  remullem  11494  remul2  11496  redivap  11497  imcj  11498  imneg  11499  imadd  11500  imsub  11501  immul2  11503  imdivap  11504  cjcj  11506  cjadd  11507  ipcnval  11509  cjmulval  11511  cjneg  11513  imval2  11517  cjreim2  11527  cjap  11529  cnrecnv  11533  caucvgrelemrec  11602  cvg1nlemres  11608  recvguniqlem  11617  recvguniq  11618  resqrexlemover  11633  resqrexlemcalc1  11637  resqrexlemcalc2  11638  resqrexlemcalc3  11639  resqrexlemnmsq  11640  resqrexlemnm  11641  resqrexlemgt0  11643  resqrexlemoverl  11644  resqrexlemglsq  11645  remsqsqrt  11655  sqrtmul  11658  sqrtdiv  11665  sqrtmsq  11668  abs00ap  11685  absext  11686  abs00  11687  absdivap  11693  absid  11694  absexp  11702  absexpzap  11703  absimle  11707  abslt  11711  absle  11712  abssubap0  11713  abssubne0  11714  releabs  11719  recvalap  11720  abstri  11727  abs2difabs  11731  amgm2  11741  icodiamlt  11803  maxabsle  11827  maxabslemab  11829  maxabslemlub  11830  maxabslemval  11831  maxcl  11833  maxltsup  11841  max0addsup  11842  minmax  11853  minabs  11859  minclpr  11860  bdtrilem  11862  bdtri  11863  mul0inf  11864  mingeb  11865  climabs0  11930  reccn2ap  11936  climrecl  11947  climge0  11948  climle  11957  climsqz  11958  climsqz2  11959  climlec2  11964  climrecvg1n  11971  climcvg1nlem  11972  isumrecl  12053  isumge0  12054  fsumlessfi  12084  fsumge1  12085  fsum00  12086  fsumle  12087  fsumlt  12088  fsumabs  12089  iserabs  12099  isumrpcl  12118  isumle  12119  isumlessdc  12120  trireciplem  12124  trirecip  12125  expcnvre  12127  expcnv  12128  explecnv  12129  absltap  12133  geo2sum  12138  cvgratnnlembern  12147  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  cvgratnnlemabsle  12151  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratz  12156  mertenslemi1  12159  mertenslem2  12160  fprodabs  12240  fprodle  12264  efcllemp  12282  ege2le3  12295  efaddlem  12298  efgt0  12308  reeftlcl  12313  eftlub  12314  effsumlt  12316  efltim  12322  eflegeo  12325  resin4p  12342  recos4p  12343  efeul  12358  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  sin01gt0  12386  cos01gt0  12387  sin02gt0  12388  cos12dec  12392  absefi  12393  absef  12394  absefib  12395  efieq1re  12396  eirraplem  12401  dvdsaddre2b  12465  dvdslelemd  12467  odd2np1  12497  divalglemnqt  12544  bitsp1o  12577  bitsfzo  12579  bitscmp  12582  nn0seqcvgd  12676  sqnprm  12771  isprm5lem  12776  odzdvds  12881  pythagtriplem14  12913  pcid  12960  fldivp1  12984  pockthlem  12992  4sqlem5  13018  4sqlem10  13023  mul4sqlem  13029  4sqlem15  13041  4sqlem16  13042  mulgneg  13790  ghmmulg  13906  rege0subm  14663  metrtri  15171  bl2in  15197  blhalf  15202  blssps  15221  blss  15222  maxcncf  15409  mincncf  15410  dedekindeu  15417  dedekindicclemicc  15426  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthinc  15437  ivthdec  15438  ivthreinc  15439  dvconstre  15490  dvidre  15491  dvcjbr  15502  dvfre  15504  dveflem  15520  plyrecj  15557  reeff1olem  15565  reeff1oleme  15566  eflt  15569  sin0pilem1  15575  sin0pilem2  15576  pilem3  15577  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  sinq12gt0  15624  sinq34lt0t  15625  cosq14gt0  15626  cosq23lt0  15627  coseq0q4123  15628  coseq0negpitopi  15630  tanrpcl  15631  tangtx  15632  coskpi  15642  cosordlem  15643  cosq34lt1  15644  cos11  15647  reexplog  15665  relogexp  15666  logdivlti  15675  rpcxpef  15688  rpcncxpcl  15696  cxpap0  15698  rpcxpadd  15699  rpmulcxp  15703  cxpmul  15706  abscxp  15709  cxplt  15710  cxplt3  15714  logsqrt  15717  apcxp2  15733  rpabscxpbnd  15734  rplogbid1  15741  rplogb1  15742  rpelogb  15743  rplogbchbase  15744  rplogbreexp  15747  rprelogbmul  15749  rprelogbdiv  15751  rplogbcxp  15757  rpcxplogb  15758  logbgcd1irraplemexp  15762  logbgcd1irraplemap  15763  pellexlem2  15775  mersenne  15794  lgsvalmod  15821  lgsdilem  15829  lgsne0  15840  gausslemma2dlem1a  15860  gausslemma2dlem6  15869  lgseisenlem1  15872  lgseisenlem2  15873  lgseisen  15876  lgsquadlem1  15879  lgsquadlem2  15880  2sqlem1  15916  mul2sq  15918  2sqlem3  15919  2sqlem8  15925  qdencn  16738  refeq  16739  repiecele0  16741  repiecege0  16742  cvgcmp2nlemabs  16747  cvgcmp2n  16748  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  trirec0  16759  apdifflemf  16761  apdifflemr  16762  apdiff  16763  qdiff  16764  redc0  16773  reap0  16774  cndcap  16775  nconstwlpolem0  16779  nconstwlpolemgt0  16780  neap0mkv  16785  ltlenmkv  16786