Theorem recnd 8131

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

Syntax hints:   -> wi 4   e. wcel 2177   CCcc 7953   RRcr 7954

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-resscn 8047

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  readdcan  8242  ltadd2  8522  ltadd1  8532  leadd2  8534  ltsubadd  8535  ltsubadd2  8536  lesubadd  8537  lesubadd2  8538  ltaddsub  8539  leaddsub  8541  lesub1  8559  lesub2  8560  ltsub1  8561  ltsub2  8562  ltnegcon1  8566  ltnegcon2  8567  add20  8577  subge0  8578  suble0  8579  lesub0  8582  eqord2  8587  possumd  8672  sublt0d  8673  rimul  8688  rereim  8689  apreap  8690  ltmul1a  8694  ltmul1  8695  reapmul1  8698  remulext2  8703  cru  8705  apreim  8706  mulreim  8707  apadd1  8711  apneg  8714  mulext1  8715  ltapd  8741  aprcl  8749  aptap  8753  rerecclap  8833  redivclap  8834  recgt0  8953  prodgt0gt0  8954  prodgt0  8955  prodge0  8957  lemul1a  8961  ltdiv1  8971  ltmuldiv  8977  ledivmul  8980  lt2mul2div  8982  ltrec  8986  lt2msq  8989  ltdiv2  8990  ltrec1  8991  lerec2  8992  ledivdiv  8993  lediv2  8994  ltdiv23  8995  lediv23  8996  lediv12a  8997  recp1lt1  9002  recreclt  9003  ledivp1  9006  mulle0r  9047  negiso  9058  avglt1  9306  avglt2  9307  div4p1lem1div2  9321  nn0cnd  9380  zcn  9407  peano2z  9438  zaddcllemneg  9441  ztri3or  9445  zeo  9508  zcnd  9526  eluzelcn  9689  infrenegsupex  9745  supinfneg  9746  infsupneg  9747  supminfex  9748  irrmulap  9799  cnref1o  9802  rpcn  9814  rpcnd  9850  ltaddrp2d  9883  mul2lt0rlt0  9911  mul2lt0rgt0  9912  mul2lt0llt0  9913  mul2lt0lgt0  9914  mul2lt0np  9915  mul2lt0pn  9916  xpncan  10023  icoshftf1o  10143  lincmb01cmp  10155  iccf1o  10156  infssuzcldc  10410  qbtwnrelemcalc  10430  flhalf  10477  intfracq  10497  flqdiv  10498  modqid  10526  modqid0  10527  mulqaddmodid  10541  seqf1oglem1  10696  ser3le  10714  expcl2lemap  10728  expnegzap  10750  expaddzaplem  10759  expaddzap  10760  expmulzap  10762  ltexp2a  10768  leexp2a  10769  leexp2r  10770  exple1  10772  expubnd  10773  sq11  10789  bernneq2  10838  expnbnd  10840  nn0ltexp2  10886  nn0opthlem2d  10898  faclbnd  10918  bcp1nk  10939  remim  11256  reim0b  11258  rereb  11259  mulreap  11260  cjreb  11262  recj  11263  reneg  11264  readd  11265  resub  11266  remullem  11267  remul2  11269  redivap  11270  imcj  11271  imneg  11272  imadd  11273  imsub  11274  immul2  11276  imdivap  11277  cjcj  11279  cjadd  11280  ipcnval  11282  cjmulval  11284  cjneg  11286  imval2  11290  cjreim2  11300  cjap  11302  cnrecnv  11306  caucvgrelemrec  11375  cvg1nlemres  11381  recvguniqlem  11390  recvguniq  11391  resqrexlemover  11406  resqrexlemcalc1  11410  resqrexlemcalc2  11411  resqrexlemcalc3  11412  resqrexlemnmsq  11413  resqrexlemnm  11414  resqrexlemgt0  11416  resqrexlemoverl  11417  resqrexlemglsq  11418  remsqsqrt  11428  sqrtmul  11431  sqrtdiv  11438  sqrtmsq  11441  abs00ap  11458  absext  11459  abs00  11460  absdivap  11466  absid  11467  absexp  11475  absexpzap  11476  absimle  11480  abslt  11484  absle  11485  abssubap0  11486  abssubne0  11487  releabs  11492  recvalap  11493  abstri  11500  abs2difabs  11504  amgm2  11514  icodiamlt  11576  maxabsle  11600  maxabslemab  11602  maxabslemlub  11603  maxabslemval  11604  maxcl  11606  maxltsup  11614  max0addsup  11615  minmax  11626  minabs  11632  minclpr  11633  bdtrilem  11635  bdtri  11636  mul0inf  11637  mingeb  11638  climabs0  11703  reccn2ap  11709  climrecl  11720  climge0  11721  climle  11730  climsqz  11731  climsqz2  11732  climlec2  11737  climrecvg1n  11744  climcvg1nlem  11745  isumrecl  11825  isumge0  11826  fsumlessfi  11856  fsumge1  11857  fsum00  11858  fsumle  11859  fsumlt  11860  fsumabs  11861  iserabs  11871  isumrpcl  11890  isumle  11891  isumlessdc  11892  trireciplem  11896  trirecip  11897  expcnvre  11899  expcnv  11900  explecnv  11901  absltap  11905  geo2sum  11910  cvgratnnlembern  11919  cvgratnnlemnexp  11920  cvgratnnlemmn  11921  cvgratnnlemabsle  11923  cvgratnnlemsumlt  11924  cvgratnnlemfm  11925  cvgratnnlemrate  11926  cvgratz  11928  mertenslemi1  11931  mertenslem2  11932  fprodabs  12012  fprodle  12036  efcllemp  12054  ege2le3  12067  efaddlem  12070  efgt0  12080  reeftlcl  12085  eftlub  12086  effsumlt  12088  efltim  12094  eflegeo  12097  resin4p  12114  recos4p  12115  efeul  12130  ef01bndlem  12152  sin01bnd  12153  cos01bnd  12154  sin01gt0  12158  cos01gt0  12159  sin02gt0  12160  cos12dec  12164  absefi  12165  absef  12166  absefib  12167  efieq1re  12168  eirraplem  12173  dvdsaddre2b  12237  dvdslelemd  12239  odd2np1  12269  divalglemnqt  12316  bitsp1o  12349  bitsfzo  12351  bitscmp  12354  nn0seqcvgd  12448  sqnprm  12543  isprm5lem  12548  odzdvds  12653  pythagtriplem14  12685  pcid  12732  fldivp1  12756  pockthlem  12764  4sqlem5  12790  4sqlem10  12795  mul4sqlem  12801  4sqlem15  12813  4sqlem16  12814  mulgneg  13561  ghmmulg  13677  rege0subm  14431  metrtri  14934  bl2in  14960  blhalf  14965  blssps  14984  blss  14985  maxcncf  15172  mincncf  15173  dedekindeu  15180  dedekindicclemicc  15189  ivthinclemlopn  15193  ivthinclemuopn  15195  ivthinc  15200  ivthdec  15201  ivthreinc  15202  dvconstre  15253  dvidre  15254  dvcjbr  15265  dvfre  15267  dveflem  15283  plyrecj  15320  reeff1olem  15328  reeff1oleme  15329  eflt  15332  sin0pilem1  15338  sin0pilem2  15339  pilem3  15340  sincosq2sgn  15384  sincosq3sgn  15385  sincosq4sgn  15386  sinq12gt0  15387  sinq34lt0t  15388  cosq14gt0  15389  cosq23lt0  15390  coseq0q4123  15391  coseq0negpitopi  15393  tanrpcl  15394  tangtx  15395  coskpi  15405  cosordlem  15406  cosq34lt1  15407  cos11  15410  reexplog  15428  relogexp  15429  logdivlti  15438  rpcxpef  15451  rpcncxpcl  15459  cxpap0  15461  rpcxpadd  15462  rpmulcxp  15466  cxpmul  15469  abscxp  15472  cxplt  15473  cxplt3  15477  logsqrt  15480  apcxp2  15496  rpabscxpbnd  15497  rplogbid1  15504  rplogb1  15505  rpelogb  15506  rplogbchbase  15507  rplogbreexp  15510  rprelogbmul  15512  rprelogbdiv  15514  rplogbcxp  15520  rpcxplogb  15521  logbgcd1irraplemexp  15525  logbgcd1irraplemap  15526  mersenne  15554  lgsvalmod  15581  lgsdilem  15589  lgsne0  15600  gausslemma2dlem1a  15620  gausslemma2dlem6  15629  lgseisenlem1  15632  lgseisenlem2  15633  lgseisen  15636  lgsquadlem1  15639  lgsquadlem2  15640  2sqlem1  15676  mul2sq  15678  2sqlem3  15679  2sqlem8  15685  qdencn  16138  refeq  16139  cvgcmp2nlemabs  16143  cvgcmp2n  16144  trilpolemisumle  16149  trilpolemeq1  16151  trilpolemlt1  16152  trirec0  16155  apdifflemf  16157  apdifflemr  16158  apdiff  16159  redc0  16168  reap0  16169  cndcap  16170  nconstwlpolem0  16174  nconstwlpolemgt0  16175  neap0mkv  16180  ltlenmkv  16181