Metamath Proof Explorer

Theorem ltmul1

Description: Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of Apostol p. 20. (Contributed by NM, 13-Feb-2005) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion ltmul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A ⁢ C < B ⁢ C

Proof

Step Hyp Ref Expression
1 ltmul1a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C ∧ A < B → A ⁢ C < B ⁢ C
2 1 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B → A ⁢ C < B ⁢ C
3 oveq1 ⊢ A = B → A ⁢ C = B ⁢ C
4 3 a1i ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A = B → A ⁢ C = B ⁢ C
5 ltmul1a ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C ∧ B < A → B ⁢ C < A ⁢ C
6 5 ex ⊢ B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B < A → B ⁢ C < A ⁢ C
7 6 3com12 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B < A → B ⁢ C < A ⁢ C
8 4 7 orim12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A = B ∨ B < A → A ⁢ C = B ⁢ C ∨ B ⁢ C < A ⁢ C
9 8 con3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → ¬ A ⁢ C = B ⁢ C ∨ B ⁢ C < A ⁢ C → ¬ A = B ∨ B < A
10 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ∈ ℝ
11 simp3l ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ∈ ℝ
12 10 11 remulcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ⁢ C ∈ ℝ
13 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B ∈ ℝ
14 13 11 remulcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B ⁢ C ∈ ℝ
15 12 14 lttrid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ⁢ C < B ⁢ C ↔ ¬ A ⁢ C = B ⁢ C ∨ B ⁢ C < A ⁢ C
16 10 13 lttrid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ ¬ A = B ∨ B < A
17 9 15 16 3imtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ⁢ C < B ⁢ C → A < B
18 2 17 impbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A ⁢ C < B ⁢ C