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 ⊢ φ → A ∈ ℝ
sn-mulgt1d.b ⊢ φ → B ∈ ℝ
sn-mulgt1d.1 ⊢ φ → 1 < A
sn-mulgt1d.2 ⊢ φ → 1 < B
Assertion sn-mulgt1d ⊢ φ → 1 < A ⁢ B

Proof

Step Hyp Ref Expression
1 sn-mulgt1d.a ⊢ φ → A ∈ ℝ
2 sn-mulgt1d.b ⊢ φ → B ∈ ℝ
3 sn-mulgt1d.1 ⊢ φ → 1 < A
4 sn-mulgt1d.2 ⊢ φ → 1 < B
5 1red ⊢ φ → 1 ∈ ℝ
6 1 2 remulcld ⊢ φ → A ⁢ B ∈ ℝ
7 0red ⊢ φ → 0 ∈ ℝ
8 sn-0lt1 ⊢ 0 < 1
9 8 a1i ⊢ φ → 0 < 1
10 7 5 1 9 3 lttrd ⊢ φ → 0 < A
11 2 1 10 sn-ltmulgt11d ⊢ φ → 1 < B ↔ A < A ⁢ B
12 4 11 mpbid ⊢ φ → A < A ⁢ B
13 5 1 6 3 12 lttrd ⊢ φ → 1 < A ⁢ B