This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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