Theorem recnd 8055

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

Syntax hints:   -> wi 4   e. wcel 2167   CCcc 7877   RRcr 7878

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7971

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  readdcan  8166  ltadd2  8446  ltadd1  8456  leadd2  8458  ltsubadd  8459  ltsubadd2  8460  lesubadd  8461  lesubadd2  8462  ltaddsub  8463  leaddsub  8465  lesub1  8483  lesub2  8484  ltsub1  8485  ltsub2  8486  ltnegcon1  8490  ltnegcon2  8491  add20  8501  subge0  8502  suble0  8503  lesub0  8506  eqord2  8511  possumd  8596  sublt0d  8597  rimul  8612  rereim  8613  apreap  8614  ltmul1a  8618  ltmul1  8619  reapmul1  8622  remulext2  8627  cru  8629  apreim  8630  mulreim  8631  apadd1  8635  apneg  8638  mulext1  8639  ltapd  8665  aprcl  8673  aptap  8677  rerecclap  8757  redivclap  8758  recgt0  8877  prodgt0gt0  8878  prodgt0  8879  prodge0  8881  lemul1a  8885  ltdiv1  8895  ltmuldiv  8901  ledivmul  8904  lt2mul2div  8906  ltrec  8910  lt2msq  8913  ltdiv2  8914  ltrec1  8915  lerec2  8916  ledivdiv  8917  lediv2  8918  ltdiv23  8919  lediv23  8920  lediv12a  8921  recp1lt1  8926  recreclt  8927  ledivp1  8930  mulle0r  8971  negiso  8982  avglt1  9230  avglt2  9231  div4p1lem1div2  9245  nn0cnd  9304  zcn  9331  peano2z  9362  zaddcllemneg  9365  ztri3or  9369  zeo  9431  zcnd  9449  eluzelcn  9612  infrenegsupex  9668  supinfneg  9669  infsupneg  9670  supminfex  9671  irrmulap  9722  cnref1o  9725  rpcn  9737  rpcnd  9773  ltaddrp2d  9806  mul2lt0rlt0  9834  mul2lt0rgt0  9835  mul2lt0llt0  9836  mul2lt0lgt0  9837  mul2lt0np  9838  mul2lt0pn  9839  xpncan  9946  icoshftf1o  10066  lincmb01cmp  10078  iccf1o  10079  infssuzcldc  10325  qbtwnrelemcalc  10345  flhalf  10392  intfracq  10412  flqdiv  10413  modqid  10441  modqid0  10442  mulqaddmodid  10456  seqf1oglem1  10611  ser3le  10629  expcl2lemap  10643  expnegzap  10665  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  ltexp2a  10683  leexp2a  10684  leexp2r  10685  exple1  10687  expubnd  10688  sq11  10704  bernneq2  10753  expnbnd  10755  nn0ltexp2  10801  nn0opthlem2d  10813  faclbnd  10833  bcp1nk  10854  remim  11025  reim0b  11027  rereb  11028  mulreap  11029  cjreb  11031  recj  11032  reneg  11033  readd  11034  resub  11035  remullem  11036  remul2  11038  redivap  11039  imcj  11040  imneg  11041  imadd  11042  imsub  11043  immul2  11045  imdivap  11046  cjcj  11048  cjadd  11049  ipcnval  11051  cjmulval  11053  cjneg  11055  imval2  11059  cjreim2  11069  cjap  11071  cnrecnv  11075  caucvgrelemrec  11144  cvg1nlemres  11150  recvguniqlem  11159  recvguniq  11160  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemcalc2  11180  resqrexlemcalc3  11181  resqrexlemnmsq  11182  resqrexlemnm  11183  resqrexlemgt0  11185  resqrexlemoverl  11186  resqrexlemglsq  11187  remsqsqrt  11197  sqrtmul  11200  sqrtdiv  11207  sqrtmsq  11210  abs00ap  11227  absext  11228  abs00  11229  absdivap  11235  absid  11236  absexp  11244  absexpzap  11245  absimle  11249  abslt  11253  absle  11254  abssubap0  11255  abssubne0  11256  releabs  11261  recvalap  11262  abstri  11269  abs2difabs  11273  amgm2  11283  icodiamlt  11345  maxabsle  11369  maxabslemab  11371  maxabslemlub  11372  maxabslemval  11373  maxcl  11375  maxltsup  11383  max0addsup  11384  minmax  11395  minabs  11401  minclpr  11402  bdtrilem  11404  bdtri  11405  mul0inf  11406  mingeb  11407  climabs0  11472  reccn2ap  11478  climrecl  11489  climge0  11490  climle  11499  climsqz  11500  climsqz2  11501  climlec2  11506  climrecvg1n  11513  climcvg1nlem  11514  isumrecl  11594  isumge0  11595  fsumlessfi  11625  fsumge1  11626  fsum00  11627  fsumle  11628  fsumlt  11629  fsumabs  11630  iserabs  11640  isumrpcl  11659  isumle  11660  isumlessdc  11661  trireciplem  11665  trirecip  11666  expcnvre  11668  expcnv  11669  explecnv  11670  absltap  11674  geo2sum  11679  cvgratnnlembern  11688  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratnnlemabsle  11692  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratz  11697  mertenslemi1  11700  mertenslem2  11701  fprodabs  11781  fprodle  11805  efcllemp  11823  ege2le3  11836  efaddlem  11839  efgt0  11849  reeftlcl  11854  eftlub  11855  effsumlt  11857  efltim  11863  eflegeo  11866  resin4p  11883  recos4p  11884  efeul  11899  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  cos12dec  11933  absefi  11934  absef  11935  absefib  11936  efieq1re  11937  eirraplem  11942  dvdsaddre2b  12006  dvdslelemd  12008  odd2np1  12038  divalglemnqt  12085  bitsp1o  12117  bitsfzo  12119  nn0seqcvgd  12209  sqnprm  12304  isprm5lem  12309  odzdvds  12414  pythagtriplem14  12446  pcid  12493  fldivp1  12517  pockthlem  12525  4sqlem5  12551  4sqlem10  12556  mul4sqlem  12562  4sqlem15  12574  4sqlem16  12575  mulgneg  13270  ghmmulg  13386  rege0subm  14140  metrtri  14613  bl2in  14639  blhalf  14644  blssps  14663  blss  14664  maxcncf  14851  mincncf  14852  dedekindeu  14859  dedekindicclemicc  14868  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthinc  14879  ivthdec  14880  ivthreinc  14881  dvconstre  14932  dvidre  14933  dvcjbr  14944  dvfre  14946  dveflem  14962  plyrecj  14999  reeff1olem  15007  reeff1oleme  15008  eflt  15011  sin0pilem1  15017  sin0pilem2  15018  pilem3  15019  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  sinq34lt0t  15067  cosq14gt0  15068  cosq23lt0  15069  coseq0q4123  15070  coseq0negpitopi  15072  tanrpcl  15073  tangtx  15074  coskpi  15084  cosordlem  15085  cosq34lt1  15086  cos11  15089  reexplog  15107  relogexp  15108  logdivlti  15117  rpcxpef  15130  rpcncxpcl  15138  cxpap0  15140  rpcxpadd  15141  rpmulcxp  15145  cxpmul  15148  abscxp  15151  cxplt  15152  cxplt3  15156  logsqrt  15159  apcxp2  15175  rpabscxpbnd  15176  rplogbid1  15183  rplogb1  15184  rpelogb  15185  rplogbchbase  15186  rplogbreexp  15189  rprelogbmul  15191  rprelogbdiv  15193  rplogbcxp  15199  rpcxplogb  15200  logbgcd1irraplemexp  15204  logbgcd1irraplemap  15205  mersenne  15233  lgsvalmod  15260  lgsdilem  15268  lgsne0  15279  gausslemma2dlem1a  15299  gausslemma2dlem6  15308  lgseisenlem1  15311  lgseisenlem2  15312  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  2sqlem1  15355  mul2sq  15357  2sqlem3  15358  2sqlem8  15364  qdencn  15671  refeq  15672  cvgcmp2nlemabs  15676  cvgcmp2n  15677  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trirec0  15688  apdifflemf  15690  apdifflemr  15691  apdiff  15692  redc0  15701  reap0  15702  cndcap  15703  nconstwlpolem0  15707  nconstwlpolemgt0  15708  neap0mkv  15713  ltlenmkv  15714