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