Metamath Proof Explorer

Theorem lighneallem4

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

Ref Expression
Assertion lighneallem4 
|- ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. 2 || N /\ -. 2 || M ) /\ ( ( 2 ^ N ) - 1 ) = ( P ^ M ) ) -> M = 1 )

Proof

Step Hyp Ref Expression
1 2cnd 
 |-  ( N e. NN -> 2 e. CC )
2 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
3 1 2 expcld 
 |-  ( N e. NN -> ( 2 ^ N ) e. CC )
4 3 3ad2ant3 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( 2 ^ N ) e. CC )
5 1cnd 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> 1 e. CC )
6 eldifi 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. Prime )
7 prmnn 
 |-  ( P e. Prime -> P e. NN )
8 nncn 
 |-  ( P e. NN -> P e. CC )
9 6 7 8 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. CC )
10 9 3ad2ant1 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> P e. CC )
11 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
12 11 3ad2ant2 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> M e. NN0 )
13 10 12 expcld 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( P ^ M ) e. CC )
14 4 5 13 3jca 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( 2 ^ N ) e. CC /\ 1 e. CC /\ ( P ^ M ) e. CC ) )
15 14 adantr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( ( 2 ^ N ) e. CC /\ 1 e. CC /\ ( P ^ M ) e. CC ) )
16 subadd2 
 |-  ( ( ( 2 ^ N ) e. CC /\ 1 e. CC /\ ( P ^ M ) e. CC ) -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) <-> ( ( P ^ M ) + 1 ) = ( 2 ^ N ) ) )
17 15 16 syl 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) <-> ( ( P ^ M ) + 1 ) = ( 2 ^ N ) ) )
18 10 adantr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> P e. CC )
19 simpl2 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> M e. NN )
20 simpr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> -. 2 || M )
21 18 19 20 oddpwp1fsum 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( ( P ^ M ) + 1 ) = ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) )
22 21 eqeq1d 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( ( ( P ^ M ) + 1 ) = ( 2 ^ N ) <-> ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) ) )
23 peano2nn 
 |-  ( P e. NN -> ( P + 1 ) e. NN )
24 23 nnzd 
 |-  ( P e. NN -> ( P + 1 ) e. ZZ )
25 6 7 24 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( P + 1 ) e. ZZ )
26 25 3ad2ant1 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( P + 1 ) e. ZZ )
27 fzfid 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( 0 ... ( M - 1 ) ) e. Fin )
28 neg1z 
 |-  -u 1 e. ZZ
29 28 a1i 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> -u 1 e. ZZ )
30 elfznn0 
 |-  ( k e. ( 0 ... ( M - 1 ) ) -> k e. NN0 )
31 zexpcl 
 |-  ( ( -u 1 e. ZZ /\ k e. NN0 ) -> ( -u 1 ^ k ) e. ZZ )
32 29 30 31 syl2an 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( -u 1 ^ k ) e. ZZ )
33 nnz 
 |-  ( P e. NN -> P e. ZZ )
34 6 7 33 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ZZ )
35 34 3ad2ant1 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> P e. ZZ )
36 zexpcl 
 |-  ( ( P e. ZZ /\ k e. NN0 ) -> ( P ^ k ) e. ZZ )
37 35 30 36 syl2an 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( P ^ k ) e. ZZ )
38 32 37 zmulcld 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ )
39 27 38 fsumzcl 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ )
40 26 39 jca 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( P + 1 ) e. ZZ /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ ) )
41 40 ad2antrr 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) /\ ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) ) -> ( ( P + 1 ) e. ZZ /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ ) )
42 dvdsmul2 
 |-  ( ( ( P + 1 ) e. ZZ /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) )
43 41 42 syl 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) /\ ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) )
44 breq2 
 |-  ( ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) <-> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) ) )
45 44 adantl 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) /\ ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) <-> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) ) )
46 2a1 
 |-  ( M = 1 -> ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> M = 1 ) ) )
47 2prm 
 |-  2 e. Prime
48 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
49 6 48 syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 2 ) )
50 49 3ad2ant1 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> P e. ( ZZ>= ` 2 ) )
51 50 adantr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> P e. ( ZZ>= ` 2 ) )
52 df-ne 
 |-  ( M =/= 1 <-> -. M = 1 )
53 eluz2b3 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ M =/= 1 ) )
54 53 simplbi2 
 |-  ( M e. NN -> ( M =/= 1 -> M e. ( ZZ>= ` 2 ) ) )
55 52 54 biimtrrid 
 |-  ( M e. NN -> ( -. M = 1 -> M e. ( ZZ>= ` 2 ) ) )
