Theorem remulcli 11234

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

Syntax hints:   ∈ wcel 2098  (class class class)co 7405  ℝcr 11111   · cmul 11117

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

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

This theorem is referenced by:  ledivp1i  12143  ltdivp1i  12144  addltmul  12452  nn0lele2xi  12531  10re  12700  numltc  12707  nn0opthlem2  14234  faclbnd4lem1  14258  ef01bndlem  16134  cos2bnd  16138  sin4lt0  16145  dvdslelem  16259  divalglem1  16344  divalglem6  16348  sincosq3sgn  26390  sincosq4sgn  26391  sincos4thpi  26403  cos02pilt1  26415  cosq34lt1  26416  cos0pilt1  26421  efif1olem1  26431  efif1olem2  26432  efif1olem4  26434  efif1o  26435  efifo  26436  ang180lem1  26696  ang180lem2  26697  log2ublem1  26833  log2ublem2  26834  bpos1lem  27170  bposlem7  27178  bposlem8  27179  bposlem9  27180  chebbnd1lem3  27359  chebbnd1  27360  chto1ub  27364  siilem1  30613  normlem6  30877  normlem7  30878  norm-ii-i  30899  bcsiALT  30941  nmopadjlem  31851  nmopcoi  31857  bdopcoi  31860  nmopcoadji  31863  unierri  31866  dpmul4  32585  hgt750lem  34192  hgt750lem2  34193  hgt750leme  34199  problem5  35182  circum  35187  iexpire  35238  taupi  36711  sin2h  36991  tan2h  36993  sumnnodd  44918  sinaover2ne0  45156  stirlinglem11  45372  dirkerper  45384  dirkercncflem2  45392  dirkercncflem4  45394  fourierdlem24  45419  fourierdlem43  45438  fourierdlem44  45439  fourierdlem68  45462  fourierdlem94  45488  fourierdlem111  45505  fourierdlem113  45507  sqwvfoura  45516  sqwvfourb  45517  fourierswlem  45518  fouriersw  45519  lighneallem4a  46848  tgoldbach  47057