Theorem recnd 8048

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 8005	. 2 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ ℂ)

Syntax hints:   → wi 4   ∈ wcel 2164  ℂcc 7870  ℝcr 7871

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-resscn 7964

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  readdcan  8159  ltadd2  8438  ltadd1  8448  leadd2  8450  ltsubadd  8451  ltsubadd2  8452  lesubadd  8453  lesubadd2  8454  ltaddsub  8455  leaddsub  8457  lesub1  8475  lesub2  8476  ltsub1  8477  ltsub2  8478  ltnegcon1  8482  ltnegcon2  8483  add20  8493  subge0  8494  suble0  8495  lesub0  8498  eqord2  8503  possumd  8588  sublt0d  8589  rimul  8604  rereim  8605  apreap  8606  ltmul1a  8610  ltmul1  8611  reapmul1  8614  remulext2  8619  cru  8621  apreim  8622  mulreim  8623  apadd1  8627  apneg  8630  mulext1  8631  ltapd  8657  aprcl  8665  aptap  8669  rerecclap  8749  redivclap  8750  recgt0  8869  prodgt0gt0  8870  prodgt0  8871  prodge0  8873  lemul1a  8877  ltdiv1  8887  ltmuldiv  8893  ledivmul  8896  lt2mul2div  8898  ltrec  8902  lt2msq  8905  ltdiv2  8906  ltrec1  8907  lerec2  8908  ledivdiv  8909  lediv2  8910  ltdiv23  8911  lediv23  8912  lediv12a  8913  recp1lt1  8918  recreclt  8919  ledivp1  8922  mulle0r  8963  negiso  8974  avglt1  9221  avglt2  9222  div4p1lem1div2  9236  nn0cnd  9295  zcn  9322  peano2z  9353  zaddcllemneg  9356  ztri3or  9360  zeo  9422  zcnd  9440  eluzelcn  9603  infrenegsupex  9659  supinfneg  9660  infsupneg  9661  supminfex  9662  irrmulap  9713  cnref1o  9716  rpcn  9728  rpcnd  9764  ltaddrp2d  9797  mul2lt0rlt0  9825  mul2lt0rgt0  9826  mul2lt0llt0  9827  mul2lt0lgt0  9828  mul2lt0np  9829  mul2lt0pn  9830  xpncan  9937  icoshftf1o  10057  lincmb01cmp  10069  iccf1o  10070  qbtwnrelemcalc  10324  flhalf  10371  intfracq  10391  flqdiv  10392  modqid  10420  modqid0  10421  mulqaddmodid  10435  seqf1oglem1  10590  ser3le  10608  expcl2lemap  10622  expnegzap  10644  expaddzaplem  10653  expaddzap  10654  expmulzap  10656  ltexp2a  10662  leexp2a  10663  leexp2r  10664  exple1  10666  expubnd  10667  sq11  10683  bernneq2  10732  expnbnd  10734  nn0ltexp2  10780  nn0opthlem2d  10792  faclbnd  10812  bcp1nk  10833  remim  11004  reim0b  11006  rereb  11007  mulreap  11008  cjreb  11010  recj  11011  reneg  11012  readd  11013  resub  11014  remullem  11015  remul2  11017  redivap  11018  imcj  11019  imneg  11020  imadd  11021  imsub  11022  immul2  11024  imdivap  11025  cjcj  11027  cjadd  11028  ipcnval  11030  cjmulval  11032  cjneg  11034  imval2  11038  cjreim2  11048  cjap  11050  cnrecnv  11054  caucvgrelemrec  11123  cvg1nlemres  11129  recvguniqlem  11138  recvguniq  11139  resqrexlemover  11154  resqrexlemcalc1  11158  resqrexlemcalc2  11159  resqrexlemcalc3  11160  resqrexlemnmsq  11161  resqrexlemnm  11162  resqrexlemgt0  11164  resqrexlemoverl  11165  resqrexlemglsq  11166  remsqsqrt  11176  sqrtmul  11179  sqrtdiv  11186  sqrtmsq  11189  abs00ap  11206  absext  11207  abs00  11208  absdivap  11214  absid  11215  absexp  11223  absexpzap  11224  absimle  11228  abslt  11232  absle  11233  abssubap0  11234  abssubne0  11235  releabs  11240  recvalap  11241  abstri  11248  abs2difabs  11252  amgm2  11262  icodiamlt  11324  maxabsle  11348  maxabslemab  11350  maxabslemlub  11351  maxabslemval  11352  maxcl  11354  maxltsup  11362  max0addsup  11363  minmax  11373  minabs  11379  minclpr  11380  bdtrilem  11382  bdtri  11383  mul0inf  11384  mingeb  11385  climabs0  11450  reccn2ap  11456  climrecl  11467  climge0  11468  climle  11477  climsqz  11478  climsqz2  11479  climlec2  11484  climrecvg1n  11491  climcvg1nlem  11492  isumrecl  11572  isumge0  11573  fsumlessfi  11603  fsumge1  11604  fsum00  11605  fsumle  11606  fsumlt  11607  fsumabs  11608  iserabs  11618  isumrpcl  11637  isumle  11638  isumlessdc  11639  trireciplem  11643  trirecip  11644  expcnvre  11646  expcnv  11647  explecnv  11648  absltap  11652  geo2sum  11657  cvgratnnlembern  11666  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemabsle  11670  cvgratnnlemsumlt  11671  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratz  11675  mertenslemi1  11678  mertenslem2  11679  fprodabs  11759  fprodle  11783  efcllemp  11801  ege2le3  11814  efaddlem  11817  efgt0  11827  reeftlcl  11832  eftlub  11833  effsumlt  11835  efltim  11841  eflegeo  11844  resin4p  11861  recos4p  11862  efeul  11877  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  cos12dec  11911  absefi  11912  absef  11913  absefib  11914  efieq1re  11915  eirraplem  11920  dvdsaddre2b  11984  dvdslelemd  11985  odd2np1  12014  divalglemnqt  12061  infssuzcldc  12088  nn0seqcvgd  12179  sqnprm  12274  isprm5lem  12279  odzdvds  12383  pythagtriplem14  12415  pcid  12462  fldivp1  12486  pockthlem  12494  4sqlem5  12520  4sqlem10  12525  mul4sqlem  12531  4sqlem15  12543  4sqlem16  12544  mulgneg  13210  ghmmulg  13326  rege0subm  14072  metrtri  14545  bl2in  14571  blhalf  14576  blssps  14595  blss  14596  maxcncf  14769  mincncf  14770  dedekindeu  14777  dedekindicclemicc  14786  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthinc  14797  ivthdec  14798  ivthreinc  14799  dvcjbr  14857  dvfre  14859  dveflem  14872  reeff1olem  14906  reeff1oleme  14907  eflt  14910  sin0pilem1  14916  sin0pilem2  14917  pilem3  14918  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  sinq34lt0t  14966  cosq14gt0  14967  cosq23lt0  14968  coseq0q4123  14969  coseq0negpitopi  14971  tanrpcl  14972  tangtx  14973  coskpi  14983  cosordlem  14984  cosq34lt1  14985  cos11  14988  reexplog  15006  relogexp  15007  logdivlti  15016  rpcxpef  15029  rpcncxpcl  15037  cxpap0  15039  rpcxpadd  15040  rpmulcxp  15044  cxpmul  15047  abscxp  15049  cxplt  15050  cxplt3  15054  logsqrt  15057  apcxp2  15072  rpabscxpbnd  15073  rplogbid1  15079  rplogb1  15080  rpelogb  15081  rplogbchbase  15082  rplogbreexp  15085  rprelogbmul  15087  rprelogbdiv  15089  rplogbcxp  15095  rpcxplogb  15096  logbgcd1irraplemexp  15100  logbgcd1irraplemap  15101  lgsvalmod  15135  lgsdilem  15143  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem6  15183  lgseisenlem1  15186  lgseisenlem2  15187  lgseisen  15190  lgsquadlem1  15191  2sqlem1  15201  mul2sq  15203  2sqlem3  15204  2sqlem8  15210  qdencn  15517  refeq  15518  cvgcmp2nlemabs  15522  cvgcmp2n  15523  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trirec0  15534  apdifflemf  15536  apdifflemr  15537  apdiff  15538  redc0  15547  reap0  15548  cndcap  15549  nconstwlpolem0  15553  nconstwlpolemgt0  15554  neap0mkv  15559  ltlenmkv  15560