Theorem recnd 8208

Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
recnd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)

Assertion

Ref	Expression
recnd	⊢ (𝜑 → 𝐴 ∈ ℂ)

Proof of Theorem recnd

Step	Hyp	Ref	Expression
1		recnd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		recn 8165	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2202  ℂcc 8030  ℝcr 8031

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-resscn 8124

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  readdcan  8319  ltadd2  8599  ltadd1  8609  leadd2  8611  ltsubadd  8612  ltsubadd2  8613  lesubadd  8614  lesubadd2  8615  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  ltnegcon1  8643  ltnegcon2  8644  add20  8654  subge0  8655  suble0  8656  lesub0  8659  eqord2  8664  possumd  8749  sublt0d  8750  rimul  8765  rereim  8766  apreap  8767  ltmul1a  8771  ltmul1  8772  reapmul1  8775  remulext2  8780  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  mulext1  8792  ltapd  8818  aprcl  8826  aptap  8830  rerecclap  8910  redivclap  8911  recgt0  9030  prodgt0gt0  9031  prodgt0  9032  prodge0  9034  lemul1a  9038  ltdiv1  9048  ltmuldiv  9054  ledivmul  9057  lt2mul2div  9059  ltrec  9063  lt2msq  9066  ltdiv2  9067  ltrec1  9068  lerec2  9069  ledivdiv  9070  lediv2  9071  ltdiv23  9072  lediv23  9073  lediv12a  9074  recp1lt1  9079  recreclt  9080  ledivp1  9083  mulle0r  9124  negiso  9135  avglt1  9383  avglt2  9384  div4p1lem1div2  9398  nn0cnd  9457  zcn  9484  peano2z  9515  zaddcllemneg  9518  ztri3or  9522  zeo  9585  zcnd  9603  eluzmn  9762  eluzelcn  9767  infrenegsupex  9828  supinfneg  9829  infsupneg  9830  supminfex  9831  irrmulap  9882  cnref1o  9885  rpcn  9897  rpcnd  9933  ltaddrp2d  9966  mul2lt0rlt0  9994  mul2lt0rgt0  9995  mul2lt0llt0  9996  mul2lt0lgt0  9997  mul2lt0np  9998  mul2lt0pn  9999  xpncan  10106  icoshftf1o  10226  lincmb01cmp  10238  iccf1o  10239  infssuzcldc  10496  qbtwnrelemcalc  10516  flhalf  10563  intfracq  10583  flqdiv  10584  modqid  10612  modqid0  10613  mulqaddmodid  10627  seqf1oglem1  10782  ser3le  10800  expcl2lemap  10814  expnegzap  10836  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  ltexp2a  10854  leexp2a  10855  leexp2r  10856  exple1  10858  expubnd  10859  sq11  10875  bernneq2  10924  expnbnd  10926  nn0ltexp2  10972  nn0opthlem2d  10984  faclbnd  11004  bcp1nk  11025  remim  11422  reim0b  11424  rereb  11425  mulreap  11426  cjreb  11428  recj  11429  reneg  11430  readd  11431  resub  11432  remullem  11433  remul2  11435  redivap  11436  imcj  11437  imneg  11438  imadd  11439  imsub  11440  immul2  11442  imdivap  11443  cjcj  11445  cjadd  11446  ipcnval  11448  cjmulval  11450  cjneg  11452  imval2  11456  cjreim2  11466  cjap  11468  cnrecnv  11472  caucvgrelemrec  11541  cvg1nlemres  11547  recvguniqlem  11556  recvguniq  11557  resqrexlemover  11572  resqrexlemcalc1  11576  resqrexlemcalc2  11577  resqrexlemcalc3  11578  resqrexlemnmsq  11579  resqrexlemnm  11580  resqrexlemgt0  11582  resqrexlemoverl  11583  resqrexlemglsq  11584  remsqsqrt  11594  sqrtmul  11597  sqrtdiv  11604  sqrtmsq  11607  abs00ap  11624  absext  11625  abs00  11626  absdivap  11632  absid  11633  absexp  11641  absexpzap  11642  absimle  11646  abslt  11650  absle  11651  abssubap0  11652  abssubne0  11653  releabs  11658  recvalap  11659  abstri  11666  abs2difabs  11670  amgm2  11680  icodiamlt  11742  maxabsle  11766  maxabslemab  11768  maxabslemlub  11769  maxabslemval  11770  maxcl  11772  maxltsup  11780  max0addsup  11781  minmax  11792  minabs  11798  minclpr  11799  bdtrilem  11801  bdtri  11802  mul0inf  11803  mingeb  11804  climabs0  11869  reccn2ap  11875  climrecl  11886  climge0  11887  climle  11896  climsqz  11897  climsqz2  11898  climlec2  11903  climrecvg1n  11910  climcvg1nlem  11911  isumrecl  11992  isumge0  11993  fsumlessfi  12023  fsumge1  12024  fsum00  12025  fsumle  12026  fsumlt  12027  fsumabs  12028  iserabs  12038  isumrpcl  12057  isumle  12058  isumlessdc  12059  trireciplem  12063  trirecip  12064  expcnvre  12066  expcnv  12067  explecnv  12068  absltap  12072  geo2sum  12077  cvgratnnlembern  12086  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  cvgratnnlemabsle  12090  cvgratnnlemsumlt  12091  cvgratnnlemfm  12092  cvgratnnlemrate  12093  cvgratz  12095  mertenslemi1  12098  mertenslem2  12099  fprodabs  12179  fprodle  12203  efcllemp  12221  ege2le3  12234  efaddlem  12237  efgt0  12247  reeftlcl  12252  eftlub  12253  effsumlt  12255  efltim  12261  eflegeo  12264  resin4p  12281  recos4p  12282  efeul  12297  ef01bndlem  12319  sin01bnd  12320  cos01bnd  12321  sin01gt0  12325  cos01gt0  12326  sin02gt0  12327  cos12dec  12331  absefi  12332  absef  12333  absefib  12334  efieq1re  12335  eirraplem  12340  dvdsaddre2b  12404  dvdslelemd  12406  odd2np1  12436  divalglemnqt  12483  bitsp1o  12516  bitsfzo  12518  bitscmp  12521  nn0seqcvgd  12615  sqnprm  12710  isprm5lem  12715  odzdvds  12820  pythagtriplem14  12852  pcid  12899  fldivp1  12923  pockthlem  12931  4sqlem5  12957  4sqlem10  12962  mul4sqlem  12968  4sqlem15  12980  4sqlem16  12981  mulgneg  13729  ghmmulg  13845  rege0subm  14601  metrtri  15104  bl2in  15130  blhalf  15135  blssps  15154  blss  15155  maxcncf  15342  mincncf  15343  dedekindeu  15350  dedekindicclemicc  15359  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthinc  15370  ivthdec  15371  ivthreinc  15372  dvconstre  15423  dvidre  15424  dvcjbr  15435  dvfre  15437  dveflem  15453  plyrecj  15490  reeff1olem  15498  reeff1oleme  15499  eflt  15502  sin0pilem1  15508  sin0pilem2  15509  pilem3  15510  sincosq2sgn  15554  sincosq3sgn  15555  sincosq4sgn  15556  sinq12gt0  15557  sinq34lt0t  15558  cosq14gt0  15559  cosq23lt0  15560  coseq0q4123  15561  coseq0negpitopi  15563  tanrpcl  15564  tangtx  15565  coskpi  15575  cosordlem  15576  cosq34lt1  15577  cos11  15580  reexplog  15598  relogexp  15599  logdivlti  15608  rpcxpef  15621  rpcncxpcl  15629  cxpap0  15631  rpcxpadd  15632  rpmulcxp  15636  cxpmul  15639  abscxp  15642  cxplt  15643  cxplt3  15647  logsqrt  15650  apcxp2  15666  rpabscxpbnd  15667  rplogbid1  15674  rplogb1  15675  rpelogb  15676  rplogbchbase  15677  rplogbreexp  15680  rprelogbmul  15682  rprelogbdiv  15684  rplogbcxp  15690  rpcxplogb  15691  logbgcd1irraplemexp  15695  logbgcd1irraplemap  15696  mersenne  15724  lgsvalmod  15751  lgsdilem  15759  lgsne0  15770  gausslemma2dlem1a  15790  gausslemma2dlem6  15799  lgseisenlem1  15802  lgseisenlem2  15803  lgseisen  15806  lgsquadlem1  15809  lgsquadlem2  15810  2sqlem1  15846  mul2sq  15848  2sqlem3  15849  2sqlem8  15855  qdencn  16652  refeq  16653  cvgcmp2nlemabs  16657  cvgcmp2n  16658  trilpolemisumle  16663  trilpolemeq1  16665  trilpolemlt1  16666  trirec0  16669  apdifflemf  16671  apdifflemr  16672  apdiff  16673  redc0  16682  reap0  16683  cndcap  16684  nconstwlpolem0  16688  nconstwlpolemgt0  16689  neap0mkv  16694  ltlenmkv  16695