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