Metamath Proof Explorer

Theorem lighneallem3

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

Ref Expression
Assertion lighneallem3 ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ ( ¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀 ) ∧ ( ( 2 ↑ 𝑁 ) − 1 ) = ( 𝑃 ↑ 𝑀 ) ) → 𝑀 = 1 )

Proof

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