| 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 ) ) } ) ) |