Theorem recnd 7960

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

Syntax hints:   → wi 4   ∈ wcel 2146  ℂcc 7784  ℝcr 7785

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-resscn 7878

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  readdcan  8071  ltadd2  8350  ltadd1  8360  leadd2  8362  ltsubadd  8363  ltsubadd2  8364  lesubadd  8365  lesubadd2  8366  ltaddsub  8367  leaddsub  8369  lesub1  8387  lesub2  8388  ltsub1  8389  ltsub2  8390  ltnegcon1  8394  ltnegcon2  8395  add20  8405  subge0  8406  suble0  8407  lesub0  8410  eqord2  8415  possumd  8500  sublt0d  8501  rimul  8516  rereim  8517  apreap  8518  ltmul1a  8522  ltmul1  8523  reapmul1  8526  remulext2  8531  cru  8533  apreim  8534  mulreim  8535  apadd1  8539  apneg  8542  mulext1  8543  ltapd  8569  aprcl  8577  rerecclap  8660  redivclap  8661  recgt0  8780  prodgt0gt0  8781  prodgt0  8782  prodge0  8784  lemul1a  8788  ltdiv1  8798  ltmuldiv  8804  ledivmul  8807  lt2mul2div  8809  ltrec  8813  lt2msq  8816  ltdiv2  8817  ltrec1  8818  lerec2  8819  ledivdiv  8820  lediv2  8821  ltdiv23  8822  lediv23  8823  lediv12a  8824  recp1lt1  8829  recreclt  8830  ledivp1  8833  mulle0r  8874  negiso  8885  avglt1  9130  avglt2  9131  div4p1lem1div2  9145  nn0cnd  9204  zcn  9231  peano2z  9262  zaddcllemneg  9265  ztri3or  9269  zeo  9331  zcnd  9349  eluzelcn  9512  infrenegsupex  9567  supinfneg  9568  infsupneg  9569  supminfex  9570  cnref1o  9623  rpcn  9633  rpcnd  9669  ltaddrp2d  9702  mul2lt0rlt0  9730  mul2lt0rgt0  9731  mul2lt0llt0  9732  mul2lt0lgt0  9733  mul2lt0np  9734  mul2lt0pn  9735  xpncan  9842  icoshftf1o  9962  lincmb01cmp  9974  iccf1o  9975  qbtwnrelemcalc  10226  flhalf  10272  intfracq  10290  flqdiv  10291  modqid  10319  modqid0  10320  mulqaddmodid  10334  ser3le  10488  expcl2lemap  10502  expnegzap  10524  expaddzaplem  10533  expaddzap  10534  expmulzap  10536  ltexp2a  10542  leexp2a  10543  leexp2r  10544  exple1  10546  expubnd  10547  sq11  10562  bernneq2  10611  expnbnd  10613  nn0ltexp2  10658  nn0opthlem2d  10669  faclbnd  10689  bcp1nk  10710  remim  10837  reim0b  10839  rereb  10840  mulreap  10841  cjreb  10843  recj  10844  reneg  10845  readd  10846  resub  10847  remullem  10848  remul2  10850  redivap  10851  imcj  10852  imneg  10853  imadd  10854  imsub  10855  immul2  10857  imdivap  10858  cjcj  10860  cjadd  10861  ipcnval  10863  cjmulval  10865  cjneg  10867  imval2  10871  cjreim2  10881  cjap  10883  cnrecnv  10887  caucvgrelemrec  10956  cvg1nlemres  10962  recvguniqlem  10971  recvguniq  10972  resqrexlemover  10987  resqrexlemcalc1  10991  resqrexlemcalc2  10992  resqrexlemcalc3  10993  resqrexlemnmsq  10994  resqrexlemnm  10995  resqrexlemgt0  10997  resqrexlemoverl  10998  resqrexlemglsq  10999  remsqsqrt  11009  sqrtmul  11012  sqrtdiv  11019  sqrtmsq  11022  abs00ap  11039  absext  11040  abs00  11041  absdivap  11047  absid  11048  absexp  11056  absexpzap  11057  absimle  11061  abslt  11065  absle  11066  abssubap0  11067  abssubne0  11068  releabs  11073  recvalap  11074  abstri  11081  abs2difabs  11085  amgm2  11095  icodiamlt  11157  maxabsle  11181  maxabslemab  11183  maxabslemlub  11184  maxabslemval  11185  maxcl  11187  maxltsup  11195  max0addsup  11196  minmax  11206  minabs  11212  minclpr  11213  bdtrilem  11215  bdtri  11216  mul0inf  11217  mingeb  11218  climabs0  11283  reccn2ap  11289  climrecl  11300  climge0  11301  climle  11310  climsqz  11311  climsqz2  11312  climlec2  11317  climrecvg1n  11324  climcvg1nlem  11325  isumrecl  11405  isumge0  11406  fsumlessfi  11436  fsumge1  11437  fsum00  11438  fsumle  11439  fsumlt  11440  fsumabs  11441  iserabs  11451  isumrpcl  11470  isumle  11471  isumlessdc  11472  trireciplem  11476  trirecip  11477  expcnvre  11479  expcnv  11480  explecnv  11481  absltap  11485  geo2sum  11490  cvgratnnlembern  11499  cvgratnnlemnexp  11500  cvgratnnlemmn  11501  cvgratnnlemabsle  11503  cvgratnnlemsumlt  11504  cvgratnnlemfm  11505  cvgratnnlemrate  11506  cvgratz  11508  mertenslemi1  11511  mertenslem2  11512  fprodabs  11592  fprodle  11616  efcllemp  11634  ege2le3  11647  efaddlem  11650  efgt0  11660  reeftlcl  11665  eftlub  11666  effsumlt  11668  efltim  11674  eflegeo  11677  resin4p  11694  recos4p  11695  efeul  11710  ef01bndlem  11732  sin01bnd  11733  cos01bnd  11734  sin01gt0  11737  cos01gt0  11738  sin02gt0  11739  cos12dec  11743  absefi  11744  absef  11745  absefib  11746  efieq1re  11747  eirraplem  11752  dvdslelemd  11816  odd2np1  11845  divalglemnqt  11892  infssuzcldc  11919  nn0seqcvgd  12008  sqnprm  12103  isprm5lem  12108  odzdvds  12212  pythagtriplem14  12244  pcid  12290  fldivp1  12313  pockthlem  12321  4sqlem5  12347  4sqlem10  12352  mul4sqlem  12358  mulgneg  12871  metrtri  13457  bl2in  13483  blhalf  13488  blssps  13507  blss  13508  dedekindeu  13681  dedekindicclemicc  13690  ivthinclemlopn  13694  ivthinclemuopn  13696  ivthinc  13701  ivthdec  13702  dvcjbr  13752  dvfre  13754  dveflem  13767  reeff1olem  13772  reeff1oleme  13773  eflt  13776  sin0pilem1  13782  sin0pilem2  13783  pilem3  13784  sincosq2sgn  13828  sincosq3sgn  13829  sincosq4sgn  13830  sinq12gt0  13831  sinq34lt0t  13832  cosq14gt0  13833  cosq23lt0  13834  coseq0q4123  13835  coseq0negpitopi  13837  tanrpcl  13838  tangtx  13839  coskpi  13849  cosordlem  13850  cosq34lt1  13851  cos11  13854  reexplog  13872  relogexp  13873  logdivlti  13882  rpcxpef  13895  rpcncxpcl  13903  cxpap0  13905  rpcxpadd  13906  rpmulcxp  13910  cxpmul  13913  abscxp  13915  cxplt  13916  cxplt3  13920  logsqrt  13923  apcxp2  13938  rpabscxpbnd  13939  rplogbid1  13945  rplogb1  13946  rpelogb  13947  rplogbchbase  13948  rplogbreexp  13951  rprelogbmul  13953  rprelogbdiv  13955  rplogbcxp  13961  rpcxplogb  13962  logbgcd1irraplemexp  13966  logbgcd1irraplemap  13967  lgsvalmod  14000  lgsdilem  14008  lgsne0  14019  2sqlem1  14030  mul2sq  14032  2sqlem3  14033  2sqlem8  14039  qdencn  14345  refeq  14346  cvgcmp2nlemabs  14350  cvgcmp2n  14351  trilpolemisumle  14356  trilpolemeq1  14358  trilpolemlt1  14359  trirec0  14362  apdifflemf  14364  apdifflemr  14365  apdiff  14366  redc0  14375  reap0  14376  nconstwlpolem0  14380  nconstwlpolemgt0  14381