Step |
Hyp |
Ref |
Expression |
1 |
|
uzind2.1 |
|- ( j = ( M + 1 ) -> ( ph <-> ps ) ) |
2 |
|
uzind2.2 |
|- ( j = k -> ( ph <-> ch ) ) |
3 |
|
uzind2.3 |
|- ( j = ( k + 1 ) -> ( ph <-> th ) ) |
4 |
|
uzind2.4 |
|- ( j = N -> ( ph <-> ta ) ) |
5 |
|
uzind2.5 |
|- ( M e. ZZ -> ps ) |
6 |
|
uzind2.6 |
|- ( ( M e. ZZ /\ k e. ZZ /\ M < k ) -> ( ch -> th ) ) |
7 |
|
zltp1le |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( M + 1 ) <_ N ) ) |
8 |
|
peano2z |
|- ( M e. ZZ -> ( M + 1 ) e. ZZ ) |
9 |
1
|
imbi2d |
|- ( j = ( M + 1 ) -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> ps ) ) ) |
10 |
2
|
imbi2d |
|- ( j = k -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> ch ) ) ) |
11 |
3
|
imbi2d |
|- ( j = ( k + 1 ) -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> th ) ) ) |
12 |
4
|
imbi2d |
|- ( j = N -> ( ( M e. ZZ -> ph ) <-> ( M e. ZZ -> ta ) ) ) |
13 |
5
|
a1i |
|- ( ( M + 1 ) e. ZZ -> ( M e. ZZ -> ps ) ) |
14 |
|
zltp1le |
|- ( ( M e. ZZ /\ k e. ZZ ) -> ( M < k <-> ( M + 1 ) <_ k ) ) |
15 |
6
|
3expia |
|- ( ( M e. ZZ /\ k e. ZZ ) -> ( M < k -> ( ch -> th ) ) ) |
16 |
14 15
|
sylbird |
|- ( ( M e. ZZ /\ k e. ZZ ) -> ( ( M + 1 ) <_ k -> ( ch -> th ) ) ) |
17 |
16
|
ex |
|- ( M e. ZZ -> ( k e. ZZ -> ( ( M + 1 ) <_ k -> ( ch -> th ) ) ) ) |
18 |
17
|
com3l |
|- ( k e. ZZ -> ( ( M + 1 ) <_ k -> ( M e. ZZ -> ( ch -> th ) ) ) ) |
19 |
18
|
imp |
|- ( ( k e. ZZ /\ ( M + 1 ) <_ k ) -> ( M e. ZZ -> ( ch -> th ) ) ) |
20 |
19
|
3adant1 |
|- ( ( ( M + 1 ) e. ZZ /\ k e. ZZ /\ ( M + 1 ) <_ k ) -> ( M e. ZZ -> ( ch -> th ) ) ) |
21 |
20
|
a2d |
|- ( ( ( M + 1 ) e. ZZ /\ k e. ZZ /\ ( M + 1 ) <_ k ) -> ( ( M e. ZZ -> ch ) -> ( M e. ZZ -> th ) ) ) |
22 |
9 10 11 12 13 21
|
uzind |
|- ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ ( M + 1 ) <_ N ) -> ( M e. ZZ -> ta ) ) |
23 |
22
|
3exp |
|- ( ( M + 1 ) e. ZZ -> ( N e. ZZ -> ( ( M + 1 ) <_ N -> ( M e. ZZ -> ta ) ) ) ) |
24 |
8 23
|
syl |
|- ( M e. ZZ -> ( N e. ZZ -> ( ( M + 1 ) <_ N -> ( M e. ZZ -> ta ) ) ) ) |
25 |
24
|
com34 |
|- ( M e. ZZ -> ( N e. ZZ -> ( M e. ZZ -> ( ( M + 1 ) <_ N -> ta ) ) ) ) |
26 |
25
|
pm2.43a |
|- ( M e. ZZ -> ( N e. ZZ -> ( ( M + 1 ) <_ N -> ta ) ) ) |
27 |
26
|
imp |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M + 1 ) <_ N -> ta ) ) |
28 |
7 27
|
sylbid |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M < N -> ta ) ) |
29 |
28
|
3impia |
|- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ta ) |