Metamath Proof Explorer

Theorem crctcshwlkn0lem3

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s 
|- ( ph -> S e. ( 1 ..^ N ) )
crctcshwlkn0lem.q 
|- Q = ( x e. ( 0 ... N ) |-> if ( x <_ ( N - S ) , ( P ` ( x + S ) ) , ( P ` ( ( x + S ) - N ) ) ) )
Assertion crctcshwlkn0lem3 
|- ( ( ph /\ J e. ( ( ( N - S ) + 1 ) ... N ) ) -> ( Q ` J ) = ( P ` ( ( J + S ) - N ) ) )

Proof

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