Metamath Proof Explorer

Theorem ltdiv1i

Description: Division of both sides of 'less than' by a positive number. (Contributed by NM, 16-May-1999)

Ref Expression
Hypotheses ltplus1.1 ⊢ A ∈ ℝ
prodgt0.2 ⊢ B ∈ ℝ
ltmul1.3 ⊢ C ∈ ℝ
Assertion ltdiv1i ⊢ 0 < C → A < B ↔ A C < B C

Proof

Step Hyp Ref Expression
1 ltplus1.1 ⊢ A ∈ ℝ
2 prodgt0.2 ⊢ B ∈ ℝ
3 ltmul1.3 ⊢ C ∈ ℝ
4 ltdiv1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A C < B C
5 1 2 4 mp3an12 ⊢ C ∈ ℝ ∧ 0 < C → A < B ↔ A C < B C
6 3 5 mpan ⊢ 0 < C → A < B ↔ A C < B C