Metamath Proof Explorer

Theorem ltrec1

Description: Reciprocal swap in a 'less than' relation. (Contributed by NM, 24-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 gt0ne0 ⊢ A ∈ ℝ ∧ 0 < A → A ≠ 0
2 rereccl ⊢ A ∈ ℝ ∧ A ≠ 0 → 1 A ∈ ℝ
3 1 2 syldan ⊢ A ∈ ℝ ∧ 0 < A → 1 A ∈ ℝ
4 recgt0 ⊢ A ∈ ℝ ∧ 0 < A → 0 < 1 A
5 3 4 jca ⊢ A ∈ ℝ ∧ 0 < A → 1 A ∈ ℝ ∧ 0 < 1 A
6 ltrec ⊢ 1 A ∈ ℝ ∧ 0 < 1 A ∧ B ∈ ℝ ∧ 0 < B → 1 A < B ↔ 1 B < 1 1 A
7 5 6 sylan ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 A < B ↔ 1 B < 1 1 A
8 recn ⊢ A ∈ ℝ → A ∈ ℂ
9 recrec ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 1 A = A
10 8 9 sylan ⊢ A ∈ ℝ ∧ A ≠ 0 → 1 1 A = A
11 1 10 syldan ⊢ A ∈ ℝ ∧ 0 < A → 1 1 A = A
12 11 adantr ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 1 A = A
13 12 breq2d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 B < 1 1 A ↔ 1 B < A
14 7 13 bitrd ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 A < B ↔ 1 B < A