56 55 3ad2ant2 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( -. M = 1 -> M e. ( ZZ>= ` 2 ) ) )
57 56 com12 
 |-  ( -. M = 1 -> ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> M e. ( ZZ>= ` 2 ) ) )
58 57 adantr 
 |-  ( ( -. M = 1 /\ -. 2 || M ) -> ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> M e. ( ZZ>= ` 2 ) ) )
59 58 impcom 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> M e. ( ZZ>= ` 2 ) )
60 simprr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> -. 2 || M )
61 lighneallem4b 
 |-  ( ( P e. ( ZZ>= ` 2 ) /\ M e. ( ZZ>= ` 2 ) /\ -. 2 || M ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ( ZZ>= ` 2 ) )
62 51 59 60 61 syl3anc 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ( ZZ>= ` 2 ) )
63 2 3ad2ant3 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> N e. NN0 )
64 63 adantr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> N e. NN0 )
65 dvdsprmpweqnn 
 |-  ( ( 2 e. Prime /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> E. n e. NN sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) ) )
66 47 62 64 65 mp3an2i 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> E. n e. NN sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) ) )
67 2z 
 |-  2 e. ZZ
68 67 a1i 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> 2 e. ZZ )
69 iddvdsexp 
 |-  ( ( 2 e. ZZ /\ n e. NN ) -> 2 || ( 2 ^ n ) )
70 68 69 sylan 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> 2 || ( 2 ^ n ) )
71 breq2 
 |-  ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) -> ( 2 || sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) <-> 2 || ( 2 ^ n ) ) )
72 71 adantl 
 |-  ( ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) ) -> ( 2 || sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) <-> 2 || ( 2 ^ n ) ) )
73 fzfid 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> ( 0 ... ( M - 1 ) ) e. Fin )
74 28 a1i 
 |-  ( P e. NN -> -u 1 e. ZZ )
75 74 31 sylan 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( -u 1 ^ k ) e. ZZ )
76 nnnn0 
 |-  ( P e. NN -> P e. NN0 )
77 76 adantr 
 |-  ( ( P e. NN /\ k e. NN0 ) -> P e. NN0 )
78 simpr 
 |-  ( ( P e. NN /\ k e. NN0 ) -> k e. NN0 )
79 77 78 nn0expcld 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( P ^ k ) e. NN0 )
80 79 nn0zd 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( P ^ k ) e. ZZ )
81 75 80 zmulcld 
 |-  ( ( P e. NN /\ k e. NN0 ) -> ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ )
82 81 ex 
 |-  ( P e. NN -> ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ ) )
83 6 7 82 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ ) )
84 83 3ad2ant1 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ ) )
85 84 ad2antrr 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> ( k e. NN0 -> ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ ) )
86 85 30 impel 
 |-  ( ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> ( ( -u 1 ^ k ) x. ( P ^ k ) ) e. ZZ )
87 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
88 m1expcl2 
 |-  ( k e. ZZ -> ( -u 1 ^ k ) e. { -u 1 , 1 } )
89 87 88 syl 
 |-  ( k e. NN0 -> ( -u 1 ^ k ) e. { -u 1 , 1 } )
90 ovex 
 |-  ( -u 1 ^ k ) e. _V
91 90 elpr 
 |-  ( ( -u 1 ^ k ) e. { -u 1 , 1 } <-> ( ( -u 1 ^ k ) = -u 1 \/ ( -u 1 ^ k ) = 1 ) )
92 n2dvdsm1 
 |-  -. 2 || -u 1
93 breq2 
 |-  ( ( -u 1 ^ k ) = -u 1 -> ( 2 || ( -u 1 ^ k ) <-> 2 || -u 1 ) )
94 92 93 mtbiri 
 |-  ( ( -u 1 ^ k ) = -u 1 -> -. 2 || ( -u 1 ^ k ) )
95 n2dvds1 
 |-  -. 2 || 1
96 breq2 
 |-  ( ( -u 1 ^ k ) = 1 -> ( 2 || ( -u 1 ^ k ) <-> 2 || 1 ) )
97 95 96 mtbiri 
 |-  ( ( -u 1 ^ k ) = 1 -> -. 2 || ( -u 1 ^ k ) )
98 94 97 jaoi 
 |-  ( ( ( -u 1 ^ k ) = -u 1 \/ ( -u 1 ^ k ) = 1 ) -> -. 2 || ( -u 1 ^ k ) )
99 98 a1d 
 |-  ( ( ( -u 1 ^ k ) = -u 1 \/ ( -u 1 ^ k ) = 1 ) -> ( k e. NN0 -> -. 2 || ( -u 1 ^ k ) ) )
100 91 99 sylbi 
 |-  ( ( -u 1 ^ k ) e. { -u 1 , 1 } -> ( k e. NN0 -> -. 2 || ( -u 1 ^ k ) ) )
