Theorem remulcli 11325

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

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulrcl 11263

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ledivp1i  12242  ltdivp1i  12243  addltmul  12582  nn0lele2xi  12662  10re  12837  numltc  12845  nn0opthlem2  14413  faclbnd4lem1  14437  ef01bndlem  16352  cos2bnd  16356  sin4lt0  16363  dvdslelem  16479  divalglem1  16564  divalglem6  16568  2pire  26784  sincosq3sgn  26829  sincosq4sgn  26830  sincos4thpi  26842  cos02pilt1  26854  cosq34lt1  26855  cos0pilt1  26860  efif1olem1  26870  efif1olem2  26871  efif1o  26874  efifo  26875  ang180lem1  27137  ang180lem2  27138  log2ublem1  27274  log2ublem2  27275  bpos1lem  27609  bposlem7  27617  bposlem8  27618  bposlem9  27619  chebbnd1lem3  27798  chebbnd1  27799  chto1ub  27803  siilem1  31453  normlem6  31717  normlem7  31718  norm-ii-i  31739  bcsiALT  31781  nmopadjlem  32691  nmopcoi  32697  bdopcoi  32700  nmopcoadji  32703  unierri  32706  dpmul4  33480  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  problem5  36434  circum  36439  iexpire  36500  taupi  38244  sin2h  38533  tan2h  38535  sumnnodd  46641  sinaover2ne0  46877  stirlinglem11  47093  dirkercncflem4  47115  fourierdlem24  47140  fourierdlem43  47159  fourierdlem44  47160  fourierdlem68  47183  fourierdlem94  47209  fourierdlem111  47226  sqwvfoura  47237  sqwvfourb  47238  fourierswlem  47239  fouriersw  47240  goldrarr  47927  goldratval  47935  lighneallem4a  48692  tgoldbach  48914