Theorem lerec

Description: The reciprocal of both sides of 'less than or equal to'. (Contributed by NM, 3-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	lerec	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltrec	⊢ ( ( ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 𝐵 < 𝐴 ↔ ( 1 / 𝐴 ) < ( 1 / 𝐵 ) ) )
2	1	ancoms	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐵 < 𝐴 ↔ ( 1 / 𝐴 ) < ( 1 / 𝐵 ) ) )
3	2	notbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ¬ 𝐵 < 𝐴 ↔ ¬ ( 1 / 𝐴 ) < ( 1 / 𝐵 ) ) )
4		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐴 ∈ ℝ )
5		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐵 ∈ ℝ )
6	4 5	lenltd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
7		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 < 𝐵 )
8	7	gt0ne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐵 ≠ 0 )
9	5 8	rereccld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 1 / 𝐵 ) ∈ ℝ )
10		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 < 𝐴 )
11	10	gt0ne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 𝐴 ≠ 0 )
12	4 11	rereccld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 1 / 𝐴 ) ∈ ℝ )
13	9 12	lenltd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ↔ ¬ ( 1 / 𝐴 ) < ( 1 / 𝐵 ) ) )
14	3 6 13	3bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( 𝐴 ≤ 𝐵 ↔ ( 1 / 𝐵 ) ≤ ( 1 / 𝐴 ) ) )