Metamath Proof Explorer

Theorem proththd

Description: Proth's theorem (1878). If P is aProth number, i.e. a number of the form k2^n+1 with k less than 2^n, and if there exists an integer x for which x^((P-1)/2) is -1 modulo P, then P is prime. Such a prime is called aProth prime. Like Pocklington's theorem (see pockthg ), Proth's theorem allows for a convenient method for verifying large primes. (Contributed by AV, 5-Jul-2020)

Ref Expression
Hypotheses proththd.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
proththd.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
proththd.p ⊢ ( 𝜑 → 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) )
proththd.l ⊢ ( 𝜑 → 𝐾 < ( 2 ↑ 𝑁 ) )
proththd.x ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
Assertion proththd ( 𝜑 → 𝑃 ∈ ℙ )

Proof

Step Hyp Ref Expression
1 proththd.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 proththd.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 proththd.p ⊢ ( 𝜑 → 𝑃 = ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) )
4 proththd.l ⊢ ( 𝜑 → 𝐾 < ( 2 ↑ 𝑁 ) )
5 proththd.x ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
6 2nn ⊢ 2 ∈ ℕ
7 6 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
8 1 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 7 8 nnexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ )
10 2 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
11 9 nncnd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℂ )
12 10 11 mulcomd ⊢ ( 𝜑 → ( 𝐾 · ( 2 ↑ 𝑁 ) ) = ( ( 2 ↑ 𝑁 ) · 𝐾 ) )
13 12 oveq1d ⊢ ( 𝜑 → ( ( 𝐾 · ( 2 ↑ 𝑁 ) ) + 1 ) = ( ( ( 2 ↑ 𝑁 ) · 𝐾 ) + 1 ) )
14 3 13 eqtrd ⊢ ( 𝜑 → 𝑃 = ( ( ( 2 ↑ 𝑁 ) · 𝐾 ) + 1 ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
16 2prm ⊢ 2 ∈ ℙ
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 2 ∈ ℙ )
18 1 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → 𝑁 ∈ ℕ )
19 prmdvdsexpb ⊢ ( ( 𝑝 ∈ ℙ ∧ 2 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑝 ∥ ( 2 ↑ 𝑁 ) ↔ 𝑝 = 2 ) )
20 15 17 18 19 syl3anc ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 2 ↑ 𝑁 ) ↔ 𝑝 = 2 ) )
21 1 2 3 proththdlem ⊢ ( 𝜑 → ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) )
22 21 simp1d ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
23 22 nncnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
24 peano2cnm ⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − 1 ) ∈ ℂ )
25 23 24 syl ⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℂ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑃 − 1 ) ∈ ℂ )
27 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 2 ∈ ℂ )
28 2ne0 ⊢ 2 ≠ 0
29 28 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 2 ≠ 0 )
30 26 27 29 divcan1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) = ( 𝑃 − 1 ) )
31 30 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑃 − 1 ) = ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) )
32 31 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ ( 𝑃 − 1 ) ) = ( 𝑥 ↑ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) ) )
33 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
34 33 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℂ )
35 2nn0 ⊢ 2 ∈ ℕ0
36 35 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 2 ∈ ℕ0 )
37 21 simp3d ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
38 37 nnnn0d ⊢ ( 𝜑 → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
40 34 36 39 expmuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ ( ( ( 𝑃 − 1 ) / 2 ) · 2 ) ) = ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) )
41 32 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ ( 𝑃 − 1 ) ) = ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) )
42 41 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( 𝑥 ↑ ( 𝑃 − 1 ) ) = ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) )
43 42 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) mod 𝑃 ) )
44 38 adantr ⊢ ( ( 𝜑 ∧ 𝑝 = 2 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 )
45 44 anim1i ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ∧ 𝑥 ∈ ℤ ) )
46 45 ancomd ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) )
47 zexpcl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
48 46 47 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
49 48 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℤ )
50 22 nnrpd ⊢ ( 𝜑 → 𝑃 ∈ ℝ+ )
51 50 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → 𝑃 ∈ ℝ+ )
52 21 simp2d ⊢ ( 𝜑 → 1 < 𝑃 )
53 52 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → 1 < 𝑃 )
54 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
55 49 51 53 54 modexp2m1d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ↑ 2 ) mod 𝑃 ) = 1 )
56 43 55 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 )
57 oveq2 ⊢ ( 𝑝 = 2 → ( ( 𝑃 − 1 ) / 𝑝 ) = ( ( 𝑃 − 1 ) / 2 ) )
58 57 eleq1d ⊢ ( 𝑝 = 2 → ( ( ( 𝑃 − 1 ) / 𝑝 ) ∈ ℕ0 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ 𝑝 = 2 ) → ( ( ( 𝑃 − 1 ) / 𝑝 ) ∈ ℕ0 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ0 ) )
60 44 59 mpbird ⊢ ( ( 𝜑 ∧ 𝑝 = 2 ) → ( ( 𝑃 − 1 ) / 𝑝 ) ∈ ℕ0 )
61 60 anim2i ⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝜑 ∧ 𝑝 = 2 ) ) → ( 𝑥 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 𝑝 ) ∈ ℕ0 ) )
62 61 ancoms ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 𝑝 ) ∈ ℕ0 ) )
63 zexpcl ⊢ ( ( 𝑥 ∈ ℤ ∧ ( ( 𝑃 − 1 ) / 𝑝 ) ∈ ℕ0 ) → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) ∈ ℤ )
64 62 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) ∈ ℤ )
65 64 zred ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) ∈ ℝ )
66 65 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) ∈ ℝ )
67 1red ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → 1 ∈ ℝ )
68 67 renegcld ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → - 1 ∈ ℝ )
69 oveq2 ⊢ ( 2 = 𝑝 → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 − 1 ) / 𝑝 ) )
70 69 eqcoms ⊢ ( 𝑝 = 2 → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 − 1 ) / 𝑝 ) )
71 70 oveq2d ⊢ ( 𝑝 = 2 → ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) )
72 71 oveq1d ⊢ ( 𝑝 = 2 → ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) mod 𝑃 ) )
73 72 eqeq1d ⊢ ( 𝑝 = 2 → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑝 = 2 ) → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
75 74 adantr ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
76 75 biimpa ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
77 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( 1 mod 𝑃 ) = ( 1 mod 𝑃 ) )
78 66 68 67 67 51 76 77 modsub12d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) mod 𝑃 ) = ( ( - 1 − 1 ) mod 𝑃 ) )
79 78 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) mod 𝑃 ) gcd 𝑃 ) = ( ( ( - 1 − 1 ) mod 𝑃 ) gcd 𝑃 ) )
80 peano2zm ⊢ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) ∈ ℤ → ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) ∈ ℤ )
81 64 80 syl ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) ∈ ℤ )
82 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → 𝑃 ∈ ℕ )
83 modgcd ⊢ ( ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) mod 𝑃 ) gcd 𝑃 ) = ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) )
84 81 82 83 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) mod 𝑃 ) gcd 𝑃 ) = ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) )
85 84 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) mod 𝑃 ) gcd 𝑃 ) = ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) )
86 ax-1cn ⊢ 1 ∈ ℂ
87 negdi2 ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) → - ( 1 + 1 ) = ( - 1 − 1 ) )
88 87 eqcomd ⊢ ( ( 1 ∈ ℂ ∧ 1 ∈ ℂ ) → ( - 1 − 1 ) = - ( 1 + 1 ) )
89 86 86 88 mp2an ⊢ ( - 1 − 1 ) = - ( 1 + 1 )
90 1p1e2 ⊢ ( 1 + 1 ) = 2
91 90 negeqi ⊢ - ( 1 + 1 ) = - 2
92 89 91 eqtri ⊢ ( - 1 − 1 ) = - 2
93 92 a1i ⊢ ( 𝜑 → ( - 1 − 1 ) = - 2 )
94 93 oveq1d ⊢ ( 𝜑 → ( ( - 1 − 1 ) mod 𝑃 ) = ( - 2 mod 𝑃 ) )
95 94 oveq1d ⊢ ( 𝜑 → ( ( ( - 1 − 1 ) mod 𝑃 ) gcd 𝑃 ) = ( ( - 2 mod 𝑃 ) gcd 𝑃 ) )
96 nnnegz ⊢ ( 2 ∈ ℕ → - 2 ∈ ℤ )
97 7 96 syl ⊢ ( 𝜑 → - 2 ∈ ℤ )
98 modgcd ⊢ ( ( - 2 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( - 2 mod 𝑃 ) gcd 𝑃 ) = ( - 2 gcd 𝑃 ) )
99 97 22 98 syl2anc ⊢ ( 𝜑 → ( ( - 2 mod 𝑃 ) gcd 𝑃 ) = ( - 2 gcd 𝑃 ) )
100 2z ⊢ 2 ∈ ℤ
101 22 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
102 neggcd ⊢ ( ( 2 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( - 2 gcd 𝑃 ) = ( 2 gcd 𝑃 ) )
103 100 101 102 sylancr ⊢ ( 𝜑 → ( - 2 gcd 𝑃 ) = ( 2 gcd 𝑃 ) )
104 nnz ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
105 oddm1d2 ⊢ ( 𝑃 ∈ ℤ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
106 104 105 syl ⊢ ( 𝑃 ∈ ℕ → ( ¬ 2 ∥ 𝑃 ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ ) )
107 106 biimprd ⊢ ( 𝑃 ∈ ℕ → ( ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ → ¬ 2 ∥ 𝑃 ) )
108 nnz ⊢ ( ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ → ( ( 𝑃 − 1 ) / 2 ) ∈ ℤ )
109 107 108 impel ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) → ¬ 2 ∥ 𝑃 )
110 isoddgcd1 ⊢ ( 𝑃 ∈ ℤ → ( ¬ 2 ∥ 𝑃 ↔ ( 2 gcd 𝑃 ) = 1 ) )
111 104 110 syl ⊢ ( 𝑃 ∈ ℕ → ( ¬ 2 ∥ 𝑃 ↔ ( 2 gcd 𝑃 ) = 1 ) )
112 111 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) → ( ¬ 2 ∥ 𝑃 ↔ ( 2 gcd 𝑃 ) = 1 ) )
113 109 112 mpbid ⊢ ( ( 𝑃 ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) → ( 2 gcd 𝑃 ) = 1 )
114 113 3adant2 ⊢ ( ( 𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ) → ( 2 gcd 𝑃 ) = 1 )
115 21 114 syl ⊢ ( 𝜑 → ( 2 gcd 𝑃 ) = 1 )
116 103 115 eqtrd ⊢ ( 𝜑 → ( - 2 gcd 𝑃 ) = 1 )
117 99 116 eqtrd ⊢ ( 𝜑 → ( ( - 2 mod 𝑃 ) gcd 𝑃 ) = 1 )
118 95 117 eqtrd ⊢ ( 𝜑 → ( ( ( - 1 − 1 ) mod 𝑃 ) gcd 𝑃 ) = 1 )
119 118 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( - 1 − 1 ) mod 𝑃 ) gcd 𝑃 ) = 1 )
120 79 85 119 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 )
121 56 120 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) ∧ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) )
122 121 ex ⊢ ( ( ( 𝜑 ∧ 𝑝 = 2 ) ∧ 𝑥 ∈ ℤ ) → ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) ) )
123 122 reximdva ⊢ ( ( 𝜑 ∧ 𝑝 = 2 ) → ( ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) ) )
124 123 ex ⊢ ( 𝜑 → ( 𝑝 = 2 → ( ∃ 𝑥 ∈ ℤ ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) ) ) )
125 5 124 mpid ⊢ ( 𝜑 → ( 𝑝 = 2 → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) ) )
126 125 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 = 2 → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) ) )
127 20 126 sylbid ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 ∥ ( 2 ↑ 𝑁 ) → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) ) )
128 127 ralrimiva ⊢ ( 𝜑 → ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ ( 2 ↑ 𝑁 ) → ∃ 𝑥 ∈ ℤ ( ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) mod 𝑃 ) = 1 ∧ ( ( ( 𝑥 ↑ ( ( 𝑃 − 1 ) / 𝑝 ) ) − 1 ) gcd 𝑃 ) = 1 ) ) )
129 9 2 4 14 128 pockthg ⊢ ( 𝜑 → 𝑃 ∈ ℙ )