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

Proof

Step Hyp Ref Expression
1 gt0ne0 ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to {B}\ne 0$
2 rereccl ${⊢}\left({B}\in ℝ\wedge {B}\ne 0\right)\to \frac{1}{{B}}\in ℝ$
3 1 2 syldan ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to \frac{1}{{B}}\in ℝ$
4 recgt0 ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to 0<\frac{1}{{B}}$
5 3 4 jca ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to \left(\frac{1}{{B}}\in ℝ\wedge 0<\frac{1}{{B}}\right)$
6 lerec ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left(\frac{1}{{B}}\in ℝ\wedge 0<\frac{1}{{B}}\right)\right)\to \left({A}\le \frac{1}{{B}}↔\frac{1}{\frac{1}{{B}}}\le \frac{1}{{A}}\right)$
7 5 6 sylan2 ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}\le \frac{1}{{B}}↔\frac{1}{\frac{1}{{B}}}\le \frac{1}{{A}}\right)$
8 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
9 recrec ${⊢}\left({B}\in ℂ\wedge {B}\ne 0\right)\to \frac{1}{\frac{1}{{B}}}={B}$
10 8 1 9 syl2an2r ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to \frac{1}{\frac{1}{{B}}}={B}$
11 10 adantl ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \frac{1}{\frac{1}{{B}}}={B}$
12 11 breq1d ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{1}{\frac{1}{{B}}}\le \frac{1}{{A}}↔{B}\le \frac{1}{{A}}\right)$
13 7 12 bitrd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}\le \frac{1}{{B}}↔{B}\le \frac{1}{{A}}\right)$