Step |
Hyp |
Ref |
Expression |
1 |
|
nn0re |
|- ( N e. NN0 -> N e. RR ) |
2 |
|
2re |
|- 2 e. RR |
3 |
2
|
a1i |
|- ( N e. NN0 -> 2 e. RR ) |
4 |
1 3
|
leloed |
|- ( N e. NN0 -> ( N <_ 2 <-> ( N < 2 \/ N = 2 ) ) ) |
5 |
|
nn0z |
|- ( N e. NN0 -> N e. ZZ ) |
6 |
|
2z |
|- 2 e. ZZ |
7 |
|
zltlem1 |
|- ( ( N e. ZZ /\ 2 e. ZZ ) -> ( N < 2 <-> N <_ ( 2 - 1 ) ) ) |
8 |
5 6 7
|
sylancl |
|- ( N e. NN0 -> ( N < 2 <-> N <_ ( 2 - 1 ) ) ) |
9 |
|
2m1e1 |
|- ( 2 - 1 ) = 1 |
10 |
9
|
a1i |
|- ( N e. NN0 -> ( 2 - 1 ) = 1 ) |
11 |
10
|
breq2d |
|- ( N e. NN0 -> ( N <_ ( 2 - 1 ) <-> N <_ 1 ) ) |
12 |
8 11
|
bitrd |
|- ( N e. NN0 -> ( N < 2 <-> N <_ 1 ) ) |
13 |
|
1red |
|- ( N e. NN0 -> 1 e. RR ) |
14 |
1 13
|
leloed |
|- ( N e. NN0 -> ( N <_ 1 <-> ( N < 1 \/ N = 1 ) ) ) |
15 |
|
nn0lt10b |
|- ( N e. NN0 -> ( N < 1 <-> N = 0 ) ) |
16 |
|
3mix1 |
|- ( N = 0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) |
17 |
15 16
|
syl6bi |
|- ( N e. NN0 -> ( N < 1 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
18 |
17
|
com12 |
|- ( N < 1 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
19 |
|
3mix2 |
|- ( N = 1 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) |
20 |
19
|
a1d |
|- ( N = 1 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
21 |
18 20
|
jaoi |
|- ( ( N < 1 \/ N = 1 ) -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
22 |
21
|
com12 |
|- ( N e. NN0 -> ( ( N < 1 \/ N = 1 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
23 |
14 22
|
sylbid |
|- ( N e. NN0 -> ( N <_ 1 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
24 |
12 23
|
sylbid |
|- ( N e. NN0 -> ( N < 2 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
25 |
24
|
com12 |
|- ( N < 2 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
26 |
|
3mix3 |
|- ( N = 2 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) |
27 |
26
|
a1d |
|- ( N = 2 -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
28 |
25 27
|
jaoi |
|- ( ( N < 2 \/ N = 2 ) -> ( N e. NN0 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
29 |
28
|
com12 |
|- ( N e. NN0 -> ( ( N < 2 \/ N = 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
30 |
4 29
|
sylbid |
|- ( N e. NN0 -> ( N <_ 2 -> ( N = 0 \/ N = 1 \/ N = 2 ) ) ) |
31 |
30
|
imp |
|- ( ( N e. NN0 /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) ) |