This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐴 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ )
2 gt0ne0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ≠ 0 )
3 1 2 rereccld ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / 𝐴 ) ∈ ℝ )
4 arch ⊢ ( ( 1 / 𝐴 ) ∈ ℝ → ∃ 𝑛 ∈ ℕ ( 1 / 𝐴 ) < 𝑛 )
5 3 4 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝐴 ) < 𝑛 )
6 recgt0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 1 / 𝐴 ) )
7 3 6 jca ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 < ( 1 / 𝐴 ) ) )
8 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
9 nngt0 ⊢ ( 𝑛 ∈ ℕ → 0 < 𝑛 )
10 8 9 jca ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
11 ltrec ⊢ ( ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 < ( 1 / 𝐴 ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( 1 / 𝐴 ) < 𝑛 ↔ ( 1 / 𝑛 ) < ( 1 / ( 1 / 𝐴 ) ) ) )
12 7 10 11 syl2an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝐴 ) < 𝑛 ↔ ( 1 / 𝑛 ) < ( 1 / ( 1 / 𝐴 ) ) ) )
13 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
14 13 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 𝐴 ∈ ℂ )
15 14 2 recrecd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 1 / ( 1 / 𝐴 ) ) = 𝐴 )
16 15 breq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 1 / 𝑛 ) < ( 1 / ( 1 / 𝐴 ) ) ↔ ( 1 / 𝑛 ) < 𝐴 ) )
17 16 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝑛 ) < ( 1 / ( 1 / 𝐴 ) ) ↔ ( 1 / 𝑛 ) < 𝐴 ) )
18 12 17 bitrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ∧ 𝑛 ∈ ℕ ) → ( ( 1 / 𝐴 ) < 𝑛 ↔ ( 1 / 𝑛 ) < 𝐴 ) )
19 18 rexbidva ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ∃ 𝑛 ∈ ℕ ( 1 / 𝐴 ) < 𝑛 ↔ ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐴 ) )
20 5 19 mpbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐴 )