# Metamath Proof Explorer

## 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 ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}\le {B}↔\frac{1}{{B}}\le \frac{1}{{A}}\right)$

### Proof

Step Hyp Ref Expression
1 ltrec ${⊢}\left(\left({B}\in ℝ\wedge 0<{B}\right)\wedge \left({A}\in ℝ\wedge 0<{A}\right)\right)\to \left({B}<{A}↔\frac{1}{{A}}<\frac{1}{{B}}\right)$
2 1 ancoms ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({B}<{A}↔\frac{1}{{A}}<\frac{1}{{B}}\right)$
3 2 notbid ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(¬{B}<{A}↔¬\frac{1}{{A}}<\frac{1}{{B}}\right)$
4 simpll ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {A}\in ℝ$
5 simprl ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\in ℝ$
6 4 5 lenltd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}\le {B}↔¬{B}<{A}\right)$
7 simprr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 0<{B}$
8 7 gt0ne0d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\ne 0$
9 5 8 rereccld ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \frac{1}{{B}}\in ℝ$
10 simplr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 0<{A}$
11 10 gt0ne0d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {A}\ne 0$
12 4 11 rereccld ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \frac{1}{{A}}\in ℝ$
13 9 12 lenltd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{1}{{B}}\le \frac{1}{{A}}↔¬\frac{1}{{A}}<\frac{1}{{B}}\right)$
14 3 6 13 3bitr4d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}\le {B}↔\frac{1}{{B}}\le \frac{1}{{A}}\right)$