![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > remulcli | 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 7969 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | |
4 | 1, 2, 3 | mp2an 426 | 1 ⊢ (𝐴 · 𝐵) ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 (class class class)co 5896 ℝcr 7840 · cmul 7846 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-mulrcl 7940 |
This theorem is referenced by: addltmul 9185 nn0lele2xi 9257 numltc 9439 ef01bndlem 11796 cos2bnd 11800 sin4lt0 11806 sincosq3sgn 14706 sincosq4sgn 14707 cosq23lt0 14711 coseq0q4123 14712 coseq00topi 14713 coseq0negpitopi 14714 sincos4thpi 14718 cosq34lt1 14728 cos02pilt1 14729 cos0pilt1 14730 taupi 15280 |
Copyright terms: Public domain | W3C validator |