Metamath Proof Explorer

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 ∈ ℕ → 1 N ⊆ n ∈ ℕ | n ∥ N

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 nnz ⊢ N ∈ ℕ → N ∈ ℤ
3 1dvds ⊢ N ∈ ℤ → 1 ∥ N
4 2 3 syl ⊢ N ∈ ℕ → 1 ∥ N
5 breq1 ⊢ n = 1 → n ∥ N ↔ 1 ∥ N
6 5 elrab ⊢ 1 ∈ n ∈ ℕ | n ∥ N ↔ 1 ∈ ℕ ∧ 1 ∥ N
7 6 biimpri ⊢ 1 ∈ ℕ ∧ 1 ∥ N → 1 ∈ n ∈ ℕ | n ∥ N
8 1 4 7 sylancr ⊢ N ∈ ℕ → 1 ∈ n ∈ ℕ | n ∥ N
9 iddvds ⊢ N ∈ ℤ → N ∥ N
10 2 9 syl ⊢ N ∈ ℕ → N ∥ N
11 breq1 ⊢ n = N → n ∥ N ↔ N ∥ N
12 11 elrab ⊢ N ∈ n ∈ ℕ | n ∥ N ↔ N ∈ ℕ ∧ N ∥ N
13 12 biimpri ⊢ N ∈ ℕ ∧ N ∥ N → N ∈ n ∈ ℕ | n ∥ N
14 10 13 mpdan ⊢ N ∈ ℕ → N ∈ n ∈ ℕ | n ∥ N
15 8 14 prssd ⊢ N ∈ ℕ → 1 N ⊆ n ∈ ℕ | n ∥ N