Theorem nnrecgt0

Description: The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999)

	Ref	Expression
Assertion	nnrecgt0	$$⊢A\in \mathbb{N}\to 0<\frac{1}{A}$$

Proof

Step	Hyp	Ref	Expression
1		nnge1	$$⊢A\in \mathbb{N}\to 1\le A$$
2		0lt1	$$⊢0<1$$
3		nnre	$$⊢A\in \mathbb{N}\to A\in ℝ$$
4		0re	$$⊢0\in ℝ$$
5		1re	$$⊢1\in ℝ$$
6		ltletr	$$⊢\left(0\in ℝ\wedge 1\in ℝ\wedge A\in ℝ\right)\to \left(\left(0<1\wedge 1\le A\right)\to 0<A\right)$$
7	4 5 6	mp3an12	$$⊢A\in ℝ\to \left(\left(0<1\wedge 1\le A\right)\to 0<A\right)$$
8		recgt0	$$⊢\left(A\in ℝ\wedge 0<A\right)\to 0<\frac{1}{A}$$
9	8	ex	$$⊢A\in ℝ\to \left(0<A\to 0<\frac{1}{A}\right)$$
10	7 9	syld	$$⊢A\in ℝ\to \left(\left(0<1\wedge 1\le A\right)\to 0<\frac{1}{A}\right)$$
11	3 10	syl	$$⊢A\in \mathbb{N}\to \left(\left(0<1\wedge 1\le A\right)\to 0<\frac{1}{A}\right)$$
12	2 11	mpani	$$⊢A\in \mathbb{N}\to \left(1\le A\to 0<\frac{1}{A}\right)$$
13	1 12	mpd	$$⊢A\in \mathbb{N}\to 0<\frac{1}{A}$$