Metamath Proof Explorer

Theorem 2pwp1prm

Description: For ( ( 2 ^ k ) + 1 ) to be prime, k must be a power of 2, see Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number , 5-Aug-2021. (Contributed by AV, 7-Aug-2021)

Ref Expression
Assertion 2pwp1prm ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) )

Proof

Step Hyp Ref Expression
1 oddprmdvds ⊢ ( ( 𝐾 ∈ ℕ ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 )
2 1 adantlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) → ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 )
3 eldifi ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 𝑝 ∈ ℙ )
4 prmnn ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
5 3 4 syl ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 𝑝 ∈ ℕ )
6 simpl ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) → 𝐾 ∈ ℕ )
7 nndivides ⊢ ( ( 𝑝 ∈ ℕ ∧ 𝐾 ∈ ℕ ) → ( 𝑝 ∥ 𝐾 ↔ ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑝 ) = 𝐾 ) )
8 5 6 7 syl2anr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑝 ∥ 𝐾 ↔ ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑝 ) = 𝐾 ) )
9 2re ⊢ 2 ∈ ℝ
10 9 a1i ⊢ ( 𝑚 ∈ ℕ → 2 ∈ ℝ )
11 nnnn0 ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℕ0 )
12 1le2 ⊢ 1 ≤ 2
13 12 a1i ⊢ ( 𝑚 ∈ ℕ → 1 ≤ 2 )
14 10 11 13 expge1d ⊢ ( 𝑚 ∈ ℕ → 1 ≤ ( 2 ↑ 𝑚 ) )
15 1zzd ⊢ ( 𝑚 ∈ ℕ → 1 ∈ ℤ )
16 2nn ⊢ 2 ∈ ℕ
17 16 a1i ⊢ ( 𝑚 ∈ ℕ → 2 ∈ ℕ )
18 17 11 nnexpcld ⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℕ )
19 18 nnzd ⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℤ )
20 zleltp1 ⊢ ( ( 1 ∈ ℤ ∧ ( 2 ↑ 𝑚 ) ∈ ℤ ) → ( 1 ≤ ( 2 ↑ 𝑚 ) ↔ 1 < ( ( 2 ↑ 𝑚 ) + 1 ) ) )
21 15 19 20 syl2anc ⊢ ( 𝑚 ∈ ℕ → ( 1 ≤ ( 2 ↑ 𝑚 ) ↔ 1 < ( ( 2 ↑ 𝑚 ) + 1 ) ) )
22 14 21 mpbid ⊢ ( 𝑚 ∈ ℕ → 1 < ( ( 2 ↑ 𝑚 ) + 1 ) )
23 18 nncnd ⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℂ )
24 1cnd ⊢ ( 𝑚 ∈ ℕ → 1 ∈ ℂ )
25 subneg ⊢ ( ( ( 2 ↑ 𝑚 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 ↑ 𝑚 ) − - 1 ) = ( ( 2 ↑ 𝑚 ) + 1 ) )
26 25 breq2d ⊢ ( ( ( 2 ↑ 𝑚 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( 1 < ( ( 2 ↑ 𝑚 ) − - 1 ) ↔ 1 < ( ( 2 ↑ 𝑚 ) + 1 ) ) )
27 23 24 26 syl2anc ⊢ ( 𝑚 ∈ ℕ → ( 1 < ( ( 2 ↑ 𝑚 ) − - 1 ) ↔ 1 < ( ( 2 ↑ 𝑚 ) + 1 ) ) )
28 22 27 mpbird ⊢ ( 𝑚 ∈ ℕ → 1 < ( ( 2 ↑ 𝑚 ) − - 1 ) )
29 28 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 1 < ( ( 2 ↑ 𝑚 ) − - 1 ) )
30 29 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → 1 < ( ( 2 ↑ 𝑚 ) − - 1 ) )
31 18 nnred ⊢ ( 𝑚 ∈ ℕ → ( 2 ↑ 𝑚 ) ∈ ℝ )
32 31 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℝ )
33 16 a1i ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 2 ∈ ℕ )
34 11 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℕ0 )
35 5 nnnn0d ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 𝑝 ∈ ℕ0 )
36 35 adantr ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 𝑝 ∈ ℕ0 )
37 34 36 nn0mulcld ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 · 𝑝 ) ∈ ℕ0 )
38 33 37 nnexpcld ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ ( 𝑚 · 𝑝 ) ) ∈ ℕ )
39 38 nnred ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ ( 𝑚 · 𝑝 ) ) ∈ ℝ )
40 1red ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 1 ∈ ℝ )
41 9 a1i ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 2 ∈ ℝ )
42 nnz ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
43 42 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℤ )
44 5 nnzd ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 𝑝 ∈ ℤ )
45 44 adantr ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 𝑝 ∈ ℤ )
46 43 45 zmulcld ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 𝑚 · 𝑝 ) ∈ ℤ )
47 1lt2 ⊢ 1 < 2
48 47 a1i ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 1 < 2 )
49 prmgt1 ⊢ ( 𝑝 ∈ ℙ → 1 < 𝑝 )
50 3 49 syl ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 1 < 𝑝 )
51 50 adantr ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 1 < 𝑝 )
52 nnre ⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℝ )
53 52 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 𝑚 ∈ ℝ )
54 5 nnred ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 𝑝 ∈ ℝ )
55 54 adantr ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 𝑝 ∈ ℝ )
56 nngt0 ⊢ ( 𝑚 ∈ ℕ → 0 < 𝑚 )
57 56 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 0 < 𝑚 )
58 ltmulgt11 ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝑝 ∈ ℝ ∧ 0 < 𝑚 ) → ( 1 < 𝑝 ↔ 𝑚 < ( 𝑚 · 𝑝 ) ) )
59 53 55 57 58 syl3anc ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 1 < 𝑝 ↔ 𝑚 < ( 𝑚 · 𝑝 ) ) )
60 51 59 mpbid ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 𝑚 < ( 𝑚 · 𝑝 ) )
61 ltexp2a ⊢ ( ( ( 2 ∈ ℝ ∧ 𝑚 ∈ ℤ ∧ ( 𝑚 · 𝑝 ) ∈ ℤ ) ∧ ( 1 < 2 ∧ 𝑚 < ( 𝑚 · 𝑝 ) ) ) → ( 2 ↑ 𝑚 ) < ( 2 ↑ ( 𝑚 · 𝑝 ) ) )
62 41 43 46 48 60 61 syl32anc ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) < ( 2 ↑ ( 𝑚 · 𝑝 ) ) )
63 32 39 40 62 ltadd1dd ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ 𝑚 ) + 1 ) < ( ( 2 ↑ ( 𝑚 · 𝑝 ) ) + 1 ) )
64 63 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝑚 ) + 1 ) < ( ( 2 ↑ ( 𝑚 · 𝑝 ) ) + 1 ) )
65 23 24 subnegd ⊢ ( 𝑚 ∈ ℕ → ( ( 2 ↑ 𝑚 ) − - 1 ) = ( ( 2 ↑ 𝑚 ) + 1 ) )
66 65 eqcomd ⊢ ( 𝑚 ∈ ℕ → ( ( 2 ↑ 𝑚 ) + 1 ) = ( ( 2 ↑ 𝑚 ) − - 1 ) )
67 66 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ 𝑚 ) + 1 ) = ( ( 2 ↑ 𝑚 ) − - 1 ) )
68 67 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝑚 ) + 1 ) = ( ( 2 ↑ 𝑚 ) − - 1 ) )
69 oveq2 ⊢ ( ( 𝑚 · 𝑝 ) = 𝐾 → ( 2 ↑ ( 𝑚 · 𝑝 ) ) = ( 2 ↑ 𝐾 ) )
70 69 oveq1d ⊢ ( ( 𝑚 · 𝑝 ) = 𝐾 → ( ( 2 ↑ ( 𝑚 · 𝑝 ) ) + 1 ) = ( ( 2 ↑ 𝐾 ) + 1 ) )
71 70 adantl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ ( 𝑚 · 𝑝 ) ) + 1 ) = ( ( 2 ↑ 𝐾 ) + 1 ) )
72 64 68 71 3brtr3d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝑚 ) − - 1 ) < ( ( 2 ↑ 𝐾 ) + 1 ) )
73 neg1z ⊢ - 1 ∈ ℤ
74 73 a1i ⊢ ( 𝑚 ∈ ℕ → - 1 ∈ ℤ )
75 19 74 zsubcld ⊢ ( 𝑚 ∈ ℕ → ( ( 2 ↑ 𝑚 ) − - 1 ) ∈ ℤ )
76 75 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ 𝑚 ) − - 1 ) ∈ ℤ )
77 fzofi ⊢ ( 0 ..^ 𝑝 ) ∈ Fin
78 77 a1i ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 0 ..^ 𝑝 ) ∈ Fin )
79 19 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℤ )
80 elfzonn0 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑝 ) → 𝑘 ∈ ℕ0 )
81 zexpcl ⊢ ( ( ( 2 ↑ 𝑚 ) ∈ ℤ ∧ 𝑘 ∈ ℕ0 ) → ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) ∈ ℤ )
82 79 80 81 syl2an ⊢ ( ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑝 ) ) → ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) ∈ ℤ )
83 73 a1i ⊢ ( ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑝 ) ) → - 1 ∈ ℤ )
84 fzonnsub ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑝 ) → ( 𝑝 − 𝑘 ) ∈ ℕ )
85 84 adantl ⊢ ( ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑝 ) ) → ( 𝑝 − 𝑘 ) ∈ ℕ )
86 nnm1nn0 ⊢ ( ( 𝑝 − 𝑘 ) ∈ ℕ → ( ( 𝑝 − 𝑘 ) − 1 ) ∈ ℕ0 )
87 85 86 syl ⊢ ( ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑝 ) ) → ( ( 𝑝 − 𝑘 ) − 1 ) ∈ ℕ0 )
88 zexpcl ⊢ ( ( - 1 ∈ ℤ ∧ ( ( 𝑝 − 𝑘 ) − 1 ) ∈ ℕ0 ) → ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ∈ ℤ )
89 83 87 88 syl2anc ⊢ ( ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑝 ) ) → ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ∈ ℤ )
90 82 89 zmulcld ⊢ ( ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ∧ 𝑘 ∈ ( 0 ..^ 𝑝 ) ) → ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ∈ ℤ )
91 78 90 fsumzcl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ∈ ℤ )
92 dvdsmul1 ⊢ ( ( ( ( 2 ↑ 𝑚 ) − - 1 ) ∈ ℤ ∧ Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ∈ ℤ ) → ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) − - 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ) )
93 76 91 92 syl2anc ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) − - 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ) )
94 93 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) − - 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ) )
95 23 adantl ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ 𝑚 ) ∈ ℂ )
96 neg1cn ⊢ - 1 ∈ ℂ
97 96 a1i ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → - 1 ∈ ℂ )
98 pwdif ⊢ ( ( 𝑝 ∈ ℕ0 ∧ ( 2 ↑ 𝑚 ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) = ( ( ( 2 ↑ 𝑚 ) − - 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ) )
99 36 95 97 98 syl3anc ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) = ( ( ( 2 ↑ 𝑚 ) − - 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ) )
100 99 breq2d ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) ↔ ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) − - 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ) ) )
101 100 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) ↔ ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) − - 1 ) · Σ 𝑘 ∈ ( 0 ..^ 𝑝 ) ( ( ( 2 ↑ 𝑚 ) ↑ 𝑘 ) · ( - 1 ↑ ( ( 𝑝 − 𝑘 ) − 1 ) ) ) ) ) )
102 94 101 mpbird ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) )
103 2cnd ⊢ ( 𝐾 ∈ ℕ → 2 ∈ ℂ )
104 nnnn0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ∈ ℕ0 )
105 103 104 expcld ⊢ ( 𝐾 ∈ ℕ → ( 2 ↑ 𝐾 ) ∈ ℂ )
106 1cnd ⊢ ( 𝐾 ∈ ℕ → 1 ∈ ℂ )
107 105 106 subnegd ⊢ ( 𝐾 ∈ ℕ → ( ( 2 ↑ 𝐾 ) − - 1 ) = ( ( 2 ↑ 𝐾 ) + 1 ) )
108 107 eqcomd ⊢ ( 𝐾 ∈ ℕ → ( ( 2 ↑ 𝐾 ) + 1 ) = ( ( 2 ↑ 𝐾 ) − - 1 ) )
109 108 adantr ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) → ( ( 2 ↑ 𝐾 ) + 1 ) = ( ( 2 ↑ 𝐾 ) − - 1 ) )
110 109 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝐾 ) + 1 ) = ( ( 2 ↑ 𝐾 ) − - 1 ) )
111 oveq2 ⊢ ( 𝐾 = ( 𝑚 · 𝑝 ) → ( 2 ↑ 𝐾 ) = ( 2 ↑ ( 𝑚 · 𝑝 ) ) )
112 111 eqcoms ⊢ ( ( 𝑚 · 𝑝 ) = 𝐾 → ( 2 ↑ 𝐾 ) = ( 2 ↑ ( 𝑚 · 𝑝 ) ) )
113 112 adantl ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( 2 ↑ 𝐾 ) = ( 2 ↑ ( 𝑚 · 𝑝 ) ) )
114 2cnd ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → 2 ∈ ℂ )
115 114 36 34 expmuld ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( 2 ↑ ( 𝑚 · 𝑝 ) ) = ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) )
116 115 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( 2 ↑ ( 𝑚 · 𝑝 ) ) = ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) )
117 113 116 eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( 2 ↑ 𝐾 ) = ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) )
118 1exp ⊢ ( 𝑝 ∈ ℤ → ( 1 ↑ 𝑝 ) = 1 )
119 44 118 syl ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → ( 1 ↑ 𝑝 ) = 1 )
120 119 eqcomd ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 1 = ( 1 ↑ 𝑝 ) )
121 120 negeqd ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → - 1 = - ( 1 ↑ 𝑝 ) )
122 1cnd ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → 1 ∈ ℂ )
123 oddn2prm ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → ¬ 2 ∥ 𝑝 )
124 oexpneg ⊢ ( ( 1 ∈ ℂ ∧ 𝑝 ∈ ℕ ∧ ¬ 2 ∥ 𝑝 ) → ( - 1 ↑ 𝑝 ) = - ( 1 ↑ 𝑝 ) )
125 122 5 123 124 syl3anc ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → ( - 1 ↑ 𝑝 ) = - ( 1 ↑ 𝑝 ) )
126 125 eqcomd ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → - ( 1 ↑ 𝑝 ) = ( - 1 ↑ 𝑝 ) )
127 121 126 eqtrd ⊢ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) → - 1 = ( - 1 ↑ 𝑝 ) )
128 127 adantr ⊢ ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → - 1 = ( - 1 ↑ 𝑝 ) )
129 128 ad2antlr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → - 1 = ( - 1 ↑ 𝑝 ) )
130 117 129 oveq12d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝐾 ) − - 1 ) = ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) )
131 110 130 eqtrd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝐾 ) + 1 ) = ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) )
132 131 breq2d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( 2 ↑ 𝐾 ) + 1 ) ↔ ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( ( 2 ↑ 𝑚 ) ↑ 𝑝 ) − ( - 1 ↑ 𝑝 ) ) ) )
133 102 132 mpbird ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( 2 ↑ 𝑚 ) − - 1 ) ∥ ( ( 2 ↑ 𝐾 ) + 1 ) )
134 30 72 133 dvdsnprmd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ¬ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ )
135 134 pm2.21d ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) ∧ ( 𝑚 · 𝑝 ) = 𝐾 ) → ( ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) )
136 135 ex ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) → ( ( 𝑚 · 𝑝 ) = 𝐾 → ( ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) ) )
137 136 com23 ⊢ ( ( 𝐾 ∈ ℕ ∧ ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) ) → ( ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ → ( ( 𝑚 · 𝑝 ) = 𝐾 → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) ) )
138 137 impancom ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) → ( ( 𝑝 ∈ ( ℙ ∖ { 2 } ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑝 ) = 𝐾 → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) ) )
139 138 impl ⊢ ( ( ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ℙ ∖ { 2 } ) ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝑚 · 𝑝 ) = 𝐾 → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) )
140 139 rexlimdva ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ℙ ∖ { 2 } ) ) → ( ∃ 𝑚 ∈ ℕ ( 𝑚 · 𝑝 ) = 𝐾 → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) )
141 8 140 sylbid ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) ∧ 𝑝 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑝 ∥ 𝐾 → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) )
142 141 rexlimdva ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) → ( ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) )
143 142 adantr ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) → ( ∃ 𝑝 ∈ ( ℙ ∖ { 2 } ) 𝑝 ∥ 𝐾 → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) )
144 2 143 mpd ⊢ ( ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) ∧ ¬ ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) ) → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) )
145 144 pm2.18da ⊢ ( ( 𝐾 ∈ ℕ ∧ ( ( 2 ↑ 𝐾 ) + 1 ) ∈ ℙ ) → ∃ 𝑛 ∈ ℕ0 𝐾 = ( 2 ↑ 𝑛 ) )