Theorem sn-ltmulgt11d

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

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

Proof

Step	Hyp	Ref	Expression
1		sn-ltmulgt11d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		sn-ltmulgt11d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		sn-ltmulgt11d.1	⊢ ( 𝜑 → 0 < 𝐵 )
4		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
5	4 1 2 3	sn-ltmul2d	⊢ ( 𝜑 → ( ( 𝐵 · 1 ) < ( 𝐵 · 𝐴 ) ↔ 1 < 𝐴 ) )
6		ax-1rid	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 · 1 ) = 𝐵 )
7	2 6	syl	⊢ ( 𝜑 → ( 𝐵 · 1 ) = 𝐵 )
8	7	breq1d	⊢ ( 𝜑 → ( ( 𝐵 · 1 ) < ( 𝐵 · 𝐴 ) ↔ 𝐵 < ( 𝐵 · 𝐴 ) ) )
9	5 8	bitr3d	⊢ ( 𝜑 → ( 1 < 𝐴 ↔ 𝐵 < ( 𝐵 · 𝐴 ) ) )