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 e. NN -> { 1 , N } C_ { n e. NN | n || N } )

Proof

Step Hyp Ref Expression
1 1nn
 |-  1 e. NN
2 nnz
 |-  ( N e. NN -> N e. ZZ )
3 1dvds
 |-  ( N e. ZZ -> 1 || N )
4 2 3 syl
 |-  ( N e. NN -> 1 || N )
5 breq1
 |-  ( n = 1 -> ( n || N <-> 1 || N ) )
6 5 elrab
 |-  ( 1 e. { n e. NN | n || N } <-> ( 1 e. NN /\ 1 || N ) )
7 6 biimpri
 |-  ( ( 1 e. NN /\ 1 || N ) -> 1 e. { n e. NN | n || N } )
8 1 4 7 sylancr
 |-  ( N e. NN -> 1 e. { n e. NN | n || N } )
9 iddvds
 |-  ( N e. ZZ -> N || N )
10 2 9 syl
 |-  ( N e. NN -> N || N )
11 breq1
 |-  ( n = N -> ( n || N <-> N || N ) )
12 11 elrab
 |-  ( N e. { n e. NN | n || N } <-> ( N e. NN /\ N || N ) )
13 12 biimpri
 |-  ( ( N e. NN /\ N || N ) -> N e. { n e. NN | n || N } )
14 10 13 mpdan
 |-  ( N e. NN -> N e. { n e. NN | n || N } )
15 8 14 prssd
 |-  ( N e. NN -> { 1 , N } C_ { n e. NN | n || N } )