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 < ( 𝐴 · 𝐵 ) )