Theorem remulcli 11160

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

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037   · cmul 11043

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

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

This theorem is referenced by:  ledivp1i  12079  ltdivp1i  12080  addltmul  12389  nn0lele2xi  12469  10re  12638  numltc  12645  nn0opthlem2  14204  faclbnd4lem1  14228  ef01bndlem  16121  cos2bnd  16125  sin4lt0  16132  dvdslelem  16248  divalglem1  16333  divalglem6  16337  sincosq3sgn  26480  sincosq4sgn  26481  sincos4thpi  26493  cos02pilt1  26506  cosq34lt1  26507  cos0pilt1  26512  efif1olem1  26522  efif1olem2  26523  efif1olem4  26525  efif1o  26526  efifo  26527  ang180lem1  26790  ang180lem2  26791  log2ublem1  26927  log2ublem2  26928  bpos1lem  27264  bposlem7  27272  bposlem8  27273  bposlem9  27274  chebbnd1lem3  27453  chebbnd1  27454  chto1ub  27458  siilem1  30943  normlem6  31207  normlem7  31208  norm-ii-i  31229  bcsiALT  31271  nmopadjlem  32181  nmopcoi  32187  bdopcoi  32190  nmopcoadji  32193  unierri  32196  dpmul4  33010  hgt750lem  34833  hgt750lem2  34834  hgt750leme  34840  problem5  35889  circum  35894  iexpire  35955  taupi  37582  sin2h  37865  tan2h  37867  sumnnodd  45994  sinaover2ne0  46230  stirlinglem11  46446  dirkerper  46458  dirkercncflem2  46466  dirkercncflem4  46468  fourierdlem24  46493  fourierdlem43  46512  fourierdlem44  46513  fourierdlem68  46536  fourierdlem94  46562  fourierdlem111  46579  fourierdlem113  46581  sqwvfoura  46590  sqwvfourb  46591  fourierswlem  46592  fouriersw  46593  lighneallem4a  47972  tgoldbach  48181