Step |
Hyp |
Ref |
Expression |
1 |
|
clwlkclwwlklem2.f |
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) ) |
2 |
|
breq1 |
|- ( x = I -> ( x < ( ( # ` P ) - 2 ) <-> I < ( ( # ` P ) - 2 ) ) ) |
3 |
|
fveq2 |
|- ( x = I -> ( P ` x ) = ( P ` I ) ) |
4 |
|
fvoveq1 |
|- ( x = I -> ( P ` ( x + 1 ) ) = ( P ` ( I + 1 ) ) ) |
5 |
3 4
|
preq12d |
|- ( x = I -> { ( P ` x ) , ( P ` ( x + 1 ) ) } = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) |
6 |
5
|
fveq2d |
|- ( x = I -> ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) |
7 |
3
|
preq1d |
|- ( x = I -> { ( P ` x ) , ( P ` 0 ) } = { ( P ` I ) , ( P ` 0 ) } ) |
8 |
7
|
fveq2d |
|- ( x = I -> ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) = ( `' E ` { ( P ` I ) , ( P ` 0 ) } ) ) |
9 |
2 6 8
|
ifbieq12d |
|- ( x = I -> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) = if ( I < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) , ( `' E ` { ( P ` I ) , ( P ` 0 ) } ) ) ) |
10 |
|
elfzolt2 |
|- ( I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) -> I < ( ( # ` P ) - 2 ) ) |
11 |
10
|
adantl |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) -> I < ( ( # ` P ) - 2 ) ) |
12 |
11
|
iftrued |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) -> if ( I < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) , ( `' E ` { ( P ` I ) , ( P ` 0 ) } ) ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) |
13 |
9 12
|
sylan9eqr |
|- ( ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) /\ x = I ) -> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) |
14 |
|
nn0z |
|- ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ ) |
15 |
|
2z |
|- 2 e. ZZ |
16 |
15
|
a1i |
|- ( ( # ` P ) e. NN0 -> 2 e. ZZ ) |
17 |
14 16
|
zsubcld |
|- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. ZZ ) |
18 |
|
peano2zm |
|- ( ( # ` P ) e. ZZ -> ( ( # ` P ) - 1 ) e. ZZ ) |
19 |
14 18
|
syl |
|- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. ZZ ) |
20 |
|
1red |
|- ( ( # ` P ) e. NN0 -> 1 e. RR ) |
21 |
|
2re |
|- 2 e. RR |
22 |
21
|
a1i |
|- ( ( # ` P ) e. NN0 -> 2 e. RR ) |
23 |
|
nn0re |
|- ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR ) |
24 |
|
1le2 |
|- 1 <_ 2 |
25 |
24
|
a1i |
|- ( ( # ` P ) e. NN0 -> 1 <_ 2 ) |
26 |
20 22 23 25
|
lesub2dd |
|- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) <_ ( ( # ` P ) - 1 ) ) |
27 |
|
eluz2 |
|- ( ( ( # ` P ) - 1 ) e. ( ZZ>= ` ( ( # ` P ) - 2 ) ) <-> ( ( ( # ` P ) - 2 ) e. ZZ /\ ( ( # ` P ) - 1 ) e. ZZ /\ ( ( # ` P ) - 2 ) <_ ( ( # ` P ) - 1 ) ) ) |
28 |
17 19 26 27
|
syl3anbrc |
|- ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 1 ) e. ( ZZ>= ` ( ( # ` P ) - 2 ) ) ) |
29 |
|
fzoss2 |
|- ( ( ( # ` P ) - 1 ) e. ( ZZ>= ` ( ( # ` P ) - 2 ) ) -> ( 0 ..^ ( ( # ` P ) - 2 ) ) C_ ( 0 ..^ ( ( # ` P ) - 1 ) ) ) |
30 |
28 29
|
syl |
|- ( ( # ` P ) e. NN0 -> ( 0 ..^ ( ( # ` P ) - 2 ) ) C_ ( 0 ..^ ( ( # ` P ) - 1 ) ) ) |
31 |
30
|
sselda |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) -> I e. ( 0 ..^ ( ( # ` P ) - 1 ) ) ) |
32 |
|
fvexd |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) -> ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) e. _V ) |
33 |
1 13 31 32
|
fvmptd2 |
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) |