This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-mulgt1d

Description: mulgt1d without ax-mulcom . (Contributed by SN, 26-Jun-2024)

Ref Expression
Hypotheses sn-mulgt1d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
sn-mulgt1d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
sn-mulgt1d.1 ⊢ ( 𝜑 → 1 < 𝐴 )
sn-mulgt1d.2 ⊢ ( 𝜑 → 1 < 𝐵 )
Assertion sn-mulgt1d ( 𝜑 → 1 < ( 𝐴 · 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sn-mulgt1d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 sn-mulgt1d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 sn-mulgt1d.1 ⊢ ( 𝜑 → 1 < 𝐴 )
4 sn-mulgt1d.2 ⊢ ( 𝜑 → 1 < 𝐵 )
5 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
6 1 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
7 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
8 sn-0lt1 ⊢ 0 < 1
9 8 a1i ⊢ ( 𝜑 → 0 < 1 )
10 7 5 1 9 3 lttrd ⊢ ( 𝜑 → 0 < 𝐴 )
11 2 1 10 sn-ltmulgt11d ⊢ ( 𝜑 → ( 1 < 𝐵 ↔ 𝐴 < ( 𝐴 · 𝐵 ) ) )
12 4 11 mpbid ⊢ ( 𝜑 → 𝐴 < ( 𝐴 · 𝐵 ) )
13 5 1 6 3 12 lttrd ⊢ ( 𝜑 → 1 < ( 𝐴 · 𝐵 ) )