Metamath Proof Explorer

Theorem ltmul2

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)

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

Proof

Step Hyp Ref Expression
1 ltmul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A ⁢ C < B ⁢ C
2 recn ⊢ C ∈ ℝ → C ∈ ℂ
3 recn ⊢ A ∈ ℝ → A ∈ ℂ
4 mulcom ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
5 3 4 sylan ⊢ A ∈ ℝ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
6 5 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
7 recn ⊢ B ∈ ℝ → B ∈ ℂ
8 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
9 7 8 sylan ⊢ B ∈ ℝ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
10 9 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
11 6 10 breq12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℂ → A ⁢ C < B ⁢ C ↔ C ⁢ A < C ⁢ B
12 2 11 syl3an3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ⁢ C < B ⁢ C ↔ C ⁢ A < C ⁢ B
13 12 3adant3r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ⁢ C < B ⁢ C ↔ C ⁢ A < C ⁢ B
14 1 13 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ C ⁢ A < C ⁢ B