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

Metamath Proof Explorer

Theorem sn-ltmulgt11d

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

Ref Expression
Hypotheses sn-ltmulgt11d.a ⊢ φ → A ∈ ℝ
sn-ltmulgt11d.b ⊢ φ → B ∈ ℝ
sn-ltmulgt11d.1 ⊢ φ → 0 < B
Assertion sn-ltmulgt11d ⊢ φ → 1 < A ↔ B < B ⁢ A

Proof

Step Hyp Ref Expression
1 sn-ltmulgt11d.a ⊢ φ → A ∈ ℝ
2 sn-ltmulgt11d.b ⊢ φ → B ∈ ℝ
3 sn-ltmulgt11d.1 ⊢ φ → 0 < B
4 1red ⊢ φ → 1 ∈ ℝ
5 4 1 2 3 sn-ltmul2d ⊢ φ → B ⋅ 1 < B ⁢ A ↔ 1 < A
6 ax-1rid ⊢ B ∈ ℝ → B ⋅ 1 = B
7 2 6 syl ⊢ φ → B ⋅ 1 = B
8 7 breq1d ⊢ φ → B ⋅ 1 < B ⁢ A ↔ B < B ⁢ A
9 5 8 bitr3d ⊢ φ → 1 < A ↔ B < B ⁢ A