Theorem recnd 8143

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

Syntax hints:   → wi 4   ∈ wcel 2180  ℂcc 7965  ℝcr 7966

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-resscn 8059

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  readdcan  8254  ltadd2  8534  ltadd1  8544  leadd2  8546  ltsubadd  8547  ltsubadd2  8548  lesubadd  8549  lesubadd2  8550  ltaddsub  8551  leaddsub  8553  lesub1  8571  lesub2  8572  ltsub1  8573  ltsub2  8574  ltnegcon1  8578  ltnegcon2  8579  add20  8589  subge0  8590  suble0  8591  lesub0  8594  eqord2  8599  possumd  8684  sublt0d  8685  rimul  8700  rereim  8701  apreap  8702  ltmul1a  8706  ltmul1  8707  reapmul1  8710  remulext2  8715  cru  8717  apreim  8718  mulreim  8719  apadd1  8723  apneg  8726  mulext1  8727  ltapd  8753  aprcl  8761  aptap  8765  rerecclap  8845  redivclap  8846  recgt0  8965  prodgt0gt0  8966  prodgt0  8967  prodge0  8969  lemul1a  8973  ltdiv1  8983  ltmuldiv  8989  ledivmul  8992  lt2mul2div  8994  ltrec  8998  lt2msq  9001  ltdiv2  9002  ltrec1  9003  lerec2  9004  ledivdiv  9005  lediv2  9006  ltdiv23  9007  lediv23  9008  lediv12a  9009  recp1lt1  9014  recreclt  9015  ledivp1  9018  mulle0r  9059  negiso  9070  avglt1  9318  avglt2  9319  div4p1lem1div2  9333  nn0cnd  9392  zcn  9419  peano2z  9450  zaddcllemneg  9453  ztri3or  9457  zeo  9520  zcnd  9538  eluzelcn  9701  infrenegsupex  9757  supinfneg  9758  infsupneg  9759  supminfex  9760  irrmulap  9811  cnref1o  9814  rpcn  9826  rpcnd  9862  ltaddrp2d  9895  mul2lt0rlt0  9923  mul2lt0rgt0  9924  mul2lt0llt0  9925  mul2lt0lgt0  9926  mul2lt0np  9927  mul2lt0pn  9928  xpncan  10035  icoshftf1o  10155  lincmb01cmp  10167  iccf1o  10168  infssuzcldc  10422  qbtwnrelemcalc  10442  flhalf  10489  intfracq  10509  flqdiv  10510  modqid  10538  modqid0  10539  mulqaddmodid  10553  seqf1oglem1  10708  ser3le  10726  expcl2lemap  10740  expnegzap  10762  expaddzaplem  10771  expaddzap  10772  expmulzap  10774  ltexp2a  10780  leexp2a  10781  leexp2r  10782  exple1  10784  expubnd  10785  sq11  10801  bernneq2  10850  expnbnd  10852  nn0ltexp2  10898  nn0opthlem2d  10910  faclbnd  10930  bcp1nk  10951  remim  11337  reim0b  11339  rereb  11340  mulreap  11341  cjreb  11343  recj  11344  reneg  11345  readd  11346  resub  11347  remullem  11348  remul2  11350  redivap  11351  imcj  11352  imneg  11353  imadd  11354  imsub  11355  immul2  11357  imdivap  11358  cjcj  11360  cjadd  11361  ipcnval  11363  cjmulval  11365  cjneg  11367  imval2  11371  cjreim2  11381  cjap  11383  cnrecnv  11387  caucvgrelemrec  11456  cvg1nlemres  11462  recvguniqlem  11471  recvguniq  11472  resqrexlemover  11487  resqrexlemcalc1  11491  resqrexlemcalc2  11492  resqrexlemcalc3  11493  resqrexlemnmsq  11494  resqrexlemnm  11495  resqrexlemgt0  11497  resqrexlemoverl  11498  resqrexlemglsq  11499  remsqsqrt  11509  sqrtmul  11512  sqrtdiv  11519  sqrtmsq  11522  abs00ap  11539  absext  11540  abs00  11541  absdivap  11547  absid  11548  absexp  11556  absexpzap  11557  absimle  11561  abslt  11565  absle  11566  abssubap0  11567  abssubne0  11568  releabs  11573  recvalap  11574  abstri  11581  abs2difabs  11585  amgm2  11595  icodiamlt  11657  maxabsle  11681  maxabslemab  11683  maxabslemlub  11684  maxabslemval  11685  maxcl  11687  maxltsup  11695  max0addsup  11696  minmax  11707  minabs  11713  minclpr  11714  bdtrilem  11716  bdtri  11717  mul0inf  11718  mingeb  11719  climabs0  11784  reccn2ap  11790  climrecl  11801  climge0  11802  climle  11811  climsqz  11812  climsqz2  11813  climlec2  11818  climrecvg1n  11825  climcvg1nlem  11826  isumrecl  11906  isumge0  11907  fsumlessfi  11937  fsumge1  11938  fsum00  11939  fsumle  11940  fsumlt  11941  fsumabs  11942  iserabs  11952  isumrpcl  11971  isumle  11972  isumlessdc  11973  trireciplem  11977  trirecip  11978  expcnvre  11980  expcnv  11981  explecnv  11982  absltap  11986  geo2sum  11991  cvgratnnlembern  12000  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  cvgratnnlemabsle  12004  cvgratnnlemsumlt  12005  cvgratnnlemfm  12006  cvgratnnlemrate  12007  cvgratz  12009  mertenslemi1  12012  mertenslem2  12013  fprodabs  12093  fprodle  12117  efcllemp  12135  ege2le3  12148  efaddlem  12151  efgt0  12161  reeftlcl  12166  eftlub  12167  effsumlt  12169  efltim  12175  eflegeo  12178  resin4p  12195  recos4p  12196  efeul  12211  ef01bndlem  12233  sin01bnd  12234  cos01bnd  12235  sin01gt0  12239  cos01gt0  12240  sin02gt0  12241  cos12dec  12245  absefi  12246  absef  12247  absefib  12248  efieq1re  12249  eirraplem  12254  dvdsaddre2b  12318  dvdslelemd  12320  odd2np1  12350  divalglemnqt  12397  bitsp1o  12430  bitsfzo  12432  bitscmp  12435  nn0seqcvgd  12529  sqnprm  12624  isprm5lem  12629  odzdvds  12734  pythagtriplem14  12766  pcid  12813  fldivp1  12837  pockthlem  12845  4sqlem5  12871  4sqlem10  12876  mul4sqlem  12882  4sqlem15  12894  4sqlem16  12895  mulgneg  13643  ghmmulg  13759  rege0subm  14513  metrtri  15016  bl2in  15042  blhalf  15047  blssps  15066  blss  15067  maxcncf  15254  mincncf  15255  dedekindeu  15262  dedekindicclemicc  15271  ivthinclemlopn  15275  ivthinclemuopn  15277  ivthinc  15282  ivthdec  15283  ivthreinc  15284  dvconstre  15335  dvidre  15336  dvcjbr  15347  dvfre  15349  dveflem  15365  plyrecj  15402  reeff1olem  15410  reeff1oleme  15411  eflt  15414  sin0pilem1  15420  sin0pilem2  15421  pilem3  15422  sincosq2sgn  15466  sincosq3sgn  15467  sincosq4sgn  15468  sinq12gt0  15469  sinq34lt0t  15470  cosq14gt0  15471  cosq23lt0  15472  coseq0q4123  15473  coseq0negpitopi  15475  tanrpcl  15476  tangtx  15477  coskpi  15487  cosordlem  15488  cosq34lt1  15489  cos11  15492  reexplog  15510  relogexp  15511  logdivlti  15520  rpcxpef  15533  rpcncxpcl  15541  cxpap0  15543  rpcxpadd  15544  rpmulcxp  15548  cxpmul  15551  abscxp  15554  cxplt  15555  cxplt3  15559  logsqrt  15562  apcxp2  15578  rpabscxpbnd  15579  rplogbid1  15586  rplogb1  15587  rpelogb  15588  rplogbchbase  15589  rplogbreexp  15592  rprelogbmul  15594  rprelogbdiv  15596  rplogbcxp  15602  rpcxplogb  15603  logbgcd1irraplemexp  15607  logbgcd1irraplemap  15608  mersenne  15636  lgsvalmod  15663  lgsdilem  15671  lgsne0  15682  gausslemma2dlem1a  15702  gausslemma2dlem6  15711  lgseisenlem1  15714  lgseisenlem2  15715  lgseisen  15718  lgsquadlem1  15721  lgsquadlem2  15722  2sqlem1  15758  mul2sq  15760  2sqlem3  15761  2sqlem8  15767  qdencn  16306  refeq  16307  cvgcmp2nlemabs  16311  cvgcmp2n  16312  trilpolemisumle  16317  trilpolemeq1  16319  trilpolemlt1  16320  trirec0  16323  apdifflemf  16325  apdifflemr  16326  apdiff  16327  redc0  16336  reap0  16337  cndcap  16338  nconstwlpolem0  16342  nconstwlpolemgt0  16343  neap0mkv  16348  ltlenmkv  16349