Theorem nnrecq

Description: The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004)

	Ref	Expression
Assertion	nnrecq	$$⊢A\in \mathbb{N}\to \frac{1}{A}\in \mathbb{Q}$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		znq	$$⊢\left(1\in \mathbb{Z}\wedge A\in \mathbb{N}\right)\to \frac{1}{A}\in \mathbb{Q}$$
3	1 2	mpan	$$⊢A\in \mathbb{N}\to \frac{1}{A}\in \mathbb{Q}$$