Metamath Proof Explorer

Theorem clwwisshclwwslemlem

Description: Lemma for clwwisshclwwslem . (Contributed by Alexander van der Vekens, 23-Mar-2018)

Ref Expression
Assertion clwwisshclwwslemlem 
|- ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + 1 ) + B ) mod L ) ) } e. R )

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 1 3ad2ant2 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> A e. CC )
3 1cnd 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> 1 e. CC )
4 zcn 
 |-  ( B e. ZZ -> B e. CC )
5 4 3ad2ant3 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> B e. CC )
6 2 3 5 add32d 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( ( A + 1 ) + B ) = ( ( A + B ) + 1 ) )
7 6 fvoveq1d 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( W ` ( ( ( A + 1 ) + B ) mod L ) ) = ( W ` ( ( ( A + B ) + 1 ) mod L ) ) )
8 7 3ad2ant1 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> ( W ` ( ( ( A + 1 ) + B ) mod L ) ) = ( W ` ( ( ( A + B ) + 1 ) mod L ) ) )
9 8 preq2d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + 1 ) + B ) mod L ) ) } = { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } )
10 zaddcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
11 10 3adant1 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
12 eluz2nn 
 |-  ( L e. ( ZZ>= ` 2 ) -> L e. NN )
13 12 3ad2ant1 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> L e. NN )
14 11 13 zmodcld 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( ( A + B ) mod L ) e. NN0 )
15 14 adantr 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( ( A + B ) mod L ) e. NN0 )
16 uz2m1nn 
 |-  ( L e. ( ZZ>= ` 2 ) -> ( L - 1 ) e. NN )
17 16 3ad2ant1 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( L - 1 ) e. NN )
18 17 adantr 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( L - 1 ) e. NN )
19 simpr 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( ( A + B ) mod L ) < ( L - 1 ) )
20 elfzo0 
 |-  ( ( ( A + B ) mod L ) e. ( 0 ..^ ( L - 1 ) ) <-> ( ( ( A + B ) mod L ) e. NN0 /\ ( L - 1 ) e. NN /\ ( ( A + B ) mod L ) < ( L - 1 ) ) )
21 15 18 19 20 syl3anbrc 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( ( A + B ) mod L ) e. ( 0 ..^ ( L - 1 ) ) )
22 fveq2 
 |-  ( i = ( ( A + B ) mod L ) -> ( W ` i ) = ( W ` ( ( A + B ) mod L ) ) )
23 fvoveq1 
 |-  ( i = ( ( A + B ) mod L ) -> ( W ` ( i + 1 ) ) = ( W ` ( ( ( A + B ) mod L ) + 1 ) ) )
24 22 23 preq12d 
 |-  ( i = ( ( A + B ) mod L ) -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) mod L ) + 1 ) ) } )
25 24 eleq1d 
 |-  ( i = ( ( A + B ) mod L ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R <-> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) mod L ) + 1 ) ) } e. R ) )
26 25 rspcv 
 |-  ( ( ( A + B ) mod L ) e. ( 0 ..^ ( L - 1 ) ) -> ( A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) mod L ) + 1 ) ) } e. R ) )
