Metamath Proof Explorer

Theorem mersenne

Description: A Mersenne prime is a prime number of the form 2 ^ P - 1 . This theorem shows that the P in this expression is necessarily also prime. (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion mersenne ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 𝑃 ∈ ℙ )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 𝑃 ∈ ℤ )
2 2nn0 ⊢ 2 ∈ ℕ0
3 2 numexp1 ⊢ ( 2 ↑ 1 ) = 2
4 df-2 ⊢ 2 = ( 1 + 1 )
5 3 4 eqtri ⊢ ( 2 ↑ 1 ) = ( 1 + 1 )
6 prmuz2 ⊢ ( ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ → ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ( ℤ≥ ‘ 2 ) )
7 6 adantl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ( ℤ≥ ‘ 2 ) )
8 eluz2gt1 ⊢ ( ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ( ℤ≥ ‘ 2 ) → 1 < ( ( 2 ↑ 𝑃 ) − 1 ) )
9 7 8 syl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 1 < ( ( 2 ↑ 𝑃 ) − 1 ) )
10 1red ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 1 ∈ ℝ )
11 2re ⊢ 2 ∈ ℝ
12 11 a1i ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 2 ∈ ℝ )
13 2ne0 ⊢ 2 ≠ 0
14 13 a1i ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 2 ≠ 0 )
15 12 14 1 reexpclzd ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( 2 ↑ 𝑃 ) ∈ ℝ )
16 10 10 15 ltaddsubd ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( ( 1 + 1 ) < ( 2 ↑ 𝑃 ) ↔ 1 < ( ( 2 ↑ 𝑃 ) − 1 ) ) )
17 9 16 mpbird ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( 1 + 1 ) < ( 2 ↑ 𝑃 ) )
18 5 17 eqbrtrid ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( 2 ↑ 1 ) < ( 2 ↑ 𝑃 ) )
19 1zzd ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 1 ∈ ℤ )
20 1lt2 ⊢ 1 < 2
21 20 a1i ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 1 < 2 )
22 12 19 1 21 ltexp2d ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( 1 < 𝑃 ↔ ( 2 ↑ 1 ) < ( 2 ↑ 𝑃 ) ) )
23 18 22 mpbird ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 1 < 𝑃 )
24 eluz2b1 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑃 ∈ ℤ ∧ 1 < 𝑃 ) )
25 1 23 24 sylanbrc ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
26 simpllr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ )
27 prmnn ⊢ ( ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ → ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℕ )
28 26 27 syl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℕ )
29 28 nncnd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℂ )
30 2nn ⊢ 2 ∈ ℕ
31 elfzuz ⊢ ( 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
32 31 ad2antlr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
33 eluz2nn ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 𝑘 ∈ ℕ )
34 32 33 syl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 ∈ ℕ )
35 34 nnnn0d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 ∈ ℕ0 )
36 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
37 30 35 36 sylancr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
38 37 nnzd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑘 ) ∈ ℤ )
39 peano2zm ⊢ ( ( 2 ↑ 𝑘 ) ∈ ℤ → ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℤ )
40 38 39 syl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℤ )
41 40 zred ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℝ )
42 41 recnd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℂ )
43 0red ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 0 ∈ ℝ )
44 1red ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 1 ∈ ℝ )
45 0lt1 ⊢ 0 < 1
46 45 a1i ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 0 < 1 )
47 eluz2gt1 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑘 )
48 32 47 syl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 1 < 𝑘 )
49 11 a1i ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 2 ∈ ℝ )
50 1zzd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 1 ∈ ℤ )
51 elfzelz ⊢ ( 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) → 𝑘 ∈ ℤ )
52 51 ad2antlr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 ∈ ℤ )
53 20 a1i ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 1 < 2 )
54 49 50 52 53 ltexp2d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 1 < 𝑘 ↔ ( 2 ↑ 1 ) < ( 2 ↑ 𝑘 ) ) )
55 48 54 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 1 ) < ( 2 ↑ 𝑘 ) )
56 5 55 eqbrtrrid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 1 + 1 ) < ( 2 ↑ 𝑘 ) )
57 37 nnred ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑘 ) ∈ ℝ )
58 44 44 57 ltaddsubd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 1 + 1 ) < ( 2 ↑ 𝑘 ) ↔ 1 < ( ( 2 ↑ 𝑘 ) − 1 ) ) )
59 56 58 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 1 < ( ( 2 ↑ 𝑘 ) − 1 ) )
60 43 44 41 46 59 lttrd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 0 < ( ( 2 ↑ 𝑘 ) − 1 ) )
61 elnnz ⊢ ( ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℕ ↔ ( ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℤ ∧ 0 < ( ( 2 ↑ 𝑘 ) − 1 ) ) )
62 40 60 61 sylanbrc ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℕ )
63 62 nnne0d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑘 ) − 1 ) ≠ 0 )
64 29 42 63 divcan2d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( ( 2 ↑ 𝑘 ) − 1 ) · ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ) = ( ( 2 ↑ 𝑃 ) − 1 ) )
65 64 26 eqeltrd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( ( 2 ↑ 𝑘 ) − 1 ) · ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ) ∈ ℙ )
66 eluz2b2 ⊢ ( ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℕ ∧ 1 < ( ( 2 ↑ 𝑘 ) − 1 ) ) )
67 62 59 66 sylanbrc ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ( ℤ≥ ‘ 2 ) )
68 37 nncnd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑘 ) ∈ ℂ )
69 ax-1cn ⊢ 1 ∈ ℂ
70 subeq0 ⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 2 ↑ 𝑘 ) − 1 ) = 0 ↔ ( 2 ↑ 𝑘 ) = 1 ) )
71 68 69 70 sylancl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( ( 2 ↑ 𝑘 ) − 1 ) = 0 ↔ ( 2 ↑ 𝑘 ) = 1 ) )
72 71 necon3bid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( ( 2 ↑ 𝑘 ) − 1 ) ≠ 0 ↔ ( 2 ↑ 𝑘 ) ≠ 1 ) )
73 63 72 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑘 ) ≠ 1 )
74 simpr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 ∥ 𝑃 )
75 eluz2nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
76 25 75 syl ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 𝑃 ∈ ℕ )
77 76 ad2antrr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑃 ∈ ℕ )
78 nndivdvds ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ∥ 𝑃 ↔ ( 𝑃 / 𝑘 ) ∈ ℕ ) )
79 77 34 78 syl2anc ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 𝑘 ∥ 𝑃 ↔ ( 𝑃 / 𝑘 ) ∈ ℕ ) )
80 74 79 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 𝑃 / 𝑘 ) ∈ ℕ )
81 80 nnnn0d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 𝑃 / 𝑘 ) ∈ ℕ0 )
82 68 73 81 geoser ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑃 / 𝑘 ) − 1 ) ) ( ( 2 ↑ 𝑘 ) ↑ 𝑛 ) = ( ( 1 − ( ( 2 ↑ 𝑘 ) ↑ ( 𝑃 / 𝑘 ) ) ) / ( 1 − ( 2 ↑ 𝑘 ) ) ) )
83 15 ad2antrr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑃 ) ∈ ℝ )
84 83 recnd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑃 ) ∈ ℂ )
85 negsubdi2 ⊢ ( ( ( 2 ↑ 𝑃 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( 2 ↑ 𝑃 ) − 1 ) = ( 1 − ( 2 ↑ 𝑃 ) ) )
86 84 69 85 sylancl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → - ( ( 2 ↑ 𝑃 ) − 1 ) = ( 1 − ( 2 ↑ 𝑃 ) ) )
87 77 nncnd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑃 ∈ ℂ )
88 34 nncnd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 ∈ ℂ )
89 34 nnne0d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 ≠ 0 )
90 87 88 89 divcan2d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 𝑘 · ( 𝑃 / 𝑘 ) ) = 𝑃 )
91 90 oveq2d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ ( 𝑘 · ( 𝑃 / 𝑘 ) ) ) = ( 2 ↑ 𝑃 ) )
92 49 recnd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 2 ∈ ℂ )
93 92 81 35 expmuld ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ ( 𝑘 · ( 𝑃 / 𝑘 ) ) ) = ( ( 2 ↑ 𝑘 ) ↑ ( 𝑃 / 𝑘 ) ) )
94 91 93 eqtr3d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑃 ) = ( ( 2 ↑ 𝑘 ) ↑ ( 𝑃 / 𝑘 ) ) )
95 94 oveq2d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 1 − ( 2 ↑ 𝑃 ) ) = ( 1 − ( ( 2 ↑ 𝑘 ) ↑ ( 𝑃 / 𝑘 ) ) ) )
96 86 95 eqtrd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → - ( ( 2 ↑ 𝑃 ) − 1 ) = ( 1 − ( ( 2 ↑ 𝑘 ) ↑ ( 𝑃 / 𝑘 ) ) ) )
97 negsubdi2 ⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( 2 ↑ 𝑘 ) − 1 ) = ( 1 − ( 2 ↑ 𝑘 ) ) )
98 68 69 97 sylancl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → - ( ( 2 ↑ 𝑘 ) − 1 ) = ( 1 − ( 2 ↑ 𝑘 ) ) )
99 96 98 oveq12d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( - ( ( 2 ↑ 𝑃 ) − 1 ) / - ( ( 2 ↑ 𝑘 ) − 1 ) ) = ( ( 1 − ( ( 2 ↑ 𝑘 ) ↑ ( 𝑃 / 𝑘 ) ) ) / ( 1 − ( 2 ↑ 𝑘 ) ) ) )
100 29 42 63 div2negd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( - ( ( 2 ↑ 𝑃 ) − 1 ) / - ( ( 2 ↑ 𝑘 ) − 1 ) ) = ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) )
101 82 99 100 3eqtr2d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑃 / 𝑘 ) − 1 ) ) ( ( 2 ↑ 𝑘 ) ↑ 𝑛 ) = ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) )
102 fzfid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 0 ... ( ( 𝑃 / 𝑘 ) − 1 ) ) ∈ Fin )
103 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... ( ( 𝑃 / 𝑘 ) − 1 ) ) → 𝑛 ∈ ℕ0 )
104 zexpcl ⊢ ( ( ( 2 ↑ 𝑘 ) ∈ ℤ ∧ 𝑛 ∈ ℕ0 ) → ( ( 2 ↑ 𝑘 ) ↑ 𝑛 ) ∈ ℤ )
105 38 103 104 syl2an ⊢ ( ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) ∧ 𝑛 ∈ ( 0 ... ( ( 𝑃 / 𝑘 ) − 1 ) ) ) → ( ( 2 ↑ 𝑘 ) ↑ 𝑛 ) ∈ ℤ )
106 102 105 fsumzcl ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → Σ 𝑛 ∈ ( 0 ... ( ( 𝑃 / 𝑘 ) − 1 ) ) ( ( 2 ↑ 𝑘 ) ↑ 𝑛 ) ∈ ℤ )
107 101 106 eqeltrrd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ∈ ℤ )
108 42 mullidd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 1 · ( ( 2 ↑ 𝑘 ) − 1 ) ) = ( ( 2 ↑ 𝑘 ) − 1 ) )
109 2z ⊢ 2 ∈ ℤ
110 elfzm11 ⊢ ( ( 2 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃 ) ) )
111 109 1 110 sylancr ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ( 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃 ) ) )
112 111 biimpa ⊢ ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) → ( 𝑘 ∈ ℤ ∧ 2 ≤ 𝑘 ∧ 𝑘 < 𝑃 ) )
113 112 simp3d ⊢ ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) → 𝑘 < 𝑃 )
114 113 adantr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑘 < 𝑃 )
115 1 ad2antrr ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 𝑃 ∈ ℤ )
116 49 52 115 53 ltexp2d ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 𝑘 < 𝑃 ↔ ( 2 ↑ 𝑘 ) < ( 2 ↑ 𝑃 ) ) )
117 114 116 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 2 ↑ 𝑘 ) < ( 2 ↑ 𝑃 ) )
118 57 83 44 117 ltsub1dd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑘 ) − 1 ) < ( ( 2 ↑ 𝑃 ) − 1 ) )
119 108 118 eqbrtrd ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( 1 · ( ( 2 ↑ 𝑘 ) − 1 ) ) < ( ( 2 ↑ 𝑃 ) − 1 ) )
120 28 nnred ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℝ )
121 ltmuldiv ⊢ ( ( 1 ∈ ℝ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℝ ∧ ( ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ℝ ∧ 0 < ( ( 2 ↑ 𝑘 ) − 1 ) ) ) → ( ( 1 · ( ( 2 ↑ 𝑘 ) − 1 ) ) < ( ( 2 ↑ 𝑃 ) − 1 ) ↔ 1 < ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ) )
122 44 120 41 60 121 syl112anc ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( 1 · ( ( 2 ↑ 𝑘 ) − 1 ) ) < ( ( 2 ↑ 𝑃 ) − 1 ) ↔ 1 < ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ) )
123 119 122 mpbid ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → 1 < ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) )
124 eluz2b1 ⊢ ( ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ∈ ( ℤ≥ ‘ 2 ) ↔ ( ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ∈ ℤ ∧ 1 < ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ) )
125 107 123 124 sylanbrc ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ∈ ( ℤ≥ ‘ 2 ) )
126 nprm ⊢ ( ( ( ( 2 ↑ 𝑘 ) − 1 ) ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ∈ ( ℤ≥ ‘ 2 ) ) → ¬ ( ( ( 2 ↑ 𝑘 ) − 1 ) · ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ) ∈ ℙ )
127 67 125 126 syl2anc ⊢ ( ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ∧ 𝑘 ∥ 𝑃 ) → ¬ ( ( ( 2 ↑ 𝑘 ) − 1 ) · ( ( ( 2 ↑ 𝑃 ) − 1 ) / ( ( 2 ↑ 𝑘 ) − 1 ) ) ) ∈ ℙ )
128 65 127 pm2.65da ⊢ ( ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) ∧ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑘 ∥ 𝑃 )
129 128 ralrimiva ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → ∀ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ¬ 𝑘 ∥ 𝑃 )
130 isprm3 ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑘 ∈ ( 2 ... ( 𝑃 − 1 ) ) ¬ 𝑘 ∥ 𝑃 ) )
131 25 129 130 sylanbrc ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 2 ↑ 𝑃 ) − 1 ) ∈ ℙ ) → 𝑃 ∈ ℙ )