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

Metamath Proof Explorer

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 mulgt0b1d ⊢ ( 𝜑 → ( 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 ⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) < ( 𝐶 · 𝐵 ) ↔ 𝐴 < 𝐵 ) )