Step |
Hyp |
Ref |
Expression |
1 |
|
nn0ge0 |
|- ( N e. NN0 -> 0 <_ N ) |
2 |
|
nn0re |
|- ( N e. NN0 -> N e. RR ) |
3 |
|
nn0addge1 |
|- ( ( N e. RR /\ N e. NN0 ) -> N <_ ( N + N ) ) |
4 |
2 3
|
mpancom |
|- ( N e. NN0 -> N <_ ( N + N ) ) |
5 |
|
nn0cn |
|- ( N e. NN0 -> N e. CC ) |
6 |
5
|
2timesd |
|- ( N e. NN0 -> ( 2 x. N ) = ( N + N ) ) |
7 |
4 6
|
breqtrrd |
|- ( N e. NN0 -> N <_ ( 2 x. N ) ) |
8 |
|
nn0z |
|- ( N e. NN0 -> N e. ZZ ) |
9 |
|
0zd |
|- ( N e. NN0 -> 0 e. ZZ ) |
10 |
|
2z |
|- 2 e. ZZ |
11 |
|
zmulcl |
|- ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ ) |
12 |
10 8 11
|
sylancr |
|- ( N e. NN0 -> ( 2 x. N ) e. ZZ ) |
13 |
|
elfz |
|- ( ( N e. ZZ /\ 0 e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( N e. ( 0 ... ( 2 x. N ) ) <-> ( 0 <_ N /\ N <_ ( 2 x. N ) ) ) ) |
14 |
8 9 12 13
|
syl3anc |
|- ( N e. NN0 -> ( N e. ( 0 ... ( 2 x. N ) ) <-> ( 0 <_ N /\ N <_ ( 2 x. N ) ) ) ) |
15 |
1 7 14
|
mpbir2and |
|- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) ) |