Metamath Proof Explorer

Theorem lighneallem3

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

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