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	⊢ ( 𝑁 ∈ ℕ → { 1 , 𝑁 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } )

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3		1dvds	⊢ ( 𝑁 ∈ ℤ → 1 ∥ 𝑁 )
4	2 3	syl	⊢ ( 𝑁 ∈ ℕ → 1 ∥ 𝑁 )
5		breq1	⊢ ( 𝑛 = 1 → ( 𝑛 ∥ 𝑁 ↔ 1 ∥ 𝑁 ) )
6	5	elrab	⊢ ( 1 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } ↔ ( 1 ∈ ℕ ∧ 1 ∥ 𝑁 ) )
7	6	biimpri	⊢ ( ( 1 ∈ ℕ ∧ 1 ∥ 𝑁 ) → 1 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } )
8	1 4 7	sylancr	⊢ ( 𝑁 ∈ ℕ → 1 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } )
9		iddvds	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∥ 𝑁 )
10	2 9	syl	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∥ 𝑁 )
11		breq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ∥ 𝑁 ↔ 𝑁 ∥ 𝑁 ) )
12	11	elrab	⊢ ( 𝑁 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } ↔ ( 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑁 ) )
13	12	biimpri	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑁 ) → 𝑁 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } )
14	10 13	mpdan	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } )
15	8 14	prssd	⊢ ( 𝑁 ∈ ℕ → { 1 , 𝑁 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁 } )