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 \in ℝ \land 0 < A) \to \exists n \in ℕ \frac{1}{n} < A$

Proof

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

Metamath Proof Explorer

Theorem nnrecl

Proof