Metamath Proof Explorer


Theorem clwwisshclwwslemlem

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

Ref Expression
Assertion clwwisshclwwslemlem L 2 A B i 0 ..^ L 1 W i W i + 1 R W L 1 W 0 R W A + B mod L W A + 1 + B mod L R

Proof

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