Theorem remulcli 11242

Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)

Hypotheses

Ref	Expression
recni.1	⊢ 𝐴 ∈ ℝ
axri.2	⊢ 𝐵 ∈ ℝ

Assertion

Ref	Expression
remulcli	⊢ (𝐴 · 𝐵) ∈ ℝ

Proof of Theorem remulcli

Step	Hyp	Ref	Expression
1		recni.1	. 2 ⊢ 𝐴 ∈ ℝ
2		axri.2	. 2 ⊢ 𝐵 ∈ ℝ
3		remulcl 11202	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 · 𝐵) ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116   · cmul 11122

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11180

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ledivp1i  12157  ltdivp1i  12158  addltmul  12497  nn0lele2xi  12577  10re  12752  numltc  12760  nn0opthlem2  14325  faclbnd4lem1  14349  ef01bndlem  16264  cos2bnd  16268  sin4lt0  16275  dvdslelem  16391  divalglem1  16476  divalglem6  16480  2pire  26673  sincosq3sgn  26718  sincosq4sgn  26719  sincos4thpi  26731  cos02pilt1  26744  cosq34lt1  26745  cos0pilt1  26750  efif1olem1  26760  efif1olem2  26761  efif1olem4  26763  efif1o  26764  efifo  26765  ang180lem1  27027  ang180lem2  27028  log2ublem1  27164  log2ublem2  27165  bpos1lem  27499  bposlem7  27507  bposlem8  27508  bposlem9  27509  chebbnd1lem3  27688  chebbnd1  27689  chto1ub  27693  siilem1  31276  normlem6  31540  normlem7  31541  norm-ii-i  31562  bcsiALT  31604  nmopadjlem  32514  nmopcoi  32520  bdopcoi  32523  nmopcoadji  32526  unierri  32529  dpmul4  33305  hgt750lem  35105  hgt750lem2  35106  hgt750leme  35112  problem5  36200  circum  36205  iexpire  36266  taupi  38026  sin2h  38320  tan2h  38322  sumnnodd  46406  sinaover2ne0  46642  stirlinglem11  46858  dirkercncflem4  46880  fourierdlem24  46905  fourierdlem43  46924  fourierdlem44  46925  fourierdlem68  46948  fourierdlem94  46974  fourierdlem111  46991  sqwvfoura  47002  sqwvfourb  47003  fourierswlem  47004  fouriersw  47005  goldrarr  47678  lighneallem4a  48420  tgoldbach  48642