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 } )