Metamath Proof Explorer

Theorem lighneallem4b

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

Ref Expression
Assertion lighneallem4b ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ( ℤ≥ ‘ 2 ) )

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 2 ∈ ℤ )
3 fzfid ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ( 0 ... ( 𝑀 − 1 ) ) ∈ Fin )
4 neg1z ⊢ - 1 ∈ ℤ
5 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) → 𝑘 ∈ ℕ0 )
6 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( - 1 ↑ 𝑘 ) ∈ ℤ )
7 4 5 6 sylancr ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) → ( - 1 ↑ 𝑘 ) ∈ ℤ )
8 7 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ) → ( - 1 ↑ 𝑘 ) ∈ ℤ )
9 eluzge2nn0 ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ0 )
10 9 adantr ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℕ0 )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ) → 𝐴 ∈ ℕ0 )
12 5 adantl ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ) → 𝑘 ∈ ℕ0 )
13 11 12 nn0expcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℕ0 )
14 13 nn0zd ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ) → ( 𝐴 ↑ 𝑘 ) ∈ ℤ )
15 8 14 zmulcld ⊢ ( ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ) → ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℤ )
16 3 15 fsumzcl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℤ )
17 16 3adant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℤ )
18 simp1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 𝐴 ∈ ( ℤ≥ ‘ 2 ) )
19 3z ⊢ 3 ∈ ℤ
20 19 a1i ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 3 ∈ ℤ )
21 eluzelz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℤ )
22 21 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 𝑀 ∈ ℤ )
23 eluz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ≤ 𝑀 ) )
24 2re ⊢ 2 ∈ ℝ
25 24 a1i ⊢ ( 𝑀 ∈ ℤ → 2 ∈ ℝ )
26 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
27 25 26 leloed ⊢ ( 𝑀 ∈ ℤ → ( 2 ≤ 𝑀 ↔ ( 2 < 𝑀 ∨ 2 = 𝑀 ) ) )
28 zltp1le ⊢ ( ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 2 < 𝑀 ↔ ( 2 + 1 ) ≤ 𝑀 ) )
29 1 28 mpan ⊢ ( 𝑀 ∈ ℤ → ( 2 < 𝑀 ↔ ( 2 + 1 ) ≤ 𝑀 ) )
30 29 biimpd ⊢ ( 𝑀 ∈ ℤ → ( 2 < 𝑀 → ( 2 + 1 ) ≤ 𝑀 ) )
31 df-3 ⊢ 3 = ( 2 + 1 )
32 31 breq1i ⊢ ( 3 ≤ 𝑀 ↔ ( 2 + 1 ) ≤ 𝑀 )
33 30 32 imbitrrdi ⊢ ( 𝑀 ∈ ℤ → ( 2 < 𝑀 → 3 ≤ 𝑀 ) )
34 33 a1i ⊢ ( ¬ 2 ∥ 𝑀 → ( 𝑀 ∈ ℤ → ( 2 < 𝑀 → 3 ≤ 𝑀 ) ) )
35 34 com13 ⊢ ( 2 < 𝑀 → ( 𝑀 ∈ ℤ → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) ) )
36 z2even ⊢ 2 ∥ 2
37 breq2 ⊢ ( 2 = 𝑀 → ( 2 ∥ 2 ↔ 2 ∥ 𝑀 ) )
38 36 37 mpbii ⊢ ( 2 = 𝑀 → 2 ∥ 𝑀 )
39 38 pm2.24d ⊢ ( 2 = 𝑀 → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) )
40 39 a1d ⊢ ( 2 = 𝑀 → ( 𝑀 ∈ ℤ → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) ) )
41 35 40 jaoi ⊢ ( ( 2 < 𝑀 ∨ 2 = 𝑀 ) → ( 𝑀 ∈ ℤ → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) ) )
42 41 com12 ⊢ ( 𝑀 ∈ ℤ → ( ( 2 < 𝑀 ∨ 2 = 𝑀 ) → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) ) )
43 27 42 sylbid ⊢ ( 𝑀 ∈ ℤ → ( 2 ≤ 𝑀 → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) ) )
44 43 imp ⊢ ( ( 𝑀 ∈ ℤ ∧ 2 ≤ 𝑀 ) → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) )
45 44 3adant1 ⊢ ( ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 2 ≤ 𝑀 ) → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) )
46 23 45 sylbi ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → ( ¬ 2 ∥ 𝑀 → 3 ≤ 𝑀 ) )
47 46 imp ⊢ ( ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 3 ≤ 𝑀 )
48 47 3adant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 3 ≤ 𝑀 )
49 eluz2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 3 ≤ 𝑀 ) )
50 20 22 48 49 syl3anbrc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 𝑀 ∈ ( ℤ≥ ‘ 3 ) )
51 eluzelcn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℂ )
52 51 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 𝐴 ∈ ℂ )
53 eluz2nn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ )
54 53 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 𝑀 ∈ ℕ )
55 simp3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → ¬ 2 ∥ 𝑀 )
56 52 54 55 oddpwp1fsum ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → ( ( 𝐴 ↑ 𝑀 ) + 1 ) = ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
57 56 eqcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) + 1 ) )
58 eluzge2nn0 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 2 ) → 𝑀 ∈ ℕ0 )
59 58 adantl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → 𝑀 ∈ ℕ0 )
60 10 59 nn0expcld ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℕ0 )
61 60 nn0cnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝐴 ↑ 𝑀 ) ∈ ℂ )
62 peano2cn ⊢ ( ( 𝐴 ↑ 𝑀 ) ∈ ℂ → ( ( 𝐴 ↑ 𝑀 ) + 1 ) ∈ ℂ )
63 61 62 syl ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝐴 ↑ 𝑀 ) + 1 ) ∈ ℂ )
64 63 3adant3 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → ( ( 𝐴 ↑ 𝑀 ) + 1 ) ∈ ℂ )
65 17 zcnd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ )
66 eluz2nn ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
67 66 peano2nnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + 1 ) ∈ ℕ )
68 67 nncnd ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + 1 ) ∈ ℂ )
69 67 nnne0d ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 + 1 ) ≠ 0 )
70 68 69 jca ⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝐴 + 1 ) ∈ ℂ ∧ ( 𝐴 + 1 ) ≠ 0 ) )
71 70 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → ( ( 𝐴 + 1 ) ∈ ℂ ∧ ( 𝐴 + 1 ) ≠ 0 ) )
72 divmul ⊢ ( ( ( ( 𝐴 ↑ 𝑀 ) + 1 ) ∈ ℂ ∧ Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℂ ∧ ( ( 𝐴 + 1 ) ∈ ℂ ∧ ( 𝐴 + 1 ) ≠ 0 ) ) → ( ( ( ( 𝐴 ↑ 𝑀 ) + 1 ) / ( 𝐴 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ↔ ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) + 1 ) ) )
73 64 65 71 72 syl3anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → ( ( ( ( 𝐴 ↑ 𝑀 ) + 1 ) / ( 𝐴 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ↔ ( ( 𝐴 + 1 ) · Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) = ( ( 𝐴 ↑ 𝑀 ) + 1 ) ) )
74 57 73 mpbird ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → ( ( ( 𝐴 ↑ 𝑀 ) + 1 ) / ( 𝐴 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
75 74 eqcomd ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( ( 𝐴 ↑ 𝑀 ) + 1 ) / ( 𝐴 + 1 ) ) )
76 lighneallem4a ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 3 ) ∧ Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) = ( ( ( 𝐴 ↑ 𝑀 ) + 1 ) / ( 𝐴 + 1 ) ) ) → 2 ≤ Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
77 18 50 75 76 syl3anc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → 2 ≤ Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
78 eluz2 ⊢ ( Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℤ ∧ 2 ≤ Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ) )
79 2 17 77 78 syl3anbrc ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ( ℤ≥ ‘ 2 ) ∧ ¬ 2 ∥ 𝑀 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑀 − 1 ) ) ( ( - 1 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ( ℤ≥ ‘ 2 ) )