27 21 26 syl 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) mod L ) + 1 ) ) } e. R ) )
28 10 zred 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. RR )
29 28 3adant1 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. RR )
30 29 adantr 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( A + B ) e. RR )
31 12 nnrpd 
 |-  ( L e. ( ZZ>= ` 2 ) -> L e. RR+ )
32 31 3ad2ant1 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> L e. RR+ )
33 32 adantr 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> L e. RR+ )
34 modltm1p1mod 
 |-  ( ( ( A + B ) e. RR /\ L e. RR+ /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( ( ( A + B ) + 1 ) mod L ) = ( ( ( A + B ) mod L ) + 1 ) )
35 30 33 19 34 syl3anc 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( ( ( A + B ) + 1 ) mod L ) = ( ( ( A + B ) mod L ) + 1 ) )
36 35 fveq2d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( W ` ( ( ( A + B ) + 1 ) mod L ) ) = ( W ` ( ( ( A + B ) mod L ) + 1 ) ) )
37 36 preq2d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } = { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) mod L ) + 1 ) ) } )
38 37 eleq1d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R <-> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) mod L ) + 1 ) ) } e. R ) )
39 27 38 sylibrd 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) )
40 39 impancom 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R ) -> ( ( ( A + B ) mod L ) < ( L - 1 ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) )
41 40 3adant3 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> ( ( ( A + B ) mod L ) < ( L - 1 ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) )
42 zmodfzo 
 |-  ( ( ( A + B ) e. ZZ /\ L e. NN ) -> ( ( A + B ) mod L ) e. ( 0 ..^ L ) )
43 11 13 42 syl2anc 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( ( A + B ) mod L ) e. ( 0 ..^ L ) )
44 elfzonlteqm1 
 |-  ( ( ( ( A + B ) mod L ) e. ( 0 ..^ L ) /\ -. ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( ( A + B ) mod L ) = ( L - 1 ) )
45 44 eqcomd 
 |-  ( ( ( ( A + B ) mod L ) e. ( 0 ..^ L ) /\ -. ( ( A + B ) mod L ) < ( L - 1 ) ) -> ( L - 1 ) = ( ( A + B ) mod L ) )
46 45 ex 
 |-  ( ( ( A + B ) mod L ) e. ( 0 ..^ L ) -> ( -. ( ( A + B ) mod L ) < ( L - 1 ) -> ( L - 1 ) = ( ( A + B ) mod L ) ) )
47 43 46 syl 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( -. ( ( A + B ) mod L ) < ( L - 1 ) -> ( L - 1 ) = ( ( A + B ) mod L ) ) )
48 fveq2 
 |-  ( ( L - 1 ) = ( ( A + B ) mod L ) -> ( W ` ( L - 1 ) ) = ( W ` ( ( A + B ) mod L ) ) )
49 48 adantl 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( W ` ( L - 1 ) ) = ( W ` ( ( A + B ) mod L ) ) )
50 zre 
 |-  ( A e. ZZ -> A e. RR )
51 zre 
 |-  ( B e. ZZ -> B e. RR )
52 readdcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
53 50 51 52 syl2an 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. RR )
54 53 3adant1 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. RR )
55 54 32 jca 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( ( A + B ) e. RR /\ L e. RR+ ) )
56 55 adantr 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( ( A + B ) e. RR /\ L e. RR+ ) )
57 simpr 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( L - 1 ) = ( ( A + B ) mod L ) )
58 57 eqcomd 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( ( A + B ) mod L ) = ( L - 1 ) )
59 modm1p1mod0 
 |-  ( ( ( A + B ) e. RR /\ L e. RR+ ) -> ( ( ( A + B ) mod L ) = ( L - 1 ) -> ( ( ( A + B ) + 1 ) mod L ) = 0 ) )
60 56 58 59 sylc 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( ( ( A + B ) + 1 ) mod L ) = 0 )
61 60 eqcomd 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> 0 = ( ( ( A + B ) + 1 ) mod L ) )
62 61 fveq2d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( W ` 0 ) = ( W ` ( ( ( A + B ) + 1 ) mod L ) ) )
63 49 62 preq12d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> { ( W ` ( L - 1 ) ) , ( W ` 0 ) } = { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } )
64 63 eleq1d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R <-> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) )
65 64 biimpd 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ ( L - 1 ) = ( ( A + B ) mod L ) ) -> ( { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) )
66 65 ex 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( ( L - 1 ) = ( ( A + B ) mod L ) -> ( { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) ) )
67 47 66 syld 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( -. ( ( A + B ) mod L ) < ( L - 1 ) -> ( { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) ) )
68 67 com23 
 |-  ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) -> ( { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R -> ( -. ( ( A + B ) mod L ) < ( L - 1 ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) ) )
69 68 imp 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> ( -. ( ( A + B ) mod L ) < ( L - 1 ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) )
70 69 3adant2 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> ( -. ( ( A + B ) mod L ) < ( L - 1 ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R ) )
71 41 70 pm2.61d 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + B ) + 1 ) mod L ) ) } e. R )
72 9 71 eqeltrd 
 |-  ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0 ..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + 1 ) + B ) mod L ) ) } e. R )