Theorem remulcli 11128

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

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℝcr 11005   · cmul 11011

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

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

This theorem is referenced by:  ledivp1i  12047  ltdivp1i  12048  addltmul  12357  nn0lele2xi  12437  10re  12607  numltc  12614  nn0opthlem2  14176  faclbnd4lem1  14200  ef01bndlem  16093  cos2bnd  16097  sin4lt0  16104  dvdslelem  16220  divalglem1  16305  divalglem6  16309  sincosq3sgn  26436  sincosq4sgn  26437  sincos4thpi  26449  cos02pilt1  26462  cosq34lt1  26463  cos0pilt1  26468  efif1olem1  26478  efif1olem2  26479  efif1olem4  26481  efif1o  26482  efifo  26483  ang180lem1  26746  ang180lem2  26747  log2ublem1  26883  log2ublem2  26884  bpos1lem  27220  bposlem7  27228  bposlem8  27229  bposlem9  27230  chebbnd1lem3  27409  chebbnd1  27410  chto1ub  27414  siilem1  30831  normlem6  31095  normlem7  31096  norm-ii-i  31117  bcsiALT  31159  nmopadjlem  32069  nmopcoi  32075  bdopcoi  32078  nmopcoadji  32081  unierri  32084  dpmul4  32894  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  problem5  35713  circum  35718  iexpire  35779  taupi  37367  sin2h  37660  tan2h  37662  sumnnodd  45740  sinaover2ne0  45976  stirlinglem11  46192  dirkerper  46204  dirkercncflem2  46212  dirkercncflem4  46214  fourierdlem24  46239  fourierdlem43  46258  fourierdlem44  46259  fourierdlem68  46282  fourierdlem94  46308  fourierdlem111  46325  fourierdlem113  46327  sqwvfoura  46336  sqwvfourb  46337  fourierswlem  46338  fouriersw  46339  lighneallem4a  47718  tgoldbach  47927