Metamath Proof Explorer

Theorem ltrec

Description: The reciprocal of both sides of 'less than'. (Contributed by NM, 26-Sep-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion ltrec ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A < B ↔ 1 B < 1 A

Proof

Step Hyp Ref Expression
1 1red ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 ∈ ℝ
2 simprl ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → B ∈ ℝ
3 simpll ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A ∈ ℝ
4 simplr ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 0 < A
5 ltmuldiv ⊢ 1 ∈ ℝ ∧ B ∈ ℝ ∧ A ∈ ℝ ∧ 0 < A → 1 ⁢ A < B ↔ 1 < B A
6 1 2 3 4 5 syl112anc ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 ⁢ A < B ↔ 1 < B A
7 3 recnd ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A ∈ ℂ
8 7 mulid2d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 ⁢ A = A
9 8 breq1d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 ⁢ A < B ↔ A < B
10 2 recnd ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → B ∈ ℂ
11 4 gt0ne0d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A ≠ 0
12 10 7 11 divrecd ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → B A = B ⁢ 1 A
13 12 breq2d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 < B A ↔ 1 < B ⁢ 1 A
14 6 9 13 3bitr3d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A < B ↔ 1 < B ⁢ 1 A
15 3 11 rereccld ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 A ∈ ℝ
16 simprr ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 0 < B
17 ltdivmul ⊢ 1 ∈ ℝ ∧ 1 A ∈ ℝ ∧ B ∈ ℝ ∧ 0 < B → 1 B < 1 A ↔ 1 < B ⁢ 1 A
18 1 15 2 16 17 syl112anc ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 B < 1 A ↔ 1 < B ⁢ 1 A
19 14 18 bitr4d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A < B ↔ 1 B < 1 A