101 89 100 mpcom 
 |-  ( k e. NN0 -> -. 2 || ( -u 1 ^ k ) )
102 101 adantl 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> -. 2 || ( -u 1 ^ k ) )
103 elnn0 
 |-  ( k e. NN0 <-> ( k e. NN \/ k = 0 ) )
104 oddn2prm 
 |-  ( P e. ( Prime \ { 2 } ) -> -. 2 || P )
105 104 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN ) -> -. 2 || P )
106 simpr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN ) -> k e. NN )
107 prmdvdsexp 
 |-  ( ( 2 e. Prime /\ P e. ZZ /\ k e. NN ) -> ( 2 || ( P ^ k ) <-> 2 || P ) )
108 47 34 106 107 mp3an2ani 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN ) -> ( 2 || ( P ^ k ) <-> 2 || P ) )
109 105 108 mtbird 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN ) -> -. 2 || ( P ^ k ) )
110 109 expcom 
 |-  ( k e. NN -> ( P e. ( Prime \ { 2 } ) -> -. 2 || ( P ^ k ) ) )
111 oveq2 
 |-  ( k = 0 -> ( P ^ k ) = ( P ^ 0 ) )
112 111 adantr 
 |-  ( ( k = 0 /\ P e. ( Prime \ { 2 } ) ) -> ( P ^ k ) = ( P ^ 0 ) )
113 9 adantl 
 |-  ( ( k = 0 /\ P e. ( Prime \ { 2 } ) ) -> P e. CC )
114 113 exp0d 
 |-  ( ( k = 0 /\ P e. ( Prime \ { 2 } ) ) -> ( P ^ 0 ) = 1 )
115 112 114 eqtrd 
 |-  ( ( k = 0 /\ P e. ( Prime \ { 2 } ) ) -> ( P ^ k ) = 1 )
116 115 breq2d 
 |-  ( ( k = 0 /\ P e. ( Prime \ { 2 } ) ) -> ( 2 || ( P ^ k ) <-> 2 || 1 ) )
117 95 116 mtbiri 
 |-  ( ( k = 0 /\ P e. ( Prime \ { 2 } ) ) -> -. 2 || ( P ^ k ) )
118 117 ex 
 |-  ( k = 0 -> ( P e. ( Prime \ { 2 } ) -> -. 2 || ( P ^ k ) ) )
119 110 118 jaoi 
 |-  ( ( k e. NN \/ k = 0 ) -> ( P e. ( Prime \ { 2 } ) -> -. 2 || ( P ^ k ) ) )
120 103 119 sylbi 
 |-  ( k e. NN0 -> ( P e. ( Prime \ { 2 } ) -> -. 2 || ( P ^ k ) ) )
121 120 impcom 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> -. 2 || ( P ^ k ) )
122 ioran 
 |-  ( -. ( 2 || ( -u 1 ^ k ) \/ 2 || ( P ^ k ) ) <-> ( -. 2 || ( -u 1 ^ k ) /\ -. 2 || ( P ^ k ) ) )
123 102 121 122 sylanbrc 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> -. ( 2 || ( -u 1 ^ k ) \/ 2 || ( P ^ k ) ) )
124 28 31 mpan 
 |-  ( k e. NN0 -> ( -u 1 ^ k ) e. ZZ )
125 124 adantl 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> ( -u 1 ^ k ) e. ZZ )
126 6 7 76 3syl 
 |-  ( P e. ( Prime \ { 2 } ) -> P e. NN0 )
127 126 adantr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> P e. NN0 )
128 simpr 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> k e. NN0 )
129 127 128 nn0expcld 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> ( P ^ k ) e. NN0 )
130 129 nn0zd 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> ( P ^ k ) e. ZZ )
131 euclemma 
 |-  ( ( 2 e. Prime /\ ( -u 1 ^ k ) e. ZZ /\ ( P ^ k ) e. ZZ ) -> ( 2 || ( ( -u 1 ^ k ) x. ( P ^ k ) ) <-> ( 2 || ( -u 1 ^ k ) \/ 2 || ( P ^ k ) ) ) )
132 47 125 130 131 mp3an2i 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> ( 2 || ( ( -u 1 ^ k ) x. ( P ^ k ) ) <-> ( 2 || ( -u 1 ^ k ) \/ 2 || ( P ^ k ) ) ) )
133 123 132 mtbird 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ k e. NN0 ) -> -. 2 || ( ( -u 1 ^ k ) x. ( P ^ k ) ) )
134 133 ex 
 |-  ( P e. ( Prime \ { 2 } ) -> ( k e. NN0 -> -. 2 || ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) )
