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 / 𝑛 ) < 𝐴 )