Theorem recnd 8201

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℂcc 8023  ℝcr 8024

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-resscn 8117

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  readdcan  8312  ltadd2  8592  ltadd1  8602  leadd2  8604  ltsubadd  8605  ltsubadd2  8606  lesubadd  8607  lesubadd2  8608  ltaddsub  8609  leaddsub  8611  lesub1  8629  lesub2  8630  ltsub1  8631  ltsub2  8632  ltnegcon1  8636  ltnegcon2  8637  add20  8647  subge0  8648  suble0  8649  lesub0  8652  eqord2  8657  possumd  8742  sublt0d  8743  rimul  8758  rereim  8759  apreap  8760  ltmul1a  8764  ltmul1  8765  reapmul1  8768  remulext2  8773  cru  8775  apreim  8776  mulreim  8777  apadd1  8781  apneg  8784  mulext1  8785  ltapd  8811  aprcl  8819  aptap  8823  rerecclap  8903  redivclap  8904  recgt0  9023  prodgt0gt0  9024  prodgt0  9025  prodge0  9027  lemul1a  9031  ltdiv1  9041  ltmuldiv  9047  ledivmul  9050  lt2mul2div  9052  ltrec  9056  lt2msq  9059  ltdiv2  9060  ltrec1  9061  lerec2  9062  ledivdiv  9063  lediv2  9064  ltdiv23  9065  lediv23  9066  lediv12a  9067  recp1lt1  9072  recreclt  9073  ledivp1  9076  mulle0r  9117  negiso  9128  avglt1  9376  avglt2  9377  div4p1lem1div2  9391  nn0cnd  9450  zcn  9477  peano2z  9508  zaddcllemneg  9511  ztri3or  9515  zeo  9578  zcnd  9596  eluzmn  9755  eluzelcn  9760  infrenegsupex  9821  supinfneg  9822  infsupneg  9823  supminfex  9824  irrmulap  9875  cnref1o  9878  rpcn  9890  rpcnd  9926  ltaddrp2d  9959  mul2lt0rlt0  9987  mul2lt0rgt0  9988  mul2lt0llt0  9989  mul2lt0lgt0  9990  mul2lt0np  9991  mul2lt0pn  9992  xpncan  10099  icoshftf1o  10219  lincmb01cmp  10231  iccf1o  10232  infssuzcldc  10488  qbtwnrelemcalc  10508  flhalf  10555  intfracq  10575  flqdiv  10576  modqid  10604  modqid0  10605  mulqaddmodid  10619  seqf1oglem1  10774  ser3le  10792  expcl2lemap  10806  expnegzap  10828  expaddzaplem  10837  expaddzap  10838  expmulzap  10840  ltexp2a  10846  leexp2a  10847  leexp2r  10848  exple1  10850  expubnd  10851  sq11  10867  bernneq2  10916  expnbnd  10918  nn0ltexp2  10964  nn0opthlem2d  10976  faclbnd  10996  bcp1nk  11017  remim  11414  reim0b  11416  rereb  11417  mulreap  11418  cjreb  11420  recj  11421  reneg  11422  readd  11423  resub  11424  remullem  11425  remul2  11427  redivap  11428  imcj  11429  imneg  11430  imadd  11431  imsub  11432  immul2  11434  imdivap  11435  cjcj  11437  cjadd  11438  ipcnval  11440  cjmulval  11442  cjneg  11444  imval2  11448  cjreim2  11458  cjap  11460  cnrecnv  11464  caucvgrelemrec  11533  cvg1nlemres  11539  recvguniqlem  11548  recvguniq  11549  resqrexlemover  11564  resqrexlemcalc1  11568  resqrexlemcalc2  11569  resqrexlemcalc3  11570  resqrexlemnmsq  11571  resqrexlemnm  11572  resqrexlemgt0  11574  resqrexlemoverl  11575  resqrexlemglsq  11576  remsqsqrt  11586  sqrtmul  11589  sqrtdiv  11596  sqrtmsq  11599  abs00ap  11616  absext  11617  abs00  11618  absdivap  11624  absid  11625  absexp  11633  absexpzap  11634  absimle  11638  abslt  11642  absle  11643  abssubap0  11644  abssubne0  11645  releabs  11650  recvalap  11651  abstri  11658  abs2difabs  11662  amgm2  11672  icodiamlt  11734  maxabsle  11758  maxabslemab  11760  maxabslemlub  11761  maxabslemval  11762  maxcl  11764  maxltsup  11772  max0addsup  11773  minmax  11784  minabs  11790  minclpr  11791  bdtrilem  11793  bdtri  11794  mul0inf  11795  mingeb  11796  climabs0  11861  reccn2ap  11867  climrecl  11878  climge0  11879  climle  11888  climsqz  11889  climsqz2  11890  climlec2  11895  climrecvg1n  11902  climcvg1nlem  11903  isumrecl  11983  isumge0  11984  fsumlessfi  12014  fsumge1  12015  fsum00  12016  fsumle  12017  fsumlt  12018  fsumabs  12019  iserabs  12029  isumrpcl  12048  isumle  12049  isumlessdc  12050  trireciplem  12054  trirecip  12055  expcnvre  12057  expcnv  12058  explecnv  12059  absltap  12063  geo2sum  12068  cvgratnnlembern  12077  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  cvgratnnlemabsle  12081  cvgratnnlemsumlt  12082  cvgratnnlemfm  12083  cvgratnnlemrate  12084  cvgratz  12086  mertenslemi1  12089  mertenslem2  12090  fprodabs  12170  fprodle  12194  efcllemp  12212  ege2le3  12225  efaddlem  12228  efgt0  12238  reeftlcl  12243  eftlub  12244  effsumlt  12246  efltim  12252  eflegeo  12255  resin4p  12272  recos4p  12273  efeul  12288  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  sin01gt0  12316  cos01gt0  12317  sin02gt0  12318  cos12dec  12322  absefi  12323  absef  12324  absefib  12325  efieq1re  12326  eirraplem  12331  dvdsaddre2b  12395  dvdslelemd  12397  odd2np1  12427  divalglemnqt  12474  bitsp1o  12507  bitsfzo  12509  bitscmp  12512  nn0seqcvgd  12606  sqnprm  12701  isprm5lem  12706  odzdvds  12811  pythagtriplem14  12843  pcid  12890  fldivp1  12914  pockthlem  12922  4sqlem5  12948  4sqlem10  12953  mul4sqlem  12959  4sqlem15  12971  4sqlem16  12972  mulgneg  13720  ghmmulg  13836  rege0subm  14591  metrtri  15094  bl2in  15120  blhalf  15125  blssps  15144  blss  15145  maxcncf  15332  mincncf  15333  dedekindeu  15340  dedekindicclemicc  15349  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthinc  15360  ivthdec  15361  ivthreinc  15362  dvconstre  15413  dvidre  15414  dvcjbr  15425  dvfre  15427  dveflem  15443  plyrecj  15480  reeff1olem  15488  reeff1oleme  15489  eflt  15492  sin0pilem1  15498  sin0pilem2  15499  pilem3  15500  sincosq2sgn  15544  sincosq3sgn  15545  sincosq4sgn  15546  sinq12gt0  15547  sinq34lt0t  15548  cosq14gt0  15549  cosq23lt0  15550  coseq0q4123  15551  coseq0negpitopi  15553  tanrpcl  15554  tangtx  15555  coskpi  15565  cosordlem  15566  cosq34lt1  15567  cos11  15570  reexplog  15588  relogexp  15589  logdivlti  15598  rpcxpef  15611  rpcncxpcl  15619  cxpap0  15621  rpcxpadd  15622  rpmulcxp  15626  cxpmul  15629  abscxp  15632  cxplt  15633  cxplt3  15637  logsqrt  15640  apcxp2  15656  rpabscxpbnd  15657  rplogbid1  15664  rplogb1  15665  rpelogb  15666  rplogbchbase  15667  rplogbreexp  15670  rprelogbmul  15672  rprelogbdiv  15674  rplogbcxp  15680  rpcxplogb  15681  logbgcd1irraplemexp  15685  logbgcd1irraplemap  15686  mersenne  15714  lgsvalmod  15741  lgsdilem  15749  lgsne0  15760  gausslemma2dlem1a  15780  gausslemma2dlem6  15789  lgseisenlem1  15792  lgseisenlem2  15793  lgseisen  15796  lgsquadlem1  15799  lgsquadlem2  15800  2sqlem1  15836  mul2sq  15838  2sqlem3  15839  2sqlem8  15845  qdencn  16581  refeq  16582  cvgcmp2nlemabs  16586  cvgcmp2n  16587  trilpolemisumle  16592  trilpolemeq1  16594  trilpolemlt1  16595  trirec0  16598  apdifflemf  16600  apdifflemr  16601  apdiff  16602  redc0  16611  reap0  16612  cndcap  16613  nconstwlpolem0  16617  nconstwlpolemgt0  16618  neap0mkv  16623  ltlenmkv  16624