Metamath Proof Explorer

Theorem clwlkclwwlklem2fv1

Description: Lemma 4a for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 22-Jun-2018)

Ref Expression
Hypothesis clwlkclwwlklem2.f 
|- F = ( x e. ( 0 ..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )
Assertion clwlkclwwlklem2fv1 
|- ( ( ( # ` P ) e. NN0 /\ I e. ( 0 ..^ ( ( # ` P ) - 2 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )

Proof

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