![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > remulcli | Structured version Visualization version GIF version |
Description: Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Ref | Expression |
---|---|
recni.1 | ⊢ 𝐴 ∈ ℝ |
axri.2 | ⊢ 𝐵 ∈ ℝ |
Ref | Expression |
---|---|
remulcli | ⊢ (𝐴 · 𝐵) ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recni.1 | . 2 ⊢ 𝐴 ∈ ℝ | |
2 | axri.2 | . 2 ⊢ 𝐵 ∈ ℝ | |
3 | remulcl 10473 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | |
4 | 1, 2, 3 | mp2an 688 | 1 ⊢ (𝐴 · 𝐵) ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 (class class class)co 7021 ℝcr 10387 · cmul 10393 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulrcl 10451 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: ledivp1i 11418 ltdivp1i 11419 addltmul 11726 nn0lele2xi 11805 10re 11971 numltc 11978 nn0opthlem2 13484 faclbnd4lem1 13508 ef01bndlem 15375 cos2bnd 15379 sin4lt0 15386 dvdslelem 15497 divalglem1 15583 divalglem6 15587 sincosq3sgn 24774 sincosq4sgn 24775 sincos4thpi 24787 efif1olem1 24812 efif1olem2 24813 efif1olem4 24815 efif1o 24816 efifo 24817 ang180lem1 25073 ang180lem2 25074 log2ublem1 25211 log2ublem2 25212 bpos1lem 25545 bposlem7 25553 bposlem8 25554 bposlem9 25555 chebbnd1lem3 25734 chebbnd1 25735 chto1ub 25739 siilem1 28324 normlem6 28588 normlem7 28589 norm-ii-i 28610 bcsiALT 28652 nmopadjlem 29562 nmopcoi 29568 bdopcoi 29571 nmopcoadji 29574 unierri 29577 dpmul4 30279 hgt750lem 31544 hgt750lem2 31545 hgt750leme 31551 problem5 32526 circum 32531 iexpire 32581 taupi 34160 sin2h 34438 tan2h 34440 sumnnodd 41478 sinaover2ne0 41716 stirlinglem11 41937 dirkerper 41949 dirkercncflem2 41957 dirkercncflem4 41959 fourierdlem24 41984 fourierdlem43 42003 fourierdlem44 42004 fourierdlem68 42027 fourierdlem94 42053 fourierdlem111 42070 fourierdlem113 42072 sqwvfoura 42081 sqwvfourb 42082 fourierswlem 42083 fouriersw 42084 lighneallem4a 43281 tgoldbach 43490 |
Copyright terms: Public domain | W3C validator |