![]() |
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 7917 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ) | |
4 | 1, 2, 3 | mp2an 426 | 1 ⊢ (𝐴 · 𝐵) ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2148 (class class class)co 5868 ℝcr 7788 · cmul 7794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 ax-mulrcl 7888 |
This theorem is referenced by: addltmul 9131 nn0lele2xi 9203 numltc 9385 ef01bndlem 11735 cos2bnd 11739 sin4lt0 11745 sincosq3sgn 13882 sincosq4sgn 13883 cosq23lt0 13887 coseq0q4123 13888 coseq00topi 13889 coseq0negpitopi 13890 sincos4thpi 13894 cosq34lt1 13904 cos02pilt1 13905 cos0pilt1 13906 taupi 14441 |
Copyright terms: Public domain | W3C validator |