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

### Proof

Step Hyp Ref Expression
1 1red ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 1\in ℝ$
2 simprl ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\in ℝ$
3 simpll ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {A}\in ℝ$
4 simplr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 0<{A}$
5 ltmuldiv ${⊢}\left(1\in ℝ\wedge {B}\in ℝ\wedge \left({A}\in ℝ\wedge 0<{A}\right)\right)\to \left(1{A}<{B}↔1<\frac{{B}}{{A}}\right)$
6 1 2 3 4 5 syl112anc ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(1{A}<{B}↔1<\frac{{B}}{{A}}\right)$
7 3 recnd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {A}\in ℂ$
8 7 mulid2d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 1{A}={A}$
9 8 breq1d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(1{A}<{B}↔{A}<{B}\right)$
10 2 recnd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\in ℂ$
11 4 gt0ne0d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {A}\ne 0$
12 10 7 11 divrecd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \frac{{B}}{{A}}={B}\left(\frac{1}{{A}}\right)$
13 12 breq2d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(1<\frac{{B}}{{A}}↔1<{B}\left(\frac{1}{{A}}\right)\right)$
14 6 9 13 3bitr3d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}<{B}↔1<{B}\left(\frac{1}{{A}}\right)\right)$
15 3 11 rereccld ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \frac{1}{{A}}\in ℝ$
16 simprr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 0<{B}$
17 ltdivmul ${⊢}\left(1\in ℝ\wedge \frac{1}{{A}}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{1}{{B}}<\frac{1}{{A}}↔1<{B}\left(\frac{1}{{A}}\right)\right)$
18 1 15 2 16 17 syl112anc ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{1}{{B}}<\frac{1}{{A}}↔1<{B}\left(\frac{1}{{A}}\right)\right)$
19 14 18 bitr4d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}<{B}↔\frac{1}{{B}}<\frac{1}{{A}}\right)$