Metamath Proof Explorer

Theorem lighneallem4b

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

Ref Expression
Assertion lighneallem4b 
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. ( ZZ>= ` 2 ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 1 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> 2 e. ZZ )
3 fzfid 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) -> ( 0 ... ( M - 1 ) ) e. Fin )
4 neg1z 
 |-  -u 1 e. ZZ
5 elfznn0 
 |-  ( k e. ( 0 ... ( M - 1 ) ) -> k e. NN0 )
6 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ k e. NN0 ) -> ( -u 1 ^ k ) e. ZZ )
7 4 5 6 sylancr 
 |-  ( k e. ( 0 ... ( M - 1 ) ) -> ( -u 1 ^ k ) e. ZZ )
8 7 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( -u 1 ^ k ) e. ZZ )
9 eluzge2nn0 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN0 )
10 9 adantr 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) -> A e. NN0 )
11 10 adantr 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> A e. NN0 )
12 5 adantl 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> k e. NN0 )
13 11 12 nn0expcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( A ^ k ) e. NN0 )
14 13 nn0zd 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( A ^ k ) e. ZZ )
15 8 14 zmulcld 
 |-  ( ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. ZZ )
16 3 15 fsumzcl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. ZZ )
17 16 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. ZZ )
18 simp1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> A e. ( ZZ>= ` 2 ) )
19 3z 
 |-  3 e. ZZ
20 19 a1i 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> 3 e. ZZ )
21 eluzelz 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. ZZ )
22 21 3ad2ant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> M e. ZZ )
23 eluz2 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ M e. ZZ /\ 2 <_ M ) )
24 2re 
 |-  2 e. RR
25 24 a1i 
 |-  ( M e. ZZ -> 2 e. RR )
26 zre 
 |-  ( M e. ZZ -> M e. RR )
27 25 26 leloed 
 |-  ( M e. ZZ -> ( 2 <_ M <-> ( 2 < M \/ 2 = M ) ) )
28 zltp1le 
 |-  ( ( 2 e. ZZ /\ M e. ZZ ) -> ( 2 < M <-> ( 2 + 1 ) <_ M ) )
29 1 28 mpan 
 |-  ( M e. ZZ -> ( 2 < M <-> ( 2 + 1 ) <_ M ) )
30 29 biimpd 
 |-  ( M e. ZZ -> ( 2 < M -> ( 2 + 1 ) <_ M ) )
31 df-3 
 |-  3 = ( 2 + 1 )
32 31 breq1i 
 |-  ( 3 <_ M <-> ( 2 + 1 ) <_ M )
33 30 32 syl6ibr 
 |-  ( M e. ZZ -> ( 2 < M -> 3 <_ M ) )
34 33 a1i 
 |-  ( -. 2 || M -> ( M e. ZZ -> ( 2 < M -> 3 <_ M ) ) )
35 34 com13 
 |-  ( 2 < M -> ( M e. ZZ -> ( -. 2 || M -> 3 <_ M ) ) )
36 z2even 
 |-  2 || 2
37 breq2 
 |-  ( 2 = M -> ( 2 || 2 <-> 2 || M ) )
38 36 37 mpbii 
 |-  ( 2 = M -> 2 || M )
39 38 pm2.24d 
 |-  ( 2 = M -> ( -. 2 || M -> 3 <_ M ) )
40 39 a1d 
 |-  ( 2 = M -> ( M e. ZZ -> ( -. 2 || M -> 3 <_ M ) ) )
41 35 40 jaoi 
 |-  ( ( 2 < M \/ 2 = M ) -> ( M e. ZZ -> ( -. 2 || M -> 3 <_ M ) ) )
42 41 com12 
 |-  ( M e. ZZ -> ( ( 2 < M \/ 2 = M ) -> ( -. 2 || M -> 3 <_ M ) ) )
43 27 42 sylbid 
 |-  ( M e. ZZ -> ( 2 <_ M -> ( -. 2 || M -> 3 <_ M ) ) )
44 43 imp 
 |-  ( ( M e. ZZ /\ 2 <_ M ) -> ( -. 2 || M -> 3 <_ M ) )
45 44 3adant1 
 |-  ( ( 2 e. ZZ /\ M e. ZZ /\ 2 <_ M ) -> ( -. 2 || M -> 3 <_ M ) )
46 23 45 sylbi 
 |-  ( M e. ( ZZ>= ` 2 ) -> ( -. 2 || M -> 3 <_ M ) )
47 46 imp 
 |-  ( ( M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> 3 <_ M )
48 47 3adant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> 3 <_ M )
49 eluz2 
 |-  ( M e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ M e. ZZ /\ 3 <_ M ) )
50 20 22 48 49 syl3anbrc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> M e. ( ZZ>= ` 3 ) )
51 eluzelcn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. CC )
52 51 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> A e. CC )
53 eluz2nn 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. NN )
54 53 3ad2ant2 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> M e. NN )
55 simp3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> -. 2 || M )
56 52 54 55 oddpwp1fsum 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> ( ( A ^ M ) + 1 ) = ( ( A + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) )
57 56 eqcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> ( ( A + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) = ( ( A ^ M ) + 1 ) )
58 eluzge2nn0 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. NN0 )
59 58 adantl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) -> M e. NN0 )
60 10 59 nn0expcld 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) -> ( A ^ M ) e. NN0 )
61 60 nn0cnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) -> ( A ^ M ) e. CC )
62 peano2cn 
 |-  ( ( A ^ M ) e. CC -> ( ( A ^ M ) + 1 ) e. CC )
63 61 62 syl 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) ) -> ( ( A ^ M ) + 1 ) e. CC )
64 63 3adant3 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> ( ( A ^ M ) + 1 ) e. CC )
65 17 zcnd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. CC )
66 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
67 66 peano2nnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + 1 ) e. NN )
68 67 nncnd 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + 1 ) e. CC )
69 67 nnne0d 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A + 1 ) =/= 0 )
70 68 69 jca 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( ( A + 1 ) e. CC /\ ( A + 1 ) =/= 0 ) )
71 70 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> ( ( A + 1 ) e. CC /\ ( A + 1 ) =/= 0 ) )
72 divmul 
 |-  ( ( ( ( A ^ M ) + 1 ) e. CC /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. CC /\ ( ( A + 1 ) e. CC /\ ( A + 1 ) =/= 0 ) ) -> ( ( ( ( A ^ M ) + 1 ) / ( A + 1 ) ) = sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) <-> ( ( A + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) = ( ( A ^ M ) + 1 ) ) )
73 64 65 71 72 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> ( ( ( ( A ^ M ) + 1 ) / ( A + 1 ) ) = sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) <-> ( ( A + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) = ( ( A ^ M ) + 1 ) ) )
74 57 73 mpbird 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> ( ( ( A ^ M ) + 1 ) / ( A + 1 ) ) = sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) )
75 74 eqcomd 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) = ( ( ( A ^ M ) + 1 ) / ( A + 1 ) ) )
76 lighneallem4a 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 3 ) /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) = ( ( ( A ^ M ) + 1 ) / ( A + 1 ) ) ) -> 2 <_ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) )
77 18 50 75 76 syl3anc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> 2 <_ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) )
78 eluz2 
 |-  ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. ZZ /\ 2 <_ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) ) )
79 2 17 77 78 syl3anbrc 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( A ^ k ) ) e. ( ZZ>= ` 2 ) )