Theorem nnge2recico01

Description: The reciprocal of an integer greater than 1 is in the right open interval between 0 and 1. (Contributed by AV, 10-Apr-2026)

	Ref	Expression
Assertion	nnge2recico01	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{1}{N}\in \left[0,1\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluzelre	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in ℝ$$
2		eluz2n0	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\ne 0$$
3	1 2	rereccld	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{1}{N}\in ℝ$$
4		1red	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1\in ℝ$$
5		0le1	$$⊢0\le 1$$
6	5	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 0\le 1$$
7		eluz2nn	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to N\in \mathbb{N}$$
8	7	nngt0d	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 0<N$$
9		divge0	$$⊢\left(\left(1\in ℝ\wedge 0\le 1\right)\wedge \left(N\in ℝ\wedge 0<N\right)\right)\to 0\le \frac{1}{N}$$
10	4 6 1 8 9	syl22anc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 0\le \frac{1}{N}$$
11		eluz2gt1	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to 1<N$$
12		recgt1	$$⊢\left(N\in ℝ\wedge 0<N\right)\to \left(1<N\leftrightarrow \frac{1}{N}<1\right)$$
13	1 8 12	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(1<N\leftrightarrow \frac{1}{N}<1\right)$$
14	11 13	mpbid	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{1}{N}<1$$
15		0re	$$⊢0\in ℝ$$
16		1xr	$$⊢1\in {ℝ}^{*}$$
17	15 16	pm3.2i	$$⊢\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)$$
18		elico2	$$⊢\left(0\in ℝ\wedge 1\in {ℝ}^{*}\right)\to \left(\frac{1}{N}\in \left[0,1\right)\leftrightarrow \left(\frac{1}{N}\in ℝ\wedge 0\le \frac{1}{N}\wedge \frac{1}{N}<1\right)\right)$$
19	17 18	mp1i	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \left(\frac{1}{N}\in \left[0,1\right)\leftrightarrow \left(\frac{1}{N}\in ℝ\wedge 0\le \frac{1}{N}\wedge \frac{1}{N}<1\right)\right)$$
20	3 10 14 19	mpbir3and	$$⊢N\in {\mathbb{Z}}_{\ge 2}\to \frac{1}{N}\in \left[0,1\right)$$