Step |
Hyp |
Ref |
Expression |
1 |
|
crctcshwlkn0lem.s |
|- ( ph -> S e. ( 1 ..^ N ) ) |
2 |
|
crctcshwlkn0lem.q |
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) ) |
3 |
|
breq1 |
|- ( x = J -> ( x <_ ( N - S ) <-> J <_ ( N - S ) ) ) |
4 |
|
fvoveq1 |
|- ( x = J -> ( P ` ( x + S ) ) = ( P ` ( J + S ) ) ) |
5 |
|
oveq1 |
|- ( x = J -> ( x + S ) = ( J + S ) ) |
6 |
5
|
fvoveq1d |
|- ( x = J -> ( P ` ( ( x + S ) - N ) ) = ( P ` ( ( J + S ) - N ) ) ) |
7 |
3 4 6
|
ifbieq12d |
|- ( x = J -> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) = if ( J <_ ( N - S ) , ( P ` ( J + S ) ) , ( P ` ( ( J + S ) - N ) ) ) ) |
8 |
|
0zd |
|- ( S e. ( 1 ..^ N ) -> 0 e. ZZ ) |
9 |
|
elfzoel2 |
|- ( S e. ( 1 ..^ N ) -> N e. ZZ ) |
10 |
|
elfzoelz |
|- ( S e. ( 1 ..^ N ) -> S e. ZZ ) |
11 |
9 10
|
zsubcld |
|- ( S e. ( 1 ..^ N ) -> ( N - S ) e. ZZ ) |
12 |
11
|
peano2zd |
|- ( S e. ( 1 ..^ N ) -> ( ( N - S ) + 1 ) e. ZZ ) |
13 |
|
elfzo1 |
|- ( S e. ( 1 ..^ N ) <-> ( S e. NN /\ N e. NN /\ S < N ) ) |
14 |
|
nnre |
|- ( S e. NN -> S e. RR ) |
15 |
|
nnre |
|- ( N e. NN -> N e. RR ) |
16 |
|
posdif |
|- ( ( S e. RR /\ N e. RR ) -> ( S < N <-> 0 < ( N - S ) ) ) |
17 |
|
0red |
|- ( ( S e. RR /\ N e. RR ) -> 0 e. RR ) |
18 |
|
resubcl |
|- ( ( N e. RR /\ S e. RR ) -> ( N - S ) e. RR ) |
19 |
18
|
ancoms |
|- ( ( S e. RR /\ N e. RR ) -> ( N - S ) e. RR ) |
20 |
|
ltle |
|- ( ( 0 e. RR /\ ( N - S ) e. RR ) -> ( 0 < ( N - S ) -> 0 <_ ( N - S ) ) ) |
21 |
17 19 20
|
syl2anc |
|- ( ( S e. RR /\ N e. RR ) -> ( 0 < ( N - S ) -> 0 <_ ( N - S ) ) ) |
22 |
19
|
lep1d |
|- ( ( S e. RR /\ N e. RR ) -> ( N - S ) <_ ( ( N - S ) + 1 ) ) |
23 |
|
1red |
|- ( ( S e. RR /\ N e. RR ) -> 1 e. RR ) |
24 |
19 23
|
readdcld |
|- ( ( S e. RR /\ N e. RR ) -> ( ( N - S ) + 1 ) e. RR ) |
25 |
|
letr |
|- ( ( 0 e. RR /\ ( N - S ) e. RR /\ ( ( N - S ) + 1 ) e. RR ) -> ( ( 0 <_ ( N - S ) /\ ( N - S ) <_ ( ( N - S ) + 1 ) ) -> 0 <_ ( ( N - S ) + 1 ) ) ) |
26 |
17 19 24 25
|
syl3anc |
|- ( ( S e. RR /\ N e. RR ) -> ( ( 0 <_ ( N - S ) /\ ( N - S ) <_ ( ( N - S ) + 1 ) ) -> 0 <_ ( ( N - S ) + 1 ) ) ) |
27 |
22 26
|
mpan2d |
|- ( ( S e. RR /\ N e. RR ) -> ( 0 <_ ( N - S ) -> 0 <_ ( ( N - S ) + 1 ) ) ) |
28 |
21 27
|
syld |
|- ( ( S e. RR /\ N e. RR ) -> ( 0 < ( N - S ) -> 0 <_ ( ( N - S ) + 1 ) ) ) |
29 |
16 28
|
sylbid |
|- ( ( S e. RR /\ N e. RR ) -> ( S < N -> 0 <_ ( ( N - S ) + 1 ) ) ) |
30 |
14 15 29
|
syl2an |
|- ( ( S e. NN /\ N e. NN ) -> ( S < N -> 0 <_ ( ( N - S ) + 1 ) ) ) |
31 |
30
|
3impia |
|- ( ( S e. NN /\ N e. NN /\ S < N ) -> 0 <_ ( ( N - S ) + 1 ) ) |
32 |
13 31
|
sylbi |
|- ( S e. ( 1 ..^ N ) -> 0 <_ ( ( N - S ) + 1 ) ) |
33 |
|
eluz2 |
|- ( ( ( N - S ) + 1 ) e. ( ZZ>= ` 0 ) <-> ( 0 e. ZZ /\ ( ( N - S ) + 1 ) e. ZZ /\ 0 <_ ( ( N - S ) + 1 ) ) ) |
34 |
8 12 32 33
|
syl3anbrc |
|- ( S e. ( 1 ..^ N ) -> ( ( N - S ) + 1 ) e. ( ZZ>= ` 0 ) ) |
35 |
1 34
|
syl |
|- ( ph -> ( ( N - S ) + 1 ) e. ( ZZ>= ` 0 ) ) |
36 |
|
fzss1 |
|- ( ( ( N - S ) + 1 ) e. ( ZZ>= ` 0 ) -> ( ( ( N - S ) + 1 ) ... N ) C_ ( 0 ... N ) ) |
37 |
35 36
|
syl |
|- ( ph -> ( ( ( N - S ) + 1 ) ... N ) C_ ( 0 ... N ) ) |
38 |
37
|
sselda |
|- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> J e. ( 0 ... N ) ) |
39 |
|
fvex |
|- ( P ` ( J + S ) ) e. _V |
40 |
|
fvex |
|- ( P ` ( ( J + S ) - N ) ) e. _V |
41 |
39 40
|
ifex |
|- if ( J <_ ( N - S ) , ( P ` ( J + S ) ) , ( P ` ( ( J + S ) - N ) ) ) e. _V |
42 |
41
|
a1i |
|- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> if ( J <_ ( N - S ) , ( P ` ( J + S ) ) , ( P ` ( ( J + S ) - N ) ) ) e. _V ) |
43 |
2 7 38 42
|
fvmptd3 |
|- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> ( Q ` J ) = if ( J <_ ( N - S ) , ( P ` ( J + S ) ) , ( P ` ( ( J + S ) - N ) ) ) ) |
44 |
|
elfz2 |
|- ( J e. ( ( ( N - S ) + 1 ) ... N ) <-> ( ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ J e. ZZ ) /\ ( ( ( N - S ) + 1 ) <_ J /\ J <_ N ) ) ) |
45 |
|
zre |
|- ( S e. ZZ -> S e. RR ) |
46 |
|
zre |
|- ( J e. ZZ -> J e. RR ) |
47 |
|
zre |
|- ( N e. ZZ -> N e. RR ) |
48 |
46 47
|
anim12i |
|- ( ( J e. ZZ /\ N e. ZZ ) -> ( J e. RR /\ N e. RR ) ) |
49 |
|
simprr |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> N e. RR ) |
50 |
|
simpl |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> S e. RR ) |
51 |
49 50
|
resubcld |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> ( N - S ) e. RR ) |
52 |
51
|
ltp1d |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> ( N - S ) < ( ( N - S ) + 1 ) ) |
53 |
|
1red |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> 1 e. RR ) |
54 |
51 53
|
readdcld |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> ( ( N - S ) + 1 ) e. RR ) |
55 |
|
simprl |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> J e. RR ) |
56 |
|
ltletr |
|- ( ( ( N - S ) e. RR /\ ( ( N - S ) + 1 ) e. RR /\ J e. RR ) -> ( ( ( N - S ) < ( ( N - S ) + 1 ) /\ ( ( N - S ) + 1 ) <_ J ) -> ( N - S ) < J ) ) |
57 |
51 54 55 56
|
syl3anc |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> ( ( ( N - S ) < ( ( N - S ) + 1 ) /\ ( ( N - S ) + 1 ) <_ J ) -> ( N - S ) < J ) ) |
58 |
52 57
|
mpand |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> ( ( ( N - S ) + 1 ) <_ J -> ( N - S ) < J ) ) |
59 |
51 55
|
ltnled |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> ( ( N - S ) < J <-> -. J <_ ( N - S ) ) ) |
60 |
58 59
|
sylibd |
|- ( ( S e. RR /\ ( J e. RR /\ N e. RR ) ) -> ( ( ( N - S ) + 1 ) <_ J -> -. J <_ ( N - S ) ) ) |
61 |
45 48 60
|
syl2an |
|- ( ( S e. ZZ /\ ( J e. ZZ /\ N e. ZZ ) ) -> ( ( ( N - S ) + 1 ) <_ J -> -. J <_ ( N - S ) ) ) |
62 |
61
|
expcom |
|- ( ( J e. ZZ /\ N e. ZZ ) -> ( S e. ZZ -> ( ( ( N - S ) + 1 ) <_ J -> -. J <_ ( N - S ) ) ) ) |
63 |
62
|
ancoms |
|- ( ( N e. ZZ /\ J e. ZZ ) -> ( S e. ZZ -> ( ( ( N - S ) + 1 ) <_ J -> -. J <_ ( N - S ) ) ) ) |
64 |
63
|
3adant1 |
|- ( ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ J e. ZZ ) -> ( S e. ZZ -> ( ( ( N - S ) + 1 ) <_ J -> -. J <_ ( N - S ) ) ) ) |
65 |
10 64
|
syl5com |
|- ( S e. ( 1 ..^ N ) -> ( ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ J e. ZZ ) -> ( ( ( N - S ) + 1 ) <_ J -> -. J <_ ( N - S ) ) ) ) |
66 |
65
|
com13 |
|- ( ( ( N - S ) + 1 ) <_ J -> ( ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ J e. ZZ ) -> ( S e. ( 1 ..^ N ) -> -. J <_ ( N - S ) ) ) ) |
67 |
66
|
adantr |
|- ( ( ( ( N - S ) + 1 ) <_ J /\ J <_ N ) -> ( ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ J e. ZZ ) -> ( S e. ( 1 ..^ N ) -> -. J <_ ( N - S ) ) ) ) |
68 |
67
|
impcom |
|- ( ( ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ J e. ZZ ) /\ ( ( ( N - S ) + 1 ) <_ J /\ J <_ N ) ) -> ( S e. ( 1 ..^ N ) -> -. J <_ ( N - S ) ) ) |
69 |
68
|
com12 |
|- ( S e. ( 1 ..^ N ) -> ( ( ( ( ( N - S ) + 1 ) e. ZZ /\ N e. ZZ /\ J e. ZZ ) /\ ( ( ( N - S ) + 1 ) <_ J /\ J <_ N ) ) -> -. J <_ ( N - S ) ) ) |
70 |
44 69
|
syl5bi |
|- ( S e. ( 1 ..^ N ) -> ( J e. ( ( ( N - S ) + 1 ) ... N ) -> -. J <_ ( N - S ) ) ) |
71 |
1 70
|
syl |
|- ( ph -> ( J e. ( ( ( N - S ) + 1 ) ... N ) -> -. J <_ ( N - S ) ) ) |
72 |
71
|
imp |
|- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> -. J <_ ( N - S ) ) |
73 |
72
|
iffalsed |
|- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> if ( J <_ ( N - S ) , ( P ` ( J + S ) ) , ( P ` ( ( J + S ) - N ) ) ) = ( P ` ( ( J + S ) - N ) ) ) |
74 |
43 73
|
eqtrd |
|- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> ( Q ` J ) = ( P ` ( ( J + S ) - N ) ) ) |