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 9900 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | |
4 | 1, 2, 3 | mp2an 704 | 1 ⊢ (𝐴 · 𝐵) ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 (class class class)co 6549 ℝcr 9814 · cmul 9820 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-mulrcl 9878 |
This theorem depends on definitions: df-bi 196 df-an 385 |
This theorem is referenced by: ledivp1i 10828 ltdivp1i 10829 addltmul 11145 nn0lele2xi 11225 numltc 11404 decleOLD 11419 nn0opthlem2 12918 faclbnd4lem1 12942 ef01bndlem 14753 cos2bnd 14757 sin4lt0 14764 dvdslelem 14869 divalglem1 14955 divalglem6 14959 sincosq3sgn 24056 sincosq4sgn 24057 sincos4thpi 24069 efif1olem1 24092 efif1olem2 24093 efif1olem4 24095 efif1o 24096 efifo 24097 ang180lem1 24339 ang180lem2 24340 log2ublem1 24473 log2ublem2 24474 bpos1lem 24807 bposlem7 24815 bposlem8 24816 bposlem9 24817 chebbnd1lem3 24960 chebbnd1 24961 chto1ub 24965 siilem1 27090 normlem6 27356 normlem7 27357 norm-ii-i 27378 bcsiALT 27420 nmopadjlem 28332 nmopcoi 28338 bdopcoi 28341 nmopcoadji 28344 unierri 28347 problem5 30817 circum 30822 iexpire 30874 taupi 32346 sin2h 32569 tan2h 32571 sumnnodd 38697 sinaover2ne0 38751 stirlinglem11 38977 dirkerper 38989 dirkercncflem2 38997 dirkercncflem4 38999 fourierdlem24 39024 fourierdlem43 39043 fourierdlem44 39044 fourierdlem68 39067 fourierdlem94 39093 fourierdlem111 39110 fourierdlem113 39112 sqwvfoura 39121 sqwvfourb 39122 fourierswlem 39123 fouriersw 39124 lighneallem4a 40063 tgoldbach 40232 tgoldbachOLD 40239 |
Copyright terms: Public domain | W3C validator |