Metamath Proof Explorer

Theorem clwlkclwwlklem2fv2

Description: Lemma 4b 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 clwlkclwwlklem2fv2 
|- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( F ` ( ( # ` P ) - 2 ) ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )

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 simpr 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> x = ( ( # ` P ) - 2 ) )
3 nn0z 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. ZZ )
4 2z 
 |-  2 e. ZZ
5 3 4 jctir 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) e. ZZ /\ 2 e. ZZ ) )
6 zsubcl 
 |-  ( ( ( # ` P ) e. ZZ /\ 2 e. ZZ ) -> ( ( # ` P ) - 2 ) e. ZZ )
7 5 6 syl 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. ZZ )
8 7 adantr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. ZZ )
9 8 adantr 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> ( ( # ` P ) - 2 ) e. ZZ )
10 2 9 eqeltrd 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> x e. ZZ )
11 10 ex 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( x = ( ( # ` P ) - 2 ) -> x e. ZZ ) )
12 zre 
 |-  ( x e. ZZ -> x e. RR )
13 nn0re 
 |-  ( ( # ` P ) e. NN0 -> ( # ` P ) e. RR )
14 2re 
 |-  2 e. RR
15 14 a1i 
 |-  ( ( # ` P ) e. NN0 -> 2 e. RR )
16 13 15 resubcld 
 |-  ( ( # ` P ) e. NN0 -> ( ( # ` P ) - 2 ) e. RR )
17 16 adantr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. RR )
18 lttri3 
 |-  ( ( x e. RR /\ ( ( # ` P ) - 2 ) e. RR ) -> ( x = ( ( # ` P ) - 2 ) <-> ( -. x < ( ( # ` P ) - 2 ) /\ -. ( ( # ` P ) - 2 ) < x ) ) )
19 12 17 18 syl2anr 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x e. ZZ ) -> ( x = ( ( # ` P ) - 2 ) <-> ( -. x < ( ( # ` P ) - 2 ) /\ -. ( ( # ` P ) - 2 ) < x ) ) )
20 simpl 
 |-  ( ( -. x < ( ( # ` P ) - 2 ) /\ -. ( ( # ` P ) - 2 ) < x ) -> -. x < ( ( # ` P ) - 2 ) )
21 19 20 biimtrdi 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x e. ZZ ) -> ( x = ( ( # ` P ) - 2 ) -> -. x < ( ( # ` P ) - 2 ) ) )
22 21 ex 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( x e. ZZ -> ( x = ( ( # ` P ) - 2 ) -> -. x < ( ( # ` P ) - 2 ) ) ) )
23 11 22 syld 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( x = ( ( # ` P ) - 2 ) -> ( x = ( ( # ` P ) - 2 ) -> -. x < ( ( # ` P ) - 2 ) ) ) )
24 23 com13 
 |-  ( x = ( ( # ` P ) - 2 ) -> ( x = ( ( # ` P ) - 2 ) -> ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> -. x < ( ( # ` P ) - 2 ) ) ) )
25 24 pm2.43i 
 |-  ( x = ( ( # ` P ) - 2 ) -> ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> -. x < ( ( # ` P ) - 2 ) ) )
26 25 impcom 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> -. x < ( ( # ` P ) - 2 ) )
27 26 iffalsed 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) = ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) )
28 fveq2 
 |-  ( x = ( ( # ` P ) - 2 ) -> ( P ` x ) = ( P ` ( ( # ` P ) - 2 ) ) )
29 28 adantl 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> ( P ` x ) = ( P ` ( ( # ` P ) - 2 ) ) )
30 29 preq1d 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> { ( P ` x ) , ( P ` 0 ) } = { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } )
31 30 fveq2d 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
32 27 31 eqtrd 
 |-  ( ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) /\ x = ( ( # ` P ) - 2 ) ) -> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
33 5 adantr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) e. ZZ /\ 2 e. ZZ ) )
34 33 6 syl 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. ZZ )
35 13 15 subge0d 
 |-  ( ( # ` P ) e. NN0 -> ( 0 <_ ( ( # ` P ) - 2 ) <-> 2 <_ ( # ` P ) ) )
36 35 biimpar 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 0 <_ ( ( # ` P ) - 2 ) )
37 elnn0z 
 |-  ( ( ( # ` P ) - 2 ) e. NN0 <-> ( ( ( # ` P ) - 2 ) e. ZZ /\ 0 <_ ( ( # ` P ) - 2 ) ) )
38 34 36 37 sylanbrc 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. NN0 )
39 nn0ge2m1nn 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 1 ) e. NN )
40 1red 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 1 e. RR )
41 14 a1i 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 2 e. RR )
42 13 adantr 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( # ` P ) e. RR )
43 1lt2 
 |-  1 < 2
44 43 a1i 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> 1 < 2 )
45 40 41 42 44 ltsub2dd 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) < ( ( # ` P ) - 1 ) )
46 elfzo0 
 |-  ( ( ( # ` P ) - 2 ) e. ( 0 ..^ ( ( # ` P ) - 1 ) ) <-> ( ( ( # ` P ) - 2 ) e. NN0 /\ ( ( # ` P ) - 1 ) e. NN /\ ( ( # ` P ) - 2 ) < ( ( # ` P ) - 1 ) ) )
47 38 39 45 46 syl3anbrc 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( ( # ` P ) - 2 ) e. ( 0 ..^ ( ( # ` P ) - 1 ) ) )
48 fvexd 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) e. _V )
49 1 32 47 48 fvmptd2 
 |-  ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( F ` ( ( # ` P ) - 2 ) ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )