Theorem 1idssfct

Description: The positive divisors of a positive integer include 1 and itself. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	1idssfct	$$⊢N\in \mathbb{N}\to \left\{1,N\right\}\subseteq \left\{n\in \mathbb{N}|n\parallel N\right\}$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
3		1dvds	$$⊢N\in \mathbb{Z}\to 1\parallel N$$
4	2 3	syl	$$⊢N\in \mathbb{N}\to 1\parallel N$$
5		breq1	$$⊢n=1\to \left(n\parallel N\leftrightarrow 1\parallel N\right)$$
6	5	elrab	$$⊢1\in \left\{n\in \mathbb{N}|n\parallel N\right\}\leftrightarrow \left(1\in \mathbb{N}\wedge 1\parallel N\right)$$
7	6	biimpri	$$⊢\left(1\in \mathbb{N}\wedge 1\parallel N\right)\to 1\in \left\{n\in \mathbb{N}|n\parallel N\right\}$$
8	1 4 7	sylancr	$$⊢N\in \mathbb{N}\to 1\in \left\{n\in \mathbb{N}|n\parallel N\right\}$$
9		iddvds	$$⊢N\in \mathbb{Z}\to N\parallel N$$
10	2 9	syl	$$⊢N\in \mathbb{N}\to N\parallel N$$
11		breq1	$$⊢n=N\to \left(n\parallel N\leftrightarrow N\parallel N\right)$$
12	11	elrab	$$⊢N\in \left\{n\in \mathbb{N}|n\parallel N\right\}\leftrightarrow \left(N\in \mathbb{N}\wedge N\parallel N\right)$$
13	12	biimpri	$$⊢\left(N\in \mathbb{N}\wedge N\parallel N\right)\to N\in \left\{n\in \mathbb{N}|n\parallel N\right\}$$
14	10 13	mpdan	$$⊢N\in \mathbb{N}\to N\in \left\{n\in \mathbb{N}|n\parallel N\right\}$$
15	8 14	prssd	$$⊢N\in \mathbb{N}\to \left\{1,N\right\}\subseteq \left\{n\in \mathbb{N}|n\parallel N\right\}$$