Theorem recnd 7948

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℂcc 7772  ℝcr 7773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-resscn 7866

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  readdcan  8059  ltadd2  8338  ltadd1  8348  leadd2  8350  ltsubadd  8351  ltsubadd2  8352  lesubadd  8353  lesubadd2  8354  ltaddsub  8355  leaddsub  8357  lesub1  8375  lesub2  8376  ltsub1  8377  ltsub2  8378  ltnegcon1  8382  ltnegcon2  8383  add20  8393  subge0  8394  suble0  8395  lesub0  8398  eqord2  8403  possumd  8488  sublt0d  8489  rimul  8504  rereim  8505  apreap  8506  ltmul1a  8510  ltmul1  8511  reapmul1  8514  remulext2  8519  cru  8521  apreim  8522  mulreim  8523  apadd1  8527  apneg  8530  mulext1  8531  ltapd  8557  aprcl  8565  rerecclap  8647  redivclap  8648  recgt0  8766  prodgt0gt0  8767  prodgt0  8768  prodge0  8770  lemul1a  8774  ltdiv1  8784  ltmuldiv  8790  ledivmul  8793  lt2mul2div  8795  ltrec  8799  lt2msq  8802  ltdiv2  8803  ltrec1  8804  lerec2  8805  ledivdiv  8806  lediv2  8807  ltdiv23  8808  lediv23  8809  lediv12a  8810  recp1lt1  8815  recreclt  8816  ledivp1  8819  mulle0r  8860  negiso  8871  avglt1  9116  avglt2  9117  div4p1lem1div2  9131  nn0cnd  9190  zcn  9217  peano2z  9248  zaddcllemneg  9251  ztri3or  9255  zeo  9317  zcnd  9335  eluzelcn  9498  infrenegsupex  9553  supinfneg  9554  infsupneg  9555  supminfex  9556  cnref1o  9609  rpcn  9619  rpcnd  9655  ltaddrp2d  9688  mul2lt0rlt0  9716  mul2lt0rgt0  9717  mul2lt0llt0  9718  mul2lt0lgt0  9719  mul2lt0np  9720  mul2lt0pn  9721  xpncan  9828  icoshftf1o  9948  lincmb01cmp  9960  iccf1o  9961  qbtwnrelemcalc  10212  flhalf  10258  intfracq  10276  flqdiv  10277  modqid  10305  modqid0  10306  mulqaddmodid  10320  ser3le  10474  expcl2lemap  10488  expnegzap  10510  expaddzaplem  10519  expaddzap  10520  expmulzap  10522  ltexp2a  10528  leexp2a  10529  leexp2r  10530  exple1  10532  expubnd  10533  sq11  10548  bernneq2  10597  expnbnd  10599  nn0ltexp2  10644  nn0opthlem2d  10655  faclbnd  10675  bcp1nk  10696  remim  10824  reim0b  10826  rereb  10827  mulreap  10828  cjreb  10830  recj  10831  reneg  10832  readd  10833  resub  10834  remullem  10835  remul2  10837  redivap  10838  imcj  10839  imneg  10840  imadd  10841  imsub  10842  immul2  10844  imdivap  10845  cjcj  10847  cjadd  10848  ipcnval  10850  cjmulval  10852  cjneg  10854  imval2  10858  cjreim2  10868  cjap  10870  cnrecnv  10874  caucvgrelemrec  10943  cvg1nlemres  10949  recvguniqlem  10958  recvguniq  10959  resqrexlemover  10974  resqrexlemcalc1  10978  resqrexlemcalc2  10979  resqrexlemcalc3  10980  resqrexlemnmsq  10981  resqrexlemnm  10982  resqrexlemgt0  10984  resqrexlemoverl  10985  resqrexlemglsq  10986  remsqsqrt  10996  sqrtmul  10999  sqrtdiv  11006  sqrtmsq  11009  abs00ap  11026  absext  11027  abs00  11028  absdivap  11034  absid  11035  absexp  11043  absexpzap  11044  absimle  11048  abslt  11052  absle  11053  abssubap0  11054  abssubne0  11055  releabs  11060  recvalap  11061  abstri  11068  abs2difabs  11072  amgm2  11082  icodiamlt  11144  maxabsle  11168  maxabslemab  11170  maxabslemlub  11171  maxabslemval  11172  maxcl  11174  maxltsup  11182  max0addsup  11183  minmax  11193  minabs  11199  minclpr  11200  bdtrilem  11202  bdtri  11203  mul0inf  11204  mingeb  11205  climabs0  11270  reccn2ap  11276  climrecl  11287  climge0  11288  climle  11297  climsqz  11298  climsqz2  11299  climlec2  11304  climrecvg1n  11311  climcvg1nlem  11312  isumrecl  11392  isumge0  11393  fsumlessfi  11423  fsumge1  11424  fsum00  11425  fsumle  11426  fsumlt  11427  fsumabs  11428  iserabs  11438  isumrpcl  11457  isumle  11458  isumlessdc  11459  trireciplem  11463  trirecip  11464  expcnvre  11466  expcnv  11467  explecnv  11468  absltap  11472  geo2sum  11477  cvgratnnlembern  11486  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  cvgratnnlemabsle  11490  cvgratnnlemsumlt  11491  cvgratnnlemfm  11492  cvgratnnlemrate  11493  cvgratz  11495  mertenslemi1  11498  mertenslem2  11499  fprodabs  11579  fprodle  11603  efcllemp  11621  ege2le3  11634  efaddlem  11637  efgt0  11647  reeftlcl  11652  eftlub  11653  effsumlt  11655  efltim  11661  eflegeo  11664  resin4p  11681  recos4p  11682  efeul  11697  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  cos12dec  11730  absefi  11731  absef  11732  absefib  11733  efieq1re  11734  eirraplem  11739  dvdslelemd  11803  odd2np1  11832  divalglemnqt  11879  infssuzcldc  11906  nn0seqcvgd  11995  sqnprm  12090  isprm5lem  12095  odzdvds  12199  pythagtriplem14  12231  pcid  12277  fldivp1  12300  pockthlem  12308  4sqlem5  12334  4sqlem10  12339  mul4sqlem  12345  metrtri  13171  bl2in  13197  blhalf  13202  blssps  13221  blss  13222  dedekindeu  13395  dedekindicclemicc  13404  ivthinclemlopn  13408  ivthinclemuopn  13410  ivthinc  13415  ivthdec  13416  dvcjbr  13466  dvfre  13468  dveflem  13481  reeff1olem  13486  reeff1oleme  13487  eflt  13490  sin0pilem1  13496  sin0pilem2  13497  pilem3  13498  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  sinq34lt0t  13546  cosq14gt0  13547  cosq23lt0  13548  coseq0q4123  13549  coseq0negpitopi  13551  tanrpcl  13552  tangtx  13553  coskpi  13563  cosordlem  13564  cosq34lt1  13565  cos11  13568  reexplog  13586  relogexp  13587  logdivlti  13596  rpcxpef  13609  rpcncxpcl  13617  cxpap0  13619  rpcxpadd  13620  rpmulcxp  13624  cxpmul  13627  abscxp  13629  cxplt  13630  cxplt3  13634  logsqrt  13637  apcxp2  13652  rpabscxpbnd  13653  rplogbid1  13659  rplogb1  13660  rpelogb  13661  rplogbchbase  13662  rplogbreexp  13665  rprelogbmul  13667  rprelogbdiv  13669  rplogbcxp  13675  rpcxplogb  13676  logbgcd1irraplemexp  13680  logbgcd1irraplemap  13681  lgsvalmod  13714  lgsdilem  13722  lgsne0  13733  2sqlem1  13744  mul2sq  13746  2sqlem3  13747  2sqlem8  13753  qdencn  14059  refeq  14060  cvgcmp2nlemabs  14064  cvgcmp2n  14065  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trirec0  14076  apdifflemf  14078  apdifflemr  14079  apdiff  14080  redc0  14089  reap0  14090  nconstwlpolem0  14094  nconstwlpolemgt0  14095