Metamath Proof Explorer

Theorem lighneallem4

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

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

Proof

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