Theorem recnd 8318

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

Syntax hints:   → wi 4   ∈ wcel 2205  ℂcc 8141  ℝcr 8142

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  readdcan  8430  ltadd2  8711  ltadd1  8721  leadd2  8723  ltsubadd  8724  ltsubadd2  8725  lesubadd  8726  lesubadd2  8727  ltaddsub  8728  leaddsub  8730  lesub1  8748  lesub2  8749  ltsub1  8750  ltsub2  8751  ltnegcon1  8755  ltnegcon2  8756  add20  8766  subge0  8767  suble0  8768  lesub0  8771  eqord2  8776  possumd  8861  sublt0d  8862  rimul  8877  rereim  8878  apreap  8879  ltmul1a  8883  ltmul1  8884  reapmul1  8887  remulext2  8892  cru  8894  apreim  8895  mulreim  8896  apadd1  8900  apneg  8903  mulext1  8904  ltapd  8930  aprcl  8938  aptap  8942  rerecclap  9024  redivclap  9025  recgt0  9144  prodgt0gt0  9145  prodgt0  9146  prodge0  9148  lemul1a  9152  ltdiv1  9162  ltmuldiv  9168  ledivmul  9171  lt2mul2div  9173  ltrec  9177  lt2msq  9180  ltdiv2  9181  ltrec1  9182  lerec2  9183  ledivdiv  9184  lediv2  9185  ltdiv23  9186  lediv23  9187  lediv12a  9188  recp1lt1  9193  recreclt  9194  ledivp1  9197  mulle0r  9238  negiso  9249  avglt1  9497  avglt2  9498  div4p1lem1div2  9512  nn0cnd  9575  zcn  9602  peano2z  9633  zaddcllemneg  9636  ztri3or  9640  zeo  9704  zcnd  9722  eluzmn  9881  eluzelcn  9886  infrenegsupex  9947  supinfneg  9948  infsupneg  9949  supminfex  9950  irrmulap  10001  cnref1o  10004  rpcn  10016  rpcnd  10052  ltaddrp2d  10085  mul2lt0rlt0  10113  mul2lt0rgt0  10114  mul2lt0llt0  10115  mul2lt0lgt0  10116  mul2lt0np  10117  mul2lt0pn  10118  xpncan  10226  icoshftf1o  10346  lincmb01cmp  10358  lincmble  10359  iccf1o  10360  infssuzcldc  10620  qbtwnrelemcalc  10642  flhalf  10689  intfracq  10709  flqdiv  10710  modqid  10738  modqid0  10739  mulqaddmodid  10753  seqf1oglem1  10908  ser3le  10926  expcl2lemap  10940  expnegzap  10962  expaddzaplem  10971  expaddzap  10972  expmulzap  10974  ltexp2a  10980  leexp2a  10981  leexp2r  10982  exple1  10984  expubnd  10985  sq11  11001  resq01  11047  bernneq2  11051  expnbnd  11053  nn0ltexp2  11099  nn0opthlem2d  11111  faclbnd  11131  bcp1nk  11152  bcm1n  11159  remim  11573  reim0b  11575  rereb  11576  mulreap  11577  cjreb  11579  recj  11580  reneg  11581  readd  11582  resub  11583  remullem  11584  remul2  11586  redivap  11587  imcj  11588  imneg  11589  imadd  11590  imsub  11591  immul2  11593  imdivap  11594  cjcj  11596  cjadd  11597  ipcnval  11599  cjmulval  11601  cjneg  11603  imval2  11607  cjreim2  11617  cjap  11619  cnrecnv  11623  caucvgrelemrec  11692  cvg1nlemres  11698  recvguniqlem  11707  recvguniq  11708  resqrexlemover  11723  resqrexlemcalc1  11727  resqrexlemcalc2  11728  resqrexlemcalc3  11729  resqrexlemnmsq  11730  resqrexlemnm  11731  resqrexlemgt0  11733  resqrexlemoverl  11734  resqrexlemglsq  11735  remsqsqrt  11745  sqrtmul  11748  sqrtdiv  11755  sqrtmsq  11758  abs00ap  11775  absext  11776  abs00  11777  absdivap  11783  absid  11784  absexp  11792  absexpzap  11793  absimle  11797  abslt  11801  absle  11802  abssubap0  11803  abssubne0  11804  releabs  11809  recvalap  11810  abstri  11817  abs2difabs  11821  amgm2  11831  icodiamlt  11893  maxabsle  11917  maxabslemab  11919  maxabslemlub  11920  maxabslemval  11921  maxcl  11923  maxltsup  11931  max0addsup  11932  minmax  11943  minabs  11949  minclpr  11950  bdtrilem  11952  bdtri  11953  mul0inf  11954  mingeb  11955  climabs0  12020  reccn2ap  12026  climrecl  12037  climge0  12038  climle  12047  climsqz  12048  climsqz2  12049  climlec2  12054  climrecvg1n  12061  climcvg1nlem  12062  isumrecl  12143  isumge0  12144  fsumlessfi  12174  fsumge1  12175  fsum00  12176  fsumle  12177  fsumlt  12178  fsumabs  12179  iserabs  12189  isumrpcl  12208  isumle  12209  isumlessdc  12210  trireciplem  12214  trirecip  12215  expcnvre  12217  expcnv  12218  explecnv  12219  absltap  12223  geo2sum  12228  cvgratnnlembern  12237  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  cvgratnnlemabsle  12241  cvgratnnlemsumlt  12242  cvgratnnlemfm  12243  cvgratnnlemrate  12244  cvgratz  12246  mertenslemi1  12249  mertenslem2  12250  fprodabs  12330  fprodle  12354  efcllemp  12372  ege2le3  12385  efaddlem  12388  efgt0  12398  reeftlcl  12403  eftlub  12404  effsumlt  12406  efltim  12412  eflegeo  12415  resin4p  12432  recos4p  12433  efeul  12448  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  sin01gt0  12476  cos01gt0  12477  sin02gt0  12478  cos12dec  12482  absefi  12483  absef  12484  absefib  12485  efieq1re  12486  eirraplem  12491  dvdsaddre2b  12555  dvdslelemd  12557  odd2np1  12587  divalglemnqt  12634  bitsp1o  12667  bitsfzo  12669  bitscmp  12672  nn0seqcvgd  12766  sqnprm  12861  isprm5lem  12866  odzdvds  12971  pythagtriplem14  13003  pcid  13050  fldivp1  13074  pockthlem  13082  4sqlem5  13108  4sqlem10  13113  mul4sqlem  13119  4sqlem15  13131  4sqlem16  13132  ballotfilemsi  13205  mulgneg  13896  ghmmulg  14012  rege0subm  14861  metrtri  15371  bl2in  15397  blhalf  15402  blssps  15421  blss  15422  maxcncf  15609  mincncf  15610  dedekindeu  15617  dedekindicclemicc  15626  ivthinclemlopn  15630  ivthinclemuopn  15632  ivthinc  15637  ivthdec  15638  ivthreinc  15639  dvconstre  15690  dvidre  15691  dvcjbr  15702  dvfre  15704  dveflem  15720  plyrecj  15757  reeff1olem  15765  reeff1oleme  15766  eflt  15769  sin0pilem1  15775  sin0pilem2  15776  pilem3  15777  sincosq2sgn  15821  sincosq3sgn  15822  sincosq4sgn  15823  sinq12gt0  15824  sinq34lt0t  15825  cosq14gt0  15826  cosq23lt0  15827  coseq0q4123  15828  coseq0negpitopi  15830  tanrpcl  15831  tangtx  15832  coskpi  15842  cosordlem  15843  cosq34lt1  15844  cos11  15847  reexplog  15865  relogexp  15866  logdivlti  15875  rpcxpef  15888  rpcncxpcl  15896  cxpap0  15898  rpcxpadd  15899  rpmulcxp  15903  cxpmul  15906  abscxp  15909  cxplt  15910  cxplt3  15914  logsqrt  15917  apcxp2  15933  rpabscxpbnd  15934  rplogbid1  15941  rplogb1  15942  rpelogb  15943  rplogbchbase  15944  rplogbreexp  15947  rprelogbmul  15949  rprelogbdiv  15951  rplogbcxp  15957  rpcxplogb  15958  logbgcd1irraplemexp  15962  logbgcd1irraplemap  15963  pellexlem2  15975  mersenne  15994  lgsvalmod  16021  lgsdilem  16029  lgsne0  16040  gausslemma2dlem1a  16060  gausslemma2dlem6  16069  lgseisenlem1  16072  lgseisenlem2  16073  lgseisen  16076  lgsquadlem1  16079  lgsquadlem2  16080  2sqlem1  16116  mul2sq  16118  2sqlem3  16119  2sqlem8  16125  dichmul0orlem1  16636  dichmul0orlem4  16639  dichmul0orlem5  16640  dichmul0orlem6  16641  dichmul0orlem7  16642  qdencn  16946  refeq  16947  repiecele0  16949  repiecege0  16950  cvgcmp2nlemabs  16955  cvgcmp2n  16956  trilpolemisumle  16961  trilpolemeq1  16963  trilpolemlt1  16964  trirec0  16967  apdifflemf  16969  apdifflemr  16970  apdiff  16971  qdiff  16972  redc0  16981  reap0  16982  cndcap  16983  nconstwlpolem0  16988  nconstwlpolemgt0  16989  neap0mkv  16994  ltlenmkv  16995