Metamath Proof Explorer

Theorem lerec2

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

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

Proof

Step Hyp Ref Expression
1 gt0ne0 ⊢ B ∈ ℝ ∧ 0 < B → B ≠ 0
2 rereccl ⊢ B ∈ ℝ ∧ B ≠ 0 → 1 B ∈ ℝ
3 1 2 syldan ⊢ B ∈ ℝ ∧ 0 < B → 1 B ∈ ℝ
4 recgt0 ⊢ B ∈ ℝ ∧ 0 < B → 0 < 1 B
5 3 4 jca ⊢ B ∈ ℝ ∧ 0 < B → 1 B ∈ ℝ ∧ 0 < 1 B
6 lerec ⊢ A ∈ ℝ ∧ 0 < A ∧ 1 B ∈ ℝ ∧ 0 < 1 B → A ≤ 1 B ↔ 1 1 B ≤ 1 A
7 5 6 sylan2 ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A ≤ 1 B ↔ 1 1 B ≤ 1 A
8 recn ⊢ B ∈ ℝ → B ∈ ℂ
9 recrec ⊢ B ∈ ℂ ∧ B ≠ 0 → 1 1 B = B
10 8 1 9 syl2an2r ⊢ B ∈ ℝ ∧ 0 < B → 1 1 B = B
11 10 adantl ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 1 B = B
12 11 breq1d ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → 1 1 B ≤ 1 A ↔ B ≤ 1 A
13 7 12 bitrd ⊢ A ∈ ℝ ∧ 0 < A ∧ B ∈ ℝ ∧ 0 < B → A ≤ 1 B ↔ B ≤ 1 A