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

### Proof

Step Hyp Ref Expression
1 ltmul1a ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\wedge {A}<{B}\right)\to {A}{C}<{B}{C}$
2 1 ex ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}<{B}\to {A}{C}<{B}{C}\right)$
3 oveq1 ${⊢}{A}={B}\to {A}{C}={B}{C}$
4 3 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}={B}\to {A}{C}={B}{C}\right)$
5 ltmul1a ${⊢}\left(\left({B}\in ℝ\wedge {A}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\wedge {B}<{A}\right)\to {B}{C}<{A}{C}$
6 5 ex ${⊢}\left({B}\in ℝ\wedge {A}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({B}<{A}\to {B}{C}<{A}{C}\right)$
7 6 3com12 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({B}<{A}\to {B}{C}<{A}{C}\right)$
8 4 7 orim12d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(\left({A}={B}\vee {B}<{A}\right)\to \left({A}{C}={B}{C}\vee {B}{C}<{A}{C}\right)\right)$
9 8 con3d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(¬\left({A}{C}={B}{C}\vee {B}{C}<{A}{C}\right)\to ¬\left({A}={B}\vee {B}<{A}\right)\right)$
10 simp1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {A}\in ℝ$
11 simp3l ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}\in ℝ$
12 10 11 remulcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {A}{C}\in ℝ$
13 simp2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {B}\in ℝ$
14 13 11 remulcld ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {B}{C}\in ℝ$
15 12 14 lttrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}{C}<{B}{C}↔¬\left({A}{C}={B}{C}\vee {B}{C}<{A}{C}\right)\right)$
16 10 13 lttrid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}<{B}↔¬\left({A}={B}\vee {B}<{A}\right)\right)$
17 9 15 16 3imtr4d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}{C}<{B}{C}\to {A}<{B}\right)$
18 2 17 impbid ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}<{B}↔{A}{C}<{B}{C}\right)$