Theorem remulcli 11302

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

Syntax hints:   ∈ wcel 2103  (class class class)co 7445  ℝcr 11179   · cmul 11185

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

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  ledivp1i  12216  ltdivp1i  12217  addltmul  12525  nn0lele2xi  12604  10re  12773  numltc  12780  nn0opthlem2  14314  faclbnd4lem1  14338  ef01bndlem  16226  cos2bnd  16230  sin4lt0  16237  dvdslelem  16351  divalglem1  16436  divalglem6  16440  sincosq3sgn  26552  sincosq4sgn  26553  sincos4thpi  26565  cos02pilt1  26577  cosq34lt1  26578  cos0pilt1  26583  efif1olem1  26593  efif1olem2  26594  efif1olem4  26596  efif1o  26597  efifo  26598  ang180lem1  26861  ang180lem2  26862  log2ublem1  26998  log2ublem2  26999  bpos1lem  27335  bposlem7  27343  bposlem8  27344  bposlem9  27345  chebbnd1lem3  27524  chebbnd1  27525  chto1ub  27529  siilem1  30874  normlem6  31138  normlem7  31139  norm-ii-i  31160  bcsiALT  31202  nmopadjlem  32112  nmopcoi  32118  bdopcoi  32121  nmopcoadji  32124  unierri  32127  dpmul4  32870  hgt750lem  34620  hgt750lem2  34621  hgt750leme  34627  problem5  35629  circum  35634  iexpire  35689  taupi  37237  sin2h  37518  tan2h  37520  sumnnodd  45485  sinaover2ne0  45723  stirlinglem11  45939  dirkerper  45951  dirkercncflem2  45959  dirkercncflem4  45961  fourierdlem24  45986  fourierdlem43  46005  fourierdlem44  46006  fourierdlem68  46029  fourierdlem94  46055  fourierdlem111  46072  fourierdlem113  46074  sqwvfoura  46083  sqwvfourb  46084  fourierswlem  46085  fouriersw  46086  lighneallem4a  47414  tgoldbach  47623