Metamath Proof Explorer

Theorem ltdiv1

Description: Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ∈ ℝ
2 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B ∈ ℝ
3 simp3l ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ∈ ℝ
4 simp3r ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → 0 < C
5 4 gt0ne0d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ≠ 0
6 3 5 rereccld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → 1 C ∈ ℝ
7 recgt0 ⊢ C ∈ ℝ ∧ 0 < C → 0 < 1 C
8 7 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → 0 < 1 C
9 ltmul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 1 C ∈ ℝ ∧ 0 < 1 C → A < B ↔ A ⁢ 1 C < B ⁢ 1 C
10 1 2 6 8 9 syl112anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A ⁢ 1 C < B ⁢ 1 C
11 1 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A ∈ ℂ
12 3 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → C ∈ ℂ
13 11 12 5 divrecd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C = A ⁢ 1 C
14 2 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B ∈ ℂ
15 14 12 5 divrecd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → B C = B ⁢ 1 C
16 13 15 breq12d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A C < B C ↔ A ⁢ 1 C < B ⁢ 1 C
17 10 16 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ ∧ 0 < C → A < B ↔ A C < B C