Step |
Hyp |
Ref |
Expression |
1 |
|
fzind.1 |
|- ( x = M -> ( ph <-> ps ) ) |
2 |
|
fzind.2 |
|- ( x = y -> ( ph <-> ch ) ) |
3 |
|
fzind.3 |
|- ( x = ( y + 1 ) -> ( ph <-> th ) ) |
4 |
|
fzind.4 |
|- ( x = K -> ( ph <-> ta ) ) |
5 |
|
fzind.5 |
|- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ps ) |
6 |
|
fzind.6 |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ M <_ y /\ y < N ) ) -> ( ch -> th ) ) |
7 |
|
breq1 |
|- ( x = M -> ( x <_ N <-> M <_ N ) ) |
8 |
7
|
anbi2d |
|- ( x = M -> ( ( N e. ZZ /\ x <_ N ) <-> ( N e. ZZ /\ M <_ N ) ) ) |
9 |
8 1
|
imbi12d |
|- ( x = M -> ( ( ( N e. ZZ /\ x <_ N ) -> ph ) <-> ( ( N e. ZZ /\ M <_ N ) -> ps ) ) ) |
10 |
|
breq1 |
|- ( x = y -> ( x <_ N <-> y <_ N ) ) |
11 |
10
|
anbi2d |
|- ( x = y -> ( ( N e. ZZ /\ x <_ N ) <-> ( N e. ZZ /\ y <_ N ) ) ) |
12 |
11 2
|
imbi12d |
|- ( x = y -> ( ( ( N e. ZZ /\ x <_ N ) -> ph ) <-> ( ( N e. ZZ /\ y <_ N ) -> ch ) ) ) |
13 |
|
breq1 |
|- ( x = ( y + 1 ) -> ( x <_ N <-> ( y + 1 ) <_ N ) ) |
14 |
13
|
anbi2d |
|- ( x = ( y + 1 ) -> ( ( N e. ZZ /\ x <_ N ) <-> ( N e. ZZ /\ ( y + 1 ) <_ N ) ) ) |
15 |
14 3
|
imbi12d |
|- ( x = ( y + 1 ) -> ( ( ( N e. ZZ /\ x <_ N ) -> ph ) <-> ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> th ) ) ) |
16 |
|
breq1 |
|- ( x = K -> ( x <_ N <-> K <_ N ) ) |
17 |
16
|
anbi2d |
|- ( x = K -> ( ( N e. ZZ /\ x <_ N ) <-> ( N e. ZZ /\ K <_ N ) ) ) |
18 |
17 4
|
imbi12d |
|- ( x = K -> ( ( ( N e. ZZ /\ x <_ N ) -> ph ) <-> ( ( N e. ZZ /\ K <_ N ) -> ta ) ) ) |
19 |
5
|
3expib |
|- ( M e. ZZ -> ( ( N e. ZZ /\ M <_ N ) -> ps ) ) |
20 |
|
zre |
|- ( y e. ZZ -> y e. RR ) |
21 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
22 |
|
p1le |
|- ( ( y e. RR /\ N e. RR /\ ( y + 1 ) <_ N ) -> y <_ N ) |
23 |
22
|
3expia |
|- ( ( y e. RR /\ N e. RR ) -> ( ( y + 1 ) <_ N -> y <_ N ) ) |
24 |
20 21 23
|
syl2an |
|- ( ( y e. ZZ /\ N e. ZZ ) -> ( ( y + 1 ) <_ N -> y <_ N ) ) |
25 |
24
|
imdistanda |
|- ( y e. ZZ -> ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> ( N e. ZZ /\ y <_ N ) ) ) |
26 |
25
|
imim1d |
|- ( y e. ZZ -> ( ( ( N e. ZZ /\ y <_ N ) -> ch ) -> ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> ch ) ) ) |
27 |
26
|
3ad2ant2 |
|- ( ( M e. ZZ /\ y e. ZZ /\ M <_ y ) -> ( ( ( N e. ZZ /\ y <_ N ) -> ch ) -> ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> ch ) ) ) |
28 |
|
zltp1le |
|- ( ( y e. ZZ /\ N e. ZZ ) -> ( y < N <-> ( y + 1 ) <_ N ) ) |
29 |
28
|
adantlr |
|- ( ( ( y e. ZZ /\ M <_ y ) /\ N e. ZZ ) -> ( y < N <-> ( y + 1 ) <_ N ) ) |
30 |
29
|
expcom |
|- ( N e. ZZ -> ( ( y e. ZZ /\ M <_ y ) -> ( y < N <-> ( y + 1 ) <_ N ) ) ) |
31 |
30
|
pm5.32d |
|- ( N e. ZZ -> ( ( ( y e. ZZ /\ M <_ y ) /\ y < N ) <-> ( ( y e. ZZ /\ M <_ y ) /\ ( y + 1 ) <_ N ) ) ) |
32 |
31
|
adantl |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( y e. ZZ /\ M <_ y ) /\ y < N ) <-> ( ( y e. ZZ /\ M <_ y ) /\ ( y + 1 ) <_ N ) ) ) |
33 |
6
|
expcom |
|- ( ( y e. ZZ /\ M <_ y /\ y < N ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ch -> th ) ) ) |
34 |
33
|
3expa |
|- ( ( ( y e. ZZ /\ M <_ y ) /\ y < N ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ch -> th ) ) ) |
35 |
34
|
com12 |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( y e. ZZ /\ M <_ y ) /\ y < N ) -> ( ch -> th ) ) ) |
36 |
32 35
|
sylbird |
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( y e. ZZ /\ M <_ y ) /\ ( y + 1 ) <_ N ) -> ( ch -> th ) ) ) |
37 |
36
|
ex |
|- ( M e. ZZ -> ( N e. ZZ -> ( ( ( y e. ZZ /\ M <_ y ) /\ ( y + 1 ) <_ N ) -> ( ch -> th ) ) ) ) |
38 |
37
|
com23 |
|- ( M e. ZZ -> ( ( ( y e. ZZ /\ M <_ y ) /\ ( y + 1 ) <_ N ) -> ( N e. ZZ -> ( ch -> th ) ) ) ) |
39 |
38
|
expd |
|- ( M e. ZZ -> ( ( y e. ZZ /\ M <_ y ) -> ( ( y + 1 ) <_ N -> ( N e. ZZ -> ( ch -> th ) ) ) ) ) |
40 |
39
|
3impib |
|- ( ( M e. ZZ /\ y e. ZZ /\ M <_ y ) -> ( ( y + 1 ) <_ N -> ( N e. ZZ -> ( ch -> th ) ) ) ) |
41 |
40
|
impcomd |
|- ( ( M e. ZZ /\ y e. ZZ /\ M <_ y ) -> ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> ( ch -> th ) ) ) |
42 |
41
|
a2d |
|- ( ( M e. ZZ /\ y e. ZZ /\ M <_ y ) -> ( ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> ch ) -> ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> th ) ) ) |
43 |
27 42
|
syld |
|- ( ( M e. ZZ /\ y e. ZZ /\ M <_ y ) -> ( ( ( N e. ZZ /\ y <_ N ) -> ch ) -> ( ( N e. ZZ /\ ( y + 1 ) <_ N ) -> th ) ) ) |
44 |
9 12 15 18 19 43
|
uzind |
|- ( ( M e. ZZ /\ K e. ZZ /\ M <_ K ) -> ( ( N e. ZZ /\ K <_ N ) -> ta ) ) |
45 |
44
|
expcomd |
|- ( ( M e. ZZ /\ K e. ZZ /\ M <_ K ) -> ( K <_ N -> ( N e. ZZ -> ta ) ) ) |
46 |
45
|
3expb |
|- ( ( M e. ZZ /\ ( K e. ZZ /\ M <_ K ) ) -> ( K <_ N -> ( N e. ZZ -> ta ) ) ) |
47 |
46
|
expcom |
|- ( ( K e. ZZ /\ M <_ K ) -> ( M e. ZZ -> ( K <_ N -> ( N e. ZZ -> ta ) ) ) ) |
48 |
47
|
com23 |
|- ( ( K e. ZZ /\ M <_ K ) -> ( K <_ N -> ( M e. ZZ -> ( N e. ZZ -> ta ) ) ) ) |
49 |
48
|
3impia |
|- ( ( K e. ZZ /\ M <_ K /\ K <_ N ) -> ( M e. ZZ -> ( N e. ZZ -> ta ) ) ) |
50 |
49
|
impd |
|- ( ( K e. ZZ /\ M <_ K /\ K <_ N ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ta ) ) |
51 |
50
|
impcom |
|- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M <_ K /\ K <_ N ) ) -> ta ) |