Metamath Proof Explorer


Theorem lighneallem3

Description: Lemma 3 for lighneal . (Contributed by AV, 11-Aug-2021)

Ref Expression
Assertion lighneallem3 P 2 M N ¬ 2 N 2 M 2 N 1 = P M M = 1

Proof

Step Hyp Ref Expression
1 oveq2 N = 1 2 N = 2 1
2 2cn 2
3 exp1 2 2 1 = 2
4 2 3 ax-mp 2 1 = 2
5 1 4 eqtrdi N = 1 2 N = 2
6 5 oveq1d N = 1 2 N 1 = 2 1
7 2m1e1 2 1 = 1
8 6 7 eqtrdi N = 1 2 N 1 = 1
9 8 adantl P 2 M N = 1 2 N 1 = 1
10 9 eqeq1d P 2 M N = 1 2 N 1 = P M 1 = P M
11 eldifi P 2 P
12 prmnn P P
13 nnnn0 P P 0
14 11 12 13 3syl P 2 P 0
15 14 nn0zd P 2 P
16 iddvdsexp P M P P M
17 15 16 sylan P 2 M P P M
18 breq2 1 = P M P 1 P P M
19 18 adantl P 2 M 1 = P M P 1 P P M
20 dvds1 P 0 P 1 P = 1
21 14 20 syl P 2 P 1 P = 1
22 eleq1 P = 1 P 1
23 1nprm ¬ 1
24 23 pm2.21i 1 M = 1
25 22 24 syl6bi P = 1 P M = 1
26 11 25 syl5com P 2 P = 1 M = 1
27 21 26 sylbid P 2 P 1 M = 1
28 27 ad2antrr P 2 M 1 = P M P 1 M = 1
29 19 28 sylbird P 2 M 1 = P M P P M M = 1
30 29 ex P 2 M 1 = P M P P M M = 1
31 17 30 mpid P 2 M 1 = P M M = 1
32 31 adantr P 2 M N = 1 1 = P M M = 1
33 10 32 sylbid P 2 M N = 1 2 N 1 = P M M = 1
34 33 ex P 2 M N = 1 2 N 1 = P M M = 1
35 34 com23 P 2 M 2 N 1 = P M N = 1 M = 1
36 35 a1d P 2 M ¬ 2 N 2 M 2 N 1 = P M N = 1 M = 1
37 36 3adant3 P 2 M N ¬ 2 N 2 M 2 N 1 = P M N = 1 M = 1
38 37 3imp P 2 M N ¬ 2 N 2 M 2 N 1 = P M N = 1 M = 1
39 neqne ¬ N = 1 N 1
40 39 anim2i N ¬ N = 1 N N 1
41 eluz2b3 N 2 N N 1
42 40 41 sylibr N ¬ N = 1 N 2
43 oddge22np1 N 2 ¬ 2 N j 2 j + 1 = N
44 42 43 syl N ¬ N = 1 ¬ 2 N j 2 j + 1 = N
45 44 3ad2antl3 P 2 M N ¬ N = 1 ¬ 2 N j 2 j + 1 = N
46 oveq2 N = 2 j + 1 2 N = 2 2 j + 1
47 46 oveq1d N = 2 j + 1 2 N 1 = 2 2 j + 1 1
48 47 eqcoms 2 j + 1 = N 2 N 1 = 2 2 j + 1 1
49 2 a1i j 2
50 2nn0 2 0
51 50 a1i j 2 0
52 nnnn0 j j 0
53 51 52 nn0mulcld j 2 j 0
54 49 53 expp1d j 2 2 j + 1 = 2 2 j 2
55 51 53 nn0expcld j 2 2 j 0
56 55 nn0cnd j 2 2 j
57 56 49 mulcomd j 2 2 j 2 = 2 2 2 j
58 54 57 eqtrd j 2 2 j + 1 = 2 2 2 j
59 58 oveq1d j 2 2 j + 1 1 = 2 2 2 j 1
60 npcan1 2 2 j 2 2 j - 1 + 1 = 2 2 j
61 56 60 syl j 2 2 j - 1 + 1 = 2 2 j
62 61 eqcomd j 2 2 j = 2 2 j - 1 + 1
63 62 oveq2d j 2 2 2 j = 2 2 2 j - 1 + 1
64 peano2cnm 2 2 j 2 2 j 1
65 56 64 syl j 2 2 j 1
66 1cnd j 1
67 49 65 66 adddid j 2 2 2 j - 1 + 1 = 2 2 2 j 1 + 2 1
68 63 67 eqtrd j 2 2 2 j = 2 2 2 j 1 + 2 1
69 68 oveq1d j 2 2 2 j 1 = 2 2 2 j 1 + 2 1 - 1
70 49 65 mulcld j 2 2 2 j 1
71 ax-1cn 1
72 2 71 mulcli 2 1
73 72 a1i j 2 1
74 70 73 66 addsubassd j 2 2 2 j 1 + 2 1 - 1 = 2 2 2 j 1 + 2 1 - 1
75 2t1e2 2 1 = 2
76 75 oveq1i 2 1 1 = 2 1
77 76 7 eqtri 2 1 1 = 1
78 77 a1i j 2 1 1 = 1
79 78 oveq2d j 2 2 2 j 1 + 2 1 - 1 = 2 2 2 j 1 + 1
80 74 79 eqtrd j 2 2 2 j 1 + 2 1 - 1 = 2 2 2 j 1 + 1
81 59 69 80 3eqtrd j 2 2 j + 1 1 = 2 2 2 j 1 + 1
82 81 ad2antlr P 2 M N j 2 M 2 2 j + 1 1 = 2 2 2 j 1 + 1
83 48 82 sylan9eqr P 2 M N j 2 M 2 j + 1 = N 2 N 1 = 2 2 2 j 1 + 1
84 83 eqeq1d P 2 M N j 2 M 2 j + 1 = N 2 N 1 = P M 2 2 2 j 1 + 1 = P M
85 14 3ad2ant1 P 2 M N P 0
86 nnnn0 M M 0
87 86 3ad2ant2 P 2 M N M 0
88 85 87 nn0expcld P 2 M N P M 0
89 88 nn0cnd P 2 M N P M
90 89 adantr P 2 M N j P M
91 1cnd P 2 M N j 1
92 70 adantl P 2 M N j 2 2 2 j 1
93 90 91 92 3jca P 2 M N j P M 1 2 2 2 j 1
94 93 adantr P 2 M N j 2 M P M 1 2 2 2 j 1
95 subadd2 P M 1 2 2 2 j 1 P M 1 = 2 2 2 j 1 2 2 2 j 1 + 1 = P M
96 94 95 syl P 2 M N j 2 M P M 1 = 2 2 2 j 1 2 2 2 j 1 + 1 = P M
97 nncn P P
98 11 12 97 3syl P 2 P
99 98 3ad2ant1 P 2 M N P
100 99 87 pwm1geoser P 2 M N P M 1 = P 1 k = 0 M 1 P k
101 100 adantr P 2 M N j P M 1 = P 1 k = 0 M 1 P k
102 101 eqeq1d P 2 M N j P M 1 = 2 2 2 j 1 P 1 k = 0 M 1 P k = 2 2 2 j 1
103 102 adantr P 2 M N j 2 M P M 1 = 2 2 2 j 1 P 1 k = 0 M 1 P k = 2 2 2 j 1
104 99 ad2antrr P 2 M N j 2 M P
105 1cnd P 2 M N j 2 M 1
106 104 105 subcld P 2 M N j 2 M P 1
107 fzfid P 2 M N 0 M 1 Fin
108 85 adantr P 2 M N k 0 M 1 P 0
109 elfznn0 k 0 M 1 k 0
110 109 adantl P 2 M N k 0 M 1 k 0
111 108 110 nn0expcld P 2 M N k 0 M 1 P k 0
112 111 nn0zd P 2 M N k 0 M 1 P k
113 107 112 fsumzcl P 2 M N k = 0 M 1 P k
114 113 zcnd P 2 M N k = 0 M 1 P k
115 114 ad2antrr P 2 M N j 2 M k = 0 M 1 P k
116 106 115 mulcld P 2 M N j 2 M P 1 k = 0 M 1 P k
117 56 ad2antlr P 2 M N j 2 M 2 2 j
118 117 105 subcld P 2 M N j 2 M 2 2 j 1
119 2rp 2 +
120 119 a1i P 2 M N j 2 M 2 +
121 120 rpcnne0d P 2 M N j 2 M 2 2 0
122 divmul2 P 1 k = 0 M 1 P k 2 2 j 1 2 2 0 P 1 k = 0 M 1 P k 2 = 2 2 j 1 P 1 k = 0 M 1 P k = 2 2 2 j 1
123 116 118 121 122 syl3anc P 2 M N j 2 M P 1 k = 0 M 1 P k 2 = 2 2 j 1 P 1 k = 0 M 1 P k = 2 2 2 j 1
124 div23 P 1 k = 0 M 1 P k 2 2 0 P 1 k = 0 M 1 P k 2 = P 1 2 k = 0 M 1 P k
125 106 115 121 124 syl3anc P 2 M N j 2 M P 1 k = 0 M 1 P k 2 = P 1 2 k = 0 M 1 P k
126 125 eqeq1d P 2 M N j 2 M P 1 k = 0 M 1 P k 2 = 2 2 j 1 P 1 2 k = 0 M 1 P k = 2 2 j 1
127 51 nn0zd j 2
128 2nn 2
129 128 a1i j 2
130 id j j
131 129 130 nnmulcld j 2 j
132 iddvdsexp 2 2 j 2 2 2 j
133 127 131 132 syl2anc j 2 2 2 j
134 133 notnotd j ¬ ¬ 2 2 2 j
135 55 nn0zd j 2 2 j
136 oddm1even 2 2 j ¬ 2 2 2 j 2 2 2 j 1
137 135 136 syl j ¬ 2 2 2 j 2 2 2 j 1
138 134 137 mtbid j ¬ 2 2 2 j 1
139 138 ad2antlr P 2 M N j 2 M ¬ 2 2 2 j 1
140 breq2 P 1 2 k = 0 M 1 P k = 2 2 j 1 2 P 1 2 k = 0 M 1 P k 2 2 2 j 1
141 140 notbid P 1 2 k = 0 M 1 P k = 2 2 j 1 ¬ 2 P 1 2 k = 0 M 1 P k ¬ 2 2 2 j 1
142 141 adantl P 2 M N j 2 M P 1 2 k = 0 M 1 P k = 2 2 j 1 ¬ 2 P 1 2 k = 0 M 1 P k ¬ 2 2 2 j 1
143 fzfid P 2 M N j 2 M 0 M 1 Fin
144 112 ad4ant14 P 2 M N j 2 M k 0 M 1 P k
145 elnn0 k 0 k k = 0
146 eldifsn P 2 P P 2
147 simpr P P 2 P 2
148 147 necomd P P 2 2 P
149 146 148 sylbi P 2 2 P
150 149 adantl k P 2 2 P
151 150 neneqd k P 2 ¬ 2 = P
152 2prm 2
153 11 adantl k P 2 P
154 simpl k P 2 k
155 prmdvdsexpb 2 P k 2 P k 2 = P
156 152 153 154 155 mp3an2i k P 2 2 P k 2 = P
157 151 156 mtbird k P 2 ¬ 2 P k
158 157 ex k P 2 ¬ 2 P k
159 n2dvds1 ¬ 2 1
160 oveq2 k = 0 P k = P 0
161 98 exp0d P 2 P 0 = 1
162 160 161 sylan9eq k = 0 P 2 P k = 1
163 162 breq2d k = 0 P 2 2 P k 2 1
164 159 163 mtbiri k = 0 P 2 ¬ 2 P k
165 164 ex k = 0 P 2 ¬ 2 P k
166 158 165 jaoi k k = 0 P 2 ¬ 2 P k
167 145 166 sylbi k 0 P 2 ¬ 2 P k
168 167 109 syl11 P 2 k 0 M 1 ¬ 2 P k
169 168 3ad2ant1 P 2 M N k 0 M 1 ¬ 2 P k
170 169 ad2antrr P 2 M N j 2 M k 0 M 1 ¬ 2 P k
171 170 imp P 2 M N j 2 M k 0 M 1 ¬ 2 P k
172 nnm1nn0 M M 1 0
173 hashfz0 M 1 0 0 M 1 = M - 1 + 1
174 172 173 syl M 0 M 1 = M - 1 + 1
175 nncn M M
176 1cnd M 1
177 175 176 npcand M M - 1 + 1 = M
178 174 177 eqtr2d M M = 0 M 1
179 178 3ad2ant2 P 2 M N M = 0 M 1
180 179 adantr P 2 M N j M = 0 M 1
181 180 breq2d P 2 M N j 2 M 2 0 M 1
182 181 biimpa P 2 M N j 2 M 2 0 M 1
183 143 144 171 182 evensumodd P 2 M N j 2 M 2 k = 0 M 1 P k
184 183 olcd P 2 M N j 2 M 2 P 1 2 2 k = 0 M 1 P k
185 152 a1i P 2 M 2
186 oddn2prm P 2 ¬ 2 P
187 oddm1d2 P ¬ 2 P P 1 2
188 15 187 syl P 2 ¬ 2 P P 1 2
189 186 188 mpbid P 2 P 1 2
190 189 adantr P 2 M P 1 2
191 fzfid P 2 M 0 M 1 Fin
192 14 ad2antrr P 2 M k 0 M 1 P 0
193 109 adantl P 2 M k 0 M 1 k 0
194 192 193 nn0expcld P 2 M k 0 M 1 P k 0
195 194 nn0zd P 2 M k 0 M 1 P k
196 191 195 fsumzcl P 2 M k = 0 M 1 P k
197 185 190 196 3jca P 2 M 2 P 1 2 k = 0 M 1 P k
198 197 3adant3 P 2 M N 2 P 1 2 k = 0 M 1 P k
199 euclemma 2 P 1 2 k = 0 M 1 P k 2 P 1 2 k = 0 M 1 P k 2 P 1 2 2 k = 0 M 1 P k
200 198 199 syl P 2 M N 2 P 1 2 k = 0 M 1 P k 2 P 1 2 2 k = 0 M 1 P k
201 200 ad2antrr P 2 M N j 2 M 2 P 1 2 k = 0 M 1 P k 2 P 1 2 2 k = 0 M 1 P k
202 184 201 mpbird P 2 M N j 2 M 2 P 1 2 k = 0 M 1 P k
203 202 pm2.24d P 2 M N j 2 M ¬ 2 P 1 2 k = 0 M 1 P k M = 1
204 203 adantr P 2 M N j 2 M P 1 2 k = 0 M 1 P k = 2 2 j 1 ¬ 2 P 1 2 k = 0 M 1 P k M = 1
205 142 204 sylbird P 2 M N j 2 M P 1 2 k = 0 M 1 P k = 2 2 j 1 ¬ 2 2 2 j 1 M = 1
206 205 ex P 2 M N j 2 M P 1 2 k = 0 M 1 P k = 2 2 j 1 ¬ 2 2 2 j 1 M = 1
207 139 206 mpid P 2 M N j 2 M P 1 2 k = 0 M 1 P k = 2 2 j 1 M = 1
208 126 207 sylbid P 2 M N j 2 M P 1 k = 0 M 1 P k 2 = 2 2 j 1 M = 1
209 123 208 sylbird P 2 M N j 2 M P 1 k = 0 M 1 P k = 2 2 2 j 1 M = 1
210 103 209 sylbid P 2 M N j 2 M P M 1 = 2 2 2 j 1 M = 1
211 96 210 sylbird P 2 M N j 2 M 2 2 2 j 1 + 1 = P M M = 1
212 211 adantr P 2 M N j 2 M 2 j + 1 = N 2 2 2 j 1 + 1 = P M M = 1
213 84 212 sylbid P 2 M N j 2 M 2 j + 1 = N 2 N 1 = P M M = 1
214 213 exp31 P 2 M N j 2 M 2 j + 1 = N 2 N 1 = P M M = 1
215 214 com23 P 2 M N j 2 j + 1 = N 2 M 2 N 1 = P M M = 1
216 215 rexlimdva P 2 M N j 2 j + 1 = N 2 M 2 N 1 = P M M = 1
217 216 com34 P 2 M N j 2 j + 1 = N 2 N 1 = P M 2 M M = 1
218 217 adantr P 2 M N ¬ N = 1 j 2 j + 1 = N 2 N 1 = P M 2 M M = 1
219 45 218 sylbid P 2 M N ¬ N = 1 ¬ 2 N 2 N 1 = P M 2 M M = 1
220 219 com24 P 2 M N ¬ N = 1 2 M 2 N 1 = P M ¬ 2 N M = 1
221 220 ex P 2 M N ¬ N = 1 2 M 2 N 1 = P M ¬ 2 N M = 1
222 221 com25 P 2 M N ¬ 2 N 2 M 2 N 1 = P M ¬ N = 1 M = 1
223 222 impd P 2 M N ¬ 2 N 2 M 2 N 1 = P M ¬ N = 1 M = 1
224 223 3imp P 2 M N ¬ 2 N 2 M 2 N 1 = P M ¬ N = 1 M = 1
225 38 224 pm2.61d P 2 M N ¬ 2 N 2 M 2 N 1 = P M M = 1