Metamath Proof Explorer


Theorem lighneallem4b

Description: Lemma 2 for lighneallem4 . (Contributed by AV, 16-Aug-2021)

Ref Expression
Assertion lighneallem4b A2M2¬2Mk=0M11kAk2

Proof

Step Hyp Ref Expression
1 2z 2
2 1 a1i A2M2¬2M2
3 fzfid A2M20M1Fin
4 neg1z 1
5 elfznn0 k0M1k0
6 zexpcl 1k01k
7 4 5 6 sylancr k0M11k
8 7 adantl A2M2k0M11k
9 eluzge2nn0 A2A0
10 9 adantr A2M2A0
11 10 adantr A2M2k0M1A0
12 5 adantl A2M2k0M1k0
13 11 12 nn0expcld A2M2k0M1Ak0
14 13 nn0zd A2M2k0M1Ak
15 8 14 zmulcld A2M2k0M11kAk
16 3 15 fsumzcl A2M2k=0M11kAk
17 16 3adant3 A2M2¬2Mk=0M11kAk
18 simp1 A2M2¬2MA2
19 3z 3
20 19 a1i A2M2¬2M3
21 eluzelz M2M
22 21 3ad2ant2 A2M2¬2MM
23 eluz2 M22M2M
24 2re 2
25 24 a1i M2
26 zre MM
27 25 26 leloed M2M2<M2=M
28 zltp1le 2M2<M2+1M
29 1 28 mpan M2<M2+1M
30 29 biimpd M2<M2+1M
31 df-3 3=2+1
32 31 breq1i 3M2+1M
33 30 32 syl6ibr M2<M3M
34 33 a1i ¬2MM2<M3M
35 34 com13 2<MM¬2M3M
36 z2even 22
37 breq2 2=M222M
38 36 37 mpbii 2=M2M
39 38 pm2.24d 2=M¬2M3M
40 39 a1d 2=MM¬2M3M
41 35 40 jaoi 2<M2=MM¬2M3M
42 41 com12 M2<M2=M¬2M3M
43 27 42 sylbid M2M¬2M3M
44 43 imp M2M¬2M3M
45 44 3adant1 2M2M¬2M3M
46 23 45 sylbi M2¬2M3M
47 46 imp M2¬2M3M
48 47 3adant1 A2M2¬2M3M
49 eluz2 M33M3M
50 20 22 48 49 syl3anbrc A2M2¬2MM3
51 eluzelcn A2A
52 51 3ad2ant1 A2M2¬2MA
53 eluz2nn M2M
54 53 3ad2ant2 A2M2¬2MM
55 simp3 A2M2¬2M¬2M
56 52 54 55 oddpwp1fsum A2M2¬2MAM+1=A+1k=0M11kAk
57 56 eqcomd A2M2¬2MA+1k=0M11kAk=AM+1
58 eluzge2nn0 M2M0
59 58 adantl A2M2M0
60 10 59 nn0expcld A2M2AM0
61 60 nn0cnd A2M2AM
62 peano2cn AMAM+1
63 61 62 syl A2M2AM+1
64 63 3adant3 A2M2¬2MAM+1
65 17 zcnd A2M2¬2Mk=0M11kAk
66 eluz2nn A2A
67 66 peano2nnd A2A+1
68 67 nncnd A2A+1
69 67 nnne0d A2A+10
70 68 69 jca A2A+1A+10
71 70 3ad2ant1 A2M2¬2MA+1A+10
72 divmul AM+1k=0M11kAkA+1A+10AM+1A+1=k=0M11kAkA+1k=0M11kAk=AM+1
73 64 65 71 72 syl3anc A2M2¬2MAM+1A+1=k=0M11kAkA+1k=0M11kAk=AM+1
74 57 73 mpbird A2M2¬2MAM+1A+1=k=0M11kAk
75 74 eqcomd A2M2¬2Mk=0M11kAk=AM+1A+1
76 lighneallem4a A2M3k=0M11kAk=AM+1A+12k=0M11kAk
77 18 50 75 76 syl3anc A2M2¬2M2k=0M11kAk
78 eluz2 k=0M11kAk22k=0M11kAk2k=0M11kAk
79 2 17 77 78 syl3anbrc A2M2¬2Mk=0M11kAk2