135 134 3ad2ant1 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( k e. NN0 -> -. 2 || ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) )
136 135 ad2antrr 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> ( k e. NN0 -> -. 2 || ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) )
137 136 30 impel 
 |-  ( ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) /\ k e. ( 0 ... ( M - 1 ) ) ) -> -. 2 || ( ( -u 1 ^ k ) x. ( P ^ k ) ) )
138 nnm1nn0 
 |-  ( M e. NN -> ( M - 1 ) e. NN0 )
139 hashfz0 
 |-  ( ( M - 1 ) e. NN0 -> ( # ` ( 0 ... ( M - 1 ) ) ) = ( ( M - 1 ) + 1 ) )
140 138 139 syl 
 |-  ( M e. NN -> ( # ` ( 0 ... ( M - 1 ) ) ) = ( ( M - 1 ) + 1 ) )
141 nncn 
 |-  ( M e. NN -> M e. CC )
142 npcan1 
 |-  ( M e. CC -> ( ( M - 1 ) + 1 ) = M )
143 141 142 syl 
 |-  ( M e. NN -> ( ( M - 1 ) + 1 ) = M )
144 140 143 eqtr2d 
 |-  ( M e. NN -> M = ( # ` ( 0 ... ( M - 1 ) ) ) )
145 144 3ad2ant2 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> M = ( # ` ( 0 ... ( M - 1 ) ) ) )
146 145 adantr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. M = 1 ) -> M = ( # ` ( 0 ... ( M - 1 ) ) ) )
147 146 breq2d 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. M = 1 ) -> ( 2 || M <-> 2 || ( # ` ( 0 ... ( M - 1 ) ) ) ) )
148 147 notbid 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. M = 1 ) -> ( -. 2 || M <-> -. 2 || ( # ` ( 0 ... ( M - 1 ) ) ) ) )
149 148 biimpd 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. M = 1 ) -> ( -. 2 || M -> -. 2 || ( # ` ( 0 ... ( M - 1 ) ) ) ) )
150 149 impr 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> -. 2 || ( # ` ( 0 ... ( M - 1 ) ) ) )
151 150 adantr 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> -. 2 || ( # ` ( 0 ... ( M - 1 ) ) ) )
152 73 86 137 151 oddsumodd 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> -. 2 || sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) )
153 152 pm2.21d 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> ( 2 || sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) -> M = 1 ) )
154 153 adantr 
 |-  ( ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) ) -> ( 2 || sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) -> M = 1 ) )
155 72 154 sylbird 
 |-  ( ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) /\ sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) ) -> ( 2 || ( 2 ^ n ) -> M = 1 ) )
156 155 ex 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) -> ( 2 || ( 2 ^ n ) -> M = 1 ) ) )
157 70 156 mpid 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) /\ n e. NN ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) -> M = 1 ) )
158 157 rexlimdva 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> ( E. n e. NN sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) = ( 2 ^ n ) -> M = 1 ) )
159 66 158 syld 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. M = 1 /\ -. 2 || M ) ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> M = 1 ) )
160 159 exp32 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( -. M = 1 -> ( -. 2 || M -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> M = 1 ) ) ) )
161 160 com12 
 |-  ( -. M = 1 -> ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( -. 2 || M -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> M = 1 ) ) ) )
162 161 impd 
 |-  ( -. M = 1 -> ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> M = 1 ) ) )
163 46 162 pm2.61i 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> M = 1 ) )
164 163 adantr 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) /\ ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( 2 ^ N ) -> M = 1 ) )
165 45 164 sylbid 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) /\ ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) ) -> ( sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) || ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) -> M = 1 ) )
166 43 165 mpd 
 |-  ( ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) /\ ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) ) -> M = 1 )
167 166 ex 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( ( ( P + 1 ) x. sum_ k e. ( 0 ... ( M - 1 ) ) ( ( -u 1 ^ k ) x. ( P ^ k ) ) ) = ( 2 ^ N ) -> M = 1 ) )
168 22 167 sylbid 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( ( ( P ^ M ) + 1 ) = ( 2 ^ N ) -> M = 1 ) )
169 17 168 sylbid 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ -. 2 || M ) -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) -> M = 1 ) )
170 169 ex 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( -. 2 || M -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
171 170 adantld 
 |-  ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) -> ( ( -. 2 || N /\ -. 2 || M ) -> ( ( ( 2 ^ N ) - 1 ) = ( P ^ M ) -> M = 1 ) ) )
172 171 3imp 
 |-  ( ( ( P e. ( Prime \ { 2 } ) /\ M e. NN /\ N e. NN ) /\ ( -. 2 || N /\ -. 2 || M ) /\ ( ( 2 ^ N ) - 1 ) = ( P ^ M ) ) -> M = 1 )