Theorem remulcli 11153

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

Syntax hints:   ∈ wcel 2119  (class class class)co 7357  ℝcr 11029   · cmul 11035

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

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  ledivp1i  12073  ltdivp1i  12074  addltmul  12405  nn0lele2xi  12485  10re  12655  numltc  12662  nn0opthlem2  14223  faclbnd4lem1  14247  ef01bndlem  16143  cos2bnd  16147  sin4lt0  16154  dvdslelem  16270  divalglem1  16355  divalglem6  16359  sincosq3sgn  26483  sincosq4sgn  26484  sincos4thpi  26496  cos02pilt1  26509  cosq34lt1  26510  cos0pilt1  26515  efif1olem1  26525  efif1olem2  26526  efif1olem4  26528  efif1o  26529  efifo  26530  ang180lem1  26792  ang180lem2  26793  log2ublem1  26929  log2ublem2  26930  bpos1lem  27264  bposlem7  27272  bposlem8  27273  bposlem9  27274  chebbnd1lem3  27453  chebbnd1  27454  chto1ub  27458  siilem1  30941  normlem6  31205  normlem7  31206  norm-ii-i  31227  bcsiALT  31269  nmopadjlem  32179  nmopcoi  32185  bdopcoi  32188  nmopcoadji  32191  unierri  32194  dpmul4  32993  hgt750lem  34844  hgt750lem2  34845  hgt750leme  34851  problem5  35906  circum  35911  iexpire  35972  taupi  37692  sin2h  37986  tan2h  37988  sumnnodd  46083  sinaover2ne0  46319  stirlinglem11  46535  dirkerper  46547  dirkercncflem2  46555  dirkercncflem4  46557  fourierdlem24  46582  fourierdlem43  46601  fourierdlem44  46602  fourierdlem68  46625  fourierdlem94  46651  fourierdlem111  46668  fourierdlem113  46670  sqwvfoura  46679  sqwvfourb  46680  fourierswlem  46681  fouriersw  46682  goldrarr  47352  lighneallem4a  48094  tgoldbach  48316