Metamath Proof Explorer

Theorem nnrecl

Description: There exists a positive integer whose reciprocal is less than a given positive real. Exercise 3 of Apostol p. 28. (Contributed by NM, 8-Nov-2004)

Ref Expression
Assertion nnrecl ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{n}}<{A}$

Proof

Step Hyp Ref Expression
1 simpl ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\in ℝ$
2 gt0ne0 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\ne 0$
3 1 2 rereccld ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \frac{1}{{A}}\in ℝ$
4 arch ${⊢}\frac{1}{{A}}\in ℝ\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{A}}<{n}$
5 3 4 syl ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{A}}<{n}$
6 recgt0 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<\frac{1}{{A}}$
7 3 6 jca ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(\frac{1}{{A}}\in ℝ\wedge 0<\frac{1}{{A}}\right)$
8 nnre ${⊢}{n}\in ℕ\to {n}\in ℝ$
9 nngt0 ${⊢}{n}\in ℕ\to 0<{n}$
10 8 9 jca ${⊢}{n}\in ℕ\to \left({n}\in ℝ\wedge 0<{n}\right)$
11 ltrec ${⊢}\left(\left(\frac{1}{{A}}\in ℝ\wedge 0<\frac{1}{{A}}\right)\wedge \left({n}\in ℝ\wedge 0<{n}\right)\right)\to \left(\frac{1}{{A}}<{n}↔\frac{1}{{n}}<\frac{1}{\frac{1}{{A}}}\right)$
12 7 10 11 syl2an ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge {n}\in ℕ\right)\to \left(\frac{1}{{A}}<{n}↔\frac{1}{{n}}<\frac{1}{\frac{1}{{A}}}\right)$
13 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
14 13 adantr ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\in ℂ$
15 14 2 recrecd ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \frac{1}{\frac{1}{{A}}}={A}$
16 15 breq2d ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(\frac{1}{{n}}<\frac{1}{\frac{1}{{A}}}↔\frac{1}{{n}}<{A}\right)$
17 16 adantr ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge {n}\in ℕ\right)\to \left(\frac{1}{{n}}<\frac{1}{\frac{1}{{A}}}↔\frac{1}{{n}}<{A}\right)$
18 12 17 bitrd ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge {n}\in ℕ\right)\to \left(\frac{1}{{A}}<{n}↔\frac{1}{{n}}<{A}\right)$
19 18 rexbidva ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{A}}<{n}↔\exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{n}}<{A}\right)$
20 5 19 mpbid ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \exists {n}\in ℕ\phantom{\rule{.4em}{0ex}}\frac{1}{{n}}<{A}$