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