# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}<{B}↔{C}{A}<{C}{B}\right)$

### Proof

Step Hyp Ref Expression
1 ltmul1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}<{B}↔{A}{C}<{B}{C}\right)$
2 recn ${⊢}{C}\in ℝ\to {C}\in ℂ$
3 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
4 mulcom ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\right)\to {A}{C}={C}{A}$
5 3 4 sylan ${⊢}\left({A}\in ℝ\wedge {C}\in ℂ\right)\to {A}{C}={C}{A}$
6 5 3adant2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℂ\right)\to {A}{C}={C}{A}$
7 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
8 mulcom ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}{C}={C}{B}$
9 7 8 sylan ${⊢}\left({B}\in ℝ\wedge {C}\in ℂ\right)\to {B}{C}={C}{B}$
10 9 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℂ\right)\to {B}{C}={C}{B}$
11 6 10 breq12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℂ\right)\to \left({A}{C}<{B}{C}↔{C}{A}<{C}{B}\right)$
12 2 11 syl3an3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {C}\in ℝ\right)\to \left({A}{C}<{B}{C}↔{C}{A}<{C}{B}\right)$
13 12 3adant3r ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}{C}<{B}{C}↔{C}{A}<{C}{B}\right)$
14 1 13 bitrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}<{B}↔{C}{A}<{C}{B}\right)$