Theorem remulcli 10814

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 10779	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 · 𝐵) ∈ ℝ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℝcr 10693   · cmul 10699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 10757

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  ledivp1i  11722  ltdivp1i  11723  addltmul  12031  nn0lele2xi  12110  10re  12277  numltc  12284  nn0opthlem2  13800  faclbnd4lem1  13824  ef01bndlem  15708  cos2bnd  15712  sin4lt0  15719  dvdslelem  15833  divalglem1  15918  divalglem6  15922  sincosq3sgn  25344  sincosq4sgn  25345  sincos4thpi  25357  cos02pilt1  25369  cosq34lt1  25370  cos0pilt1  25375  efif1olem1  25385  efif1olem2  25386  efif1olem4  25388  efif1o  25389  efifo  25390  ang180lem1  25646  ang180lem2  25647  log2ublem1  25783  log2ublem2  25784  bpos1lem  26117  bposlem7  26125  bposlem8  26126  bposlem9  26127  chebbnd1lem3  26306  chebbnd1  26307  chto1ub  26311  siilem1  28886  normlem6  29150  normlem7  29151  norm-ii-i  29172  bcsiALT  29214  nmopadjlem  30124  nmopcoi  30130  bdopcoi  30133  nmopcoadji  30136  unierri  30139  dpmul4  30862  hgt750lem  32297  hgt750lem2  32298  hgt750leme  32304  problem5  33294  circum  33299  iexpire  33370  taupi  35177  sin2h  35453  tan2h  35455  sumnnodd  42789  sinaover2ne0  43027  stirlinglem11  43243  dirkerper  43255  dirkercncflem2  43263  dirkercncflem4  43265  fourierdlem24  43290  fourierdlem43  43309  fourierdlem44  43310  fourierdlem68  43333  fourierdlem94  43359  fourierdlem111  43376  fourierdlem113  43378  sqwvfoura  43387  sqwvfourb  43388  fourierswlem  43389  fouriersw  43390  lighneallem4a  44676  tgoldbach  44885