Metamath Proof Explorer

Theorem clwwisshclwwslemlem

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

Ref Expression
Assertion clwwisshclwwslemlem ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 1 ) + 𝐵 ) mod 𝐿 ) ) } ∈ 𝑅 )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
2 1 3ad2ant2 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℂ )
3 1cnd ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 1 ∈ ℂ )
4 zcn ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
5 4 3ad2ant3 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐵 ∈ ℂ )
6 2 3 5 add32d ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 1 ) + 𝐵 ) = ( ( 𝐴 + 𝐵 ) + 1 ) )
7 6 fvoveq1d ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑊 ‘ ( ( ( 𝐴 + 1 ) + 𝐵 ) mod 𝐿 ) ) = ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) )
8 7 3ad2ant1 ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → ( 𝑊 ‘ ( ( ( 𝐴 + 1 ) + 𝐵 ) mod 𝐿 ) ) = ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) )
9 8 preq2d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 1 ) + 𝐵 ) mod 𝐿 ) ) } = { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } )
10 zaddcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
11 10 3adant1 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℤ )
12 eluz2nn ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) → 𝐿 ∈ ℕ )
13 12 3ad2ant1 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐿 ∈ ℕ )
14 11 13 zmodcld ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ℕ0 )
15 14 adantr ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ℕ0 )
16 uz2m1nn ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐿 − 1 ) ∈ ℕ )
17 16 3ad2ant1 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐿 − 1 ) ∈ ℕ )
18 17 adantr ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( 𝐿 − 1 ) ∈ ℕ )
19 simpr ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) )
20 elfzo0 ⊢ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ ( 𝐿 − 1 ) ) ↔ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ℕ0 ∧ ( 𝐿 − 1 ) ∈ ℕ ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) )
21 15 18 19 20 syl3anbrc ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ ( 𝐿 − 1 ) ) )
22 fveq2 ⊢ ( 𝑖 = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) → ( 𝑊 ‘ 𝑖 ) = ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) )
23 fvoveq1 ⊢ ( 𝑖 = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) → ( 𝑊 ‘ ( 𝑖 + 1 ) ) = ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) )
24 22 23 preq12d ⊢ ( 𝑖 = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) → { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } = { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) } )
25 24 eleq1d ⊢ ( 𝑖 = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) → ( { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ↔ { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) } ∈ 𝑅 ) )
26 25 rspcv ⊢ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ ( 𝐿 − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) } ∈ 𝑅 ) )
27 21 26 syl ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) } ∈ 𝑅 ) )
28 10 zred ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
29 28 3adant1 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
30 29 adantr ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
31 12 nnrpd ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) → 𝐿 ∈ ℝ+ )
32 31 3ad2ant1 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐿 ∈ ℝ+ )
33 32 adantr ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → 𝐿 ∈ ℝ+ )
34 modltm1p1mod ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 𝐿 ∈ ℝ+ ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) = ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) )
35 30 33 19 34 syl3anc ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) = ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) )
36 35 fveq2d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) = ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) )
37 36 preq2d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } = { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) } )
38 37 eleq1d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ↔ { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) + 1 ) ) } ∈ 𝑅 ) )
39 27 38 sylibrd ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) )
40 39 impancom ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ) → ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) )
41 40 3adant3 ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) )
42 zmodfzo ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℤ ∧ 𝐿 ∈ ℕ ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ 𝐿 ) )
43 11 13 42 syl2anc ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ 𝐿 ) )
44 elfzonlteqm1 ⊢ ( ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ 𝐿 ) ∧ ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) = ( 𝐿 − 1 ) )
45 44 eqcomd ⊢ ( ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ 𝐿 ) ∧ ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) ) → ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) )
46 45 ex ⊢ ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ∈ ( 0 ..^ 𝐿 ) → ( ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) )
47 43 46 syl ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) )
48 fveq2 ⊢ ( ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) → ( 𝑊 ‘ ( 𝐿 − 1 ) ) = ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) )
49 48 adantl ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( 𝑊 ‘ ( 𝐿 − 1 ) ) = ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) )
50 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
51 zre ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
52 readdcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
53 50 51 52 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
54 53 3adant1 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
55 54 32 jca ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 𝐿 ∈ ℝ+ ) )
56 55 adantr ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 𝐿 ∈ ℝ+ ) )
57 simpr ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) )
58 57 eqcomd ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( ( 𝐴 + 𝐵 ) mod 𝐿 ) = ( 𝐿 − 1 ) )
59 modm1p1mod0 ⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 𝐿 ∈ ℝ+ ) → ( ( ( 𝐴 + 𝐵 ) mod 𝐿 ) = ( 𝐿 − 1 ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) = 0 ) )
60 56 58 59 sylc ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) = 0 )
61 60 eqcomd ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → 0 = ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) )
62 61 fveq2d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( 𝑊 ‘ 0 ) = ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) )
63 49 62 preq12d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } = { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } )
64 63 eleq1d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ↔ { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) )
65 64 biimpd ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) → ( { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) )
66 65 ex ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐿 − 1 ) = ( ( 𝐴 + 𝐵 ) mod 𝐿 ) → ( { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) ) )
67 47 66 syld ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → ( { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) ) )
68 67 com23 ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 → ( ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) ) )
69 68 imp ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → ( ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) )
70 69 3adant2 ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → ( ¬ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) < ( 𝐿 − 1 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 ) )
71 41 70 pm2.61d ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 𝐵 ) + 1 ) mod 𝐿 ) ) } ∈ 𝑅 )
72 9 71 eqeltrd ⊢ ( ( ( 𝐿 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( 𝐿 − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ 𝑅 ∧ { ( 𝑊 ‘ ( 𝐿 − 1 ) ) , ( 𝑊 ‘ 0 ) } ∈ 𝑅 ) → { ( 𝑊 ‘ ( ( 𝐴 + 𝐵 ) mod 𝐿 ) ) , ( 𝑊 ‘ ( ( ( 𝐴 + 1 ) + 𝐵 ) mod 𝐿 ) ) } ∈ 𝑅 )