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 ⊢ A ∈ ℝ ∧ 0 < A → ∃ n ∈ ℕ 1 n < A

Proof

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