Theorem sn-ltmul2d

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

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

Proof

Step	Hyp	Ref	Expression
1		sn-ltmul2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		sn-ltmul2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		sn-ltmul2d.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		sn-ltmul2d.1	⊢ ( 𝜑 → 0 < 𝐶 )
5		rersubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 −ℝ 𝐴 ) ∈ ℝ )
6	2 1 5	syl2anc	⊢ ( 𝜑 → ( 𝐵 −ℝ 𝐴 ) ∈ ℝ )
7	3 6 4	mulgt0b2d	⊢ ( 𝜑 → ( 0 < ( 𝐵 −ℝ 𝐴 ) ↔ 0 < ( 𝐶 · ( 𝐵 −ℝ 𝐴 ) ) ) )
8		resubdi	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐶 · ( 𝐵 −ℝ 𝐴 ) ) = ( ( 𝐶 · 𝐵 ) −ℝ ( 𝐶 · 𝐴 ) ) )
9	3 2 1 8	syl3anc	⊢ ( 𝜑 → ( 𝐶 · ( 𝐵 −ℝ 𝐴 ) ) = ( ( 𝐶 · 𝐵 ) −ℝ ( 𝐶 · 𝐴 ) ) )
10	9	breq2d	⊢ ( 𝜑 → ( 0 < ( 𝐶 · ( 𝐵 −ℝ 𝐴 ) ) ↔ 0 < ( ( 𝐶 · 𝐵 ) −ℝ ( 𝐶 · 𝐴 ) ) ) )
11	7 10	bitr2d	⊢ ( 𝜑 → ( 0 < ( ( 𝐶 · 𝐵 ) −ℝ ( 𝐶 · 𝐴 ) ) ↔ 0 < ( 𝐵 −ℝ 𝐴 ) ) )
12	3 1	remulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ ℝ )
13	3 2	remulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℝ )
14		reposdif	⊢ ( ( ( 𝐶 · 𝐴 ) ∈ ℝ ∧ ( 𝐶 · 𝐵 ) ∈ ℝ ) → ( ( 𝐶 · 𝐴 ) < ( 𝐶 · 𝐵 ) ↔ 0 < ( ( 𝐶 · 𝐵 ) −ℝ ( 𝐶 · 𝐴 ) ) ) )
15	12 13 14	syl2anc	⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) < ( 𝐶 · 𝐵 ) ↔ 0 < ( ( 𝐶 · 𝐵 ) −ℝ ( 𝐶 · 𝐴 ) ) ) )
16		reposdif	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 −ℝ 𝐴 ) ) )
17	1 2 16	syl2anc	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 −ℝ 𝐴 ) ) )
18	11 15 17	3bitr4d	⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) < ( 𝐶 · 𝐵 ) ↔ 𝐴 < 𝐵 ) )