Theorem remulcli 11278

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

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℝcr 11155   · cmul 11161

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

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

This theorem is referenced by:  ledivp1i  12194  ltdivp1i  12195  addltmul  12504  nn0lele2xi  12584  10re  12754  numltc  12761  nn0opthlem2  14309  faclbnd4lem1  14333  ef01bndlem  16221  cos2bnd  16225  sin4lt0  16232  dvdslelem  16347  divalglem1  16432  divalglem6  16436  sincosq3sgn  26543  sincosq4sgn  26544  sincos4thpi  26556  cos02pilt1  26569  cosq34lt1  26570  cos0pilt1  26575  efif1olem1  26585  efif1olem2  26586  efif1olem4  26588  efif1o  26589  efifo  26590  ang180lem1  26853  ang180lem2  26854  log2ublem1  26990  log2ublem2  26991  bpos1lem  27327  bposlem7  27335  bposlem8  27336  bposlem9  27337  chebbnd1lem3  27516  chebbnd1  27517  chto1ub  27521  siilem1  30871  normlem6  31135  normlem7  31136  norm-ii-i  31157  bcsiALT  31199  nmopadjlem  32109  nmopcoi  32115  bdopcoi  32118  nmopcoadji  32121  unierri  32124  dpmul4  32897  hgt750lem  34667  hgt750lem2  34668  hgt750leme  34674  problem5  35675  circum  35680  iexpire  35736  taupi  37325  sin2h  37618  tan2h  37620  sumnnodd  45650  sinaover2ne0  45888  stirlinglem11  46104  dirkerper  46116  dirkercncflem2  46124  dirkercncflem4  46126  fourierdlem24  46151  fourierdlem43  46170  fourierdlem44  46171  fourierdlem68  46194  fourierdlem94  46220  fourierdlem111  46237  fourierdlem113  46239  sqwvfoura  46248  sqwvfourb  46249  fourierswlem  46250  fouriersw  46251  lighneallem4a  47600  tgoldbach  47809