Theorem recnd 7918

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

Syntax hints:   → wi 4   ∈ wcel 2135  ℂcc 7742  ℝcr 7743

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-11 1493  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-resscn 7836

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-in 3117  df-ss 3124

This theorem is referenced by:  readdcan  8029  ltadd2  8308  ltadd1  8318  leadd2  8320  ltsubadd  8321  ltsubadd2  8322  lesubadd  8323  lesubadd2  8324  ltaddsub  8325  leaddsub  8327  lesub1  8345  lesub2  8346  ltsub1  8347  ltsub2  8348  ltnegcon1  8352  ltnegcon2  8353  add20  8363  subge0  8364  suble0  8365  lesub0  8368  eqord2  8373  possumd  8458  sublt0d  8459  rimul  8474  rereim  8475  apreap  8476  ltmul1a  8480  ltmul1  8481  reapmul1  8484  remulext2  8489  cru  8491  apreim  8492  mulreim  8493  apadd1  8497  apneg  8500  mulext1  8501  ltapd  8527  aprcl  8535  rerecclap  8617  redivclap  8618  recgt0  8736  prodgt0gt0  8737  prodgt0  8738  prodge0  8740  lemul1a  8744  ltdiv1  8754  ltmuldiv  8760  ledivmul  8763  lt2mul2div  8765  ltrec  8769  lt2msq  8772  ltdiv2  8773  ltrec1  8774  lerec2  8775  ledivdiv  8776  lediv2  8777  ltdiv23  8778  lediv23  8779  lediv12a  8780  recp1lt1  8785  recreclt  8786  ledivp1  8789  mulle0r  8830  negiso  8841  avglt1  9086  avglt2  9087  div4p1lem1div2  9101  nn0cnd  9160  zcn  9187  peano2z  9218  zaddcllemneg  9221  ztri3or  9225  zeo  9287  zcnd  9305  eluzelcn  9468  infrenegsupex  9523  supinfneg  9524  infsupneg  9525  supminfex  9526  cnref1o  9579  rpcn  9589  rpcnd  9625  ltaddrp2d  9658  mul2lt0rlt0  9686  mul2lt0rgt0  9687  mul2lt0llt0  9688  mul2lt0lgt0  9689  mul2lt0np  9690  mul2lt0pn  9691  xpncan  9798  icoshftf1o  9918  lincmb01cmp  9930  iccf1o  9931  qbtwnrelemcalc  10181  flhalf  10227  intfracq  10245  flqdiv  10246  modqid  10274  modqid0  10275  mulqaddmodid  10289  ser3le  10443  expcl2lemap  10457  expnegzap  10479  expaddzaplem  10488  expaddzap  10489  expmulzap  10491  ltexp2a  10497  leexp2a  10498  leexp2r  10499  exple1  10501  expubnd  10502  sq11  10517  bernneq2  10565  expnbnd  10567  nn0ltexp2  10612  nn0opthlem2d  10623  faclbnd  10643  bcp1nk  10664  remim  10788  reim0b  10790  rereb  10791  mulreap  10792  cjreb  10794  recj  10795  reneg  10796  readd  10797  resub  10798  remullem  10799  remul2  10801  redivap  10802  imcj  10803  imneg  10804  imadd  10805  imsub  10806  immul2  10808  imdivap  10809  cjcj  10811  cjadd  10812  ipcnval  10814  cjmulval  10816  cjneg  10818  imval2  10822  cjreim2  10832  cjap  10834  cnrecnv  10838  caucvgrelemrec  10907  cvg1nlemres  10913  recvguniqlem  10922  recvguniq  10923  resqrexlemover  10938  resqrexlemcalc1  10942  resqrexlemcalc2  10943  resqrexlemcalc3  10944  resqrexlemnmsq  10945  resqrexlemnm  10946  resqrexlemgt0  10948  resqrexlemoverl  10949  resqrexlemglsq  10950  remsqsqrt  10960  sqrtmul  10963  sqrtdiv  10970  sqrtmsq  10973  abs00ap  10990  absext  10991  abs00  10992  absdivap  10998  absid  10999  absexp  11007  absexpzap  11008  absimle  11012  abslt  11016  absle  11017  abssubap0  11018  abssubne0  11019  releabs  11024  recvalap  11025  abstri  11032  abs2difabs  11036  amgm2  11046  icodiamlt  11108  maxabsle  11132  maxabslemab  11134  maxabslemlub  11135  maxabslemval  11136  maxcl  11138  maxltsup  11146  max0addsup  11147  minmax  11157  minabs  11163  minclpr  11164  bdtrilem  11166  bdtri  11167  mul0inf  11168  mingeb  11169  climabs0  11234  reccn2ap  11240  climrecl  11251  climge0  11252  climle  11261  climsqz  11262  climsqz2  11263  climlec2  11268  climrecvg1n  11275  climcvg1nlem  11276  isumrecl  11356  isumge0  11357  fsumlessfi  11387  fsumge1  11388  fsum00  11389  fsumle  11390  fsumlt  11391  fsumabs  11392  iserabs  11402  isumrpcl  11421  isumle  11422  isumlessdc  11423  trireciplem  11427  trirecip  11428  expcnvre  11430  expcnv  11431  explecnv  11432  absltap  11436  geo2sum  11441  cvgratnnlembern  11450  cvgratnnlemnexp  11451  cvgratnnlemmn  11452  cvgratnnlemabsle  11454  cvgratnnlemsumlt  11455  cvgratnnlemfm  11456  cvgratnnlemrate  11457  cvgratz  11459  mertenslemi1  11462  mertenslem2  11463  fprodabs  11543  fprodle  11567  efcllemp  11585  ege2le3  11598  efaddlem  11601  efgt0  11611  reeftlcl  11616  eftlub  11617  effsumlt  11619  efltim  11625  eflegeo  11628  resin4p  11645  recos4p  11646  efeul  11661  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  sin01gt0  11688  cos01gt0  11689  sin02gt0  11690  cos12dec  11694  absefi  11695  absef  11696  absefib  11697  efieq1re  11698  eirraplem  11703  dvdslelemd  11766  odd2np1  11795  divalglemnqt  11842  infssuzcldc  11869  nn0seqcvgd  11952  sqnprm  12047  odzdvds  12154  pythagtriplem14  12186  pcid  12232  fldivp1  12255  metrtri  12918  bl2in  12944  blhalf  12949  blssps  12968  blss  12969  dedekindeu  13142  dedekindicclemicc  13151  ivthinclemlopn  13155  ivthinclemuopn  13157  ivthinc  13162  ivthdec  13163  dvcjbr  13213  dvfre  13215  dveflem  13228  reeff1olem  13233  reeff1oleme  13234  eflt  13237  sin0pilem1  13243  sin0pilem2  13244  pilem3  13245  sincosq2sgn  13289  sincosq3sgn  13290  sincosq4sgn  13291  sinq12gt0  13292  sinq34lt0t  13293  cosq14gt0  13294  cosq23lt0  13295  coseq0q4123  13296  coseq0negpitopi  13298  tanrpcl  13299  tangtx  13300  coskpi  13310  cosordlem  13311  cosq34lt1  13312  cos11  13315  reexplog  13333  relogexp  13334  logdivlti  13343  rpcxpef  13356  rpcncxpcl  13364  cxpap0  13366  rpcxpadd  13367  rpmulcxp  13371  cxpmul  13374  abscxp  13376  cxplt  13377  cxplt3  13381  logsqrt  13384  apcxp2  13399  rpabscxpbnd  13400  rplogbid1  13406  rplogb1  13407  rpelogb  13408  rplogbchbase  13409  rplogbreexp  13412  rprelogbmul  13414  rprelogbdiv  13416  rplogbcxp  13422  rpcxplogb  13423  logbgcd1irraplemexp  13427  logbgcd1irraplemap  13428  qdencn  13740  refeq  13741  cvgcmp2nlemabs  13745  cvgcmp2n  13746  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  trirec0  13757  apdifflemf  13759  apdifflemr  13760  apdiff  13761  redc0  13770  reap0  13771  nconstwlpolem0  13775  nconstwlpolemgt0  13776