| Step | Hyp | Ref
| Expression |
| 1 | | 2nn 12339 |
. . . 4
⊢ 2 ∈
ℕ |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 2 ∈
ℕ) |
| 3 | | proththd.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 4 | 3 | nnnn0d 12587 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 5 | 2, 4 | nnexpcld 14284 |
. 2
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
| 6 | | proththd.k |
. 2
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 7 | | proththd.l |
. 2
⊢ (𝜑 → 𝐾 < (2↑𝑁)) |
| 8 | | proththd.p |
. . 3
⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) |
| 9 | 6 | nncnd 12282 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℂ) |
| 10 | 5 | nncnd 12282 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∈ ℂ) |
| 11 | 9, 10 | mulcomd 11282 |
. . . 4
⊢ (𝜑 → (𝐾 · (2↑𝑁)) = ((2↑𝑁) · 𝐾)) |
| 12 | 11 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((𝐾 · (2↑𝑁)) + 1) = (((2↑𝑁) · 𝐾) + 1)) |
| 13 | 8, 12 | eqtrd 2777 |
. 2
⊢ (𝜑 → 𝑃 = (((2↑𝑁) · 𝐾) + 1)) |
| 14 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
| 15 | | 2prm 16729 |
. . . . . 6
⊢ 2 ∈
ℙ |
| 16 | 15 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 2 ∈
ℙ) |
| 17 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → 𝑁 ∈ ℕ) |
| 18 | | prmdvdsexpb 16753 |
. . . . 5
⊢ ((𝑝 ∈ ℙ ∧ 2 ∈
ℙ ∧ 𝑁 ∈
ℕ) → (𝑝 ∥
(2↑𝑁) ↔ 𝑝 = 2)) |
| 19 | 14, 16, 17, 18 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) ↔ 𝑝 = 2)) |
| 20 | | proththd.x |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) |
| 21 | 3, 6, 8 | proththdlem 47600 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈
ℕ)) |
| 22 | 21 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 23 | 22 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 24 | | peano2cnm 11575 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℂ → (𝑃 − 1) ∈
ℂ) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) ∈ ℂ) |
| 27 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈
ℂ) |
| 28 | | 2ne0 12370 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≠
0 |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ≠
0) |
| 30 | 26, 27, 29 | divcan1d 12044 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) · 2) = (𝑃 − 1)) |
| 31 | 30 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑃 − 1) = (((𝑃 − 1) / 2) ·
2)) |
| 32 | 31 | oveq2d 7447 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = (𝑥↑(((𝑃 − 1) / 2) ·
2))) |
| 33 | | zcn 12618 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 34 | 33 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℂ) |
| 35 | | 2nn0 12543 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
| 36 | 35 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 2 ∈
ℕ0) |
| 37 | 21 | simp3d 1145 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ) |
| 38 | 37 | nnnn0d 12587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 − 1) / 2) ∈
ℕ0) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑃 − 1) / 2) ∈
ℕ0) |
| 40 | 34, 36, 39 | expmuld 14189 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(((𝑃 − 1) / 2) · 2)) = ((𝑥↑((𝑃 − 1) / 2))↑2)) |
| 41 | 32, 40 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2)) |
| 42 | 41 | ad4ant13 751 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑(𝑃 − 1)) = ((𝑥↑((𝑃 − 1) / 2))↑2)) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃)) |
| 44 | 38 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 2) ∈
ℕ0) |
| 45 | 44 | anim1i 615 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑃 − 1) / 2) ∈ ℕ0
∧ 𝑥 ∈
ℤ)) |
| 46 | 45 | ancomd 461 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0)) |
| 47 | | zexpcl 14117 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 2) ∈
ℕ0) → (𝑥↑((𝑃 − 1) / 2)) ∈
ℤ) |
| 48 | 46, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 2)) ∈
ℤ) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑((𝑃 − 1) / 2)) ∈
ℤ) |
| 50 | 22 | nnrpd 13075 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
| 51 | 50 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 𝑃 ∈
ℝ+) |
| 52 | 21 | simp2d 1144 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 𝑃) |
| 53 | 52 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 1 < 𝑃) |
| 54 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) |
| 55 | 49, 51, 53, 54 | modexp2m1d 47599 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 2))↑2) mod 𝑃) = 1) |
| 56 | 43, 55 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑(𝑃 − 1)) mod 𝑃) = 1) |
| 57 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 2 → ((𝑃 − 1) / 𝑝) = ((𝑃 − 1) / 2)) |
| 58 | 57 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 2 → (((𝑃 − 1) / 𝑝) ∈ ℕ0 ↔ ((𝑃 − 1) / 2) ∈
ℕ0)) |
| 59 | 58 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑝 = 2) → (((𝑃 − 1) / 𝑝) ∈ ℕ0 ↔ ((𝑃 − 1) / 2) ∈
ℕ0)) |
| 60 | 44, 59 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑝 = 2) → ((𝑃 − 1) / 𝑝) ∈
ℕ0) |
| 61 | 60 | anim2i 617 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℤ ∧ (𝜑 ∧ 𝑝 = 2)) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈
ℕ0)) |
| 62 | 61 | ancoms 458 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈
ℕ0)) |
| 63 | | zexpcl 14117 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℤ ∧ ((𝑃 − 1) / 𝑝) ∈ ℕ0) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ) |
| 65 | 64 | zred 12722 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℝ) |
| 67 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → 1 ∈ ℝ) |
| 68 | 67 | renegcld 11690 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → -1 ∈
ℝ) |
| 69 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (2 =
𝑝 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝)) |
| 70 | 69 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 2 → ((𝑃 − 1) / 2) = ((𝑃 − 1) / 𝑝)) |
| 71 | 70 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 2 → (𝑥↑((𝑃 − 1) / 2)) = (𝑥↑((𝑃 − 1) / 𝑝))) |
| 72 | 71 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 2 → ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃)) |
| 73 | 72 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 2 → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃))) |
| 74 | 73 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑝 = 2) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃))) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃))) |
| 76 | 75 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((𝑥↑((𝑃 − 1) / 𝑝)) mod 𝑃) = (-1 mod 𝑃)) |
| 77 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (1 mod 𝑃) = (1 mod 𝑃)) |
| 78 | 66, 68, 67, 67, 51, 76, 77 | modsub12d 13969 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) = ((-1 − 1) mod 𝑃)) |
| 79 | 78 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((-1 − 1) mod 𝑃) gcd 𝑃)) |
| 80 | | peano2zm 12660 |
. . . . . . . . . . . . . 14
⊢ ((𝑥↑((𝑃 − 1) / 𝑝)) ∈ ℤ → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈
ℤ) |
| 81 | 64, 80 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → ((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈
ℤ) |
| 82 | 22 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → 𝑃 ∈ ℕ) |
| 83 | | modgcd 16569 |
. . . . . . . . . . . . 13
⊢ ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) ∈ ℤ ∧ 𝑃 ∈ ℕ) →
((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃)) |
| 84 | 81, 82, 83 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃)) |
| 85 | 84 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → ((((𝑥↑((𝑃 − 1) / 𝑝)) − 1) mod 𝑃) gcd 𝑃) = (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃)) |
| 86 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
| 87 | | negdi2 11567 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ) → -(1 + 1) = (-1 −
1)) |
| 88 | 87 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ 1 ∈ ℂ) → (-1 − 1) = -(1 +
1)) |
| 89 | 86, 86, 88 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (-1
− 1) = -(1 + 1) |
| 90 | | 1p1e2 12391 |
. . . . . . . . . . . . . . . . . 18
⊢ (1 + 1) =
2 |
| 91 | 90 | negeqi 11501 |
. . . . . . . . . . . . . . . . 17
⊢ -(1 + 1)
= -2 |
| 92 | 89, 91 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ (-1
− 1) = -2 |
| 93 | 92 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (-1 − 1) =
-2) |
| 94 | 93 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((-1 − 1) mod 𝑃) = (-2 mod 𝑃)) |
| 95 | 94 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = ((-2 mod 𝑃) gcd 𝑃)) |
| 96 | | nnnegz 12616 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℕ → -2 ∈ ℤ) |
| 97 | 2, 96 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → -2 ∈
ℤ) |
| 98 | | modgcd 16569 |
. . . . . . . . . . . . . . 15
⊢ ((-2
∈ ℤ ∧ 𝑃
∈ ℕ) → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃)) |
| 99 | 97, 22, 98 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = (-2 gcd 𝑃)) |
| 100 | | 2z 12649 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
| 101 | 22 | nnzd 12640 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ ℤ) |
| 102 | | neggcd 16560 |
. . . . . . . . . . . . . . . 16
⊢ ((2
∈ ℤ ∧ 𝑃
∈ ℤ) → (-2 gcd 𝑃) = (2 gcd 𝑃)) |
| 103 | 100, 101,
102 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (-2 gcd 𝑃) = (2 gcd 𝑃)) |
| 104 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℤ) |
| 105 | | oddm1d2 16397 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
| 106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℕ → (¬ 2
∥ 𝑃 ↔ ((𝑃 − 1) / 2) ∈
ℤ)) |
| 107 | 106 | biimprd 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℕ → (((𝑃 − 1) / 2) ∈ ℤ
→ ¬ 2 ∥ 𝑃)) |
| 108 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑃 − 1) / 2) ∈ ℕ
→ ((𝑃 − 1) / 2)
∈ ℤ) |
| 109 | 107, 108 | impel 505 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ)
→ ¬ 2 ∥ 𝑃) |
| 110 | | isoddgcd1 16768 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ∈ ℤ → (¬ 2
∥ 𝑃 ↔ (2 gcd
𝑃) = 1)) |
| 111 | 104, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ ℕ → (¬ 2
∥ 𝑃 ↔ (2 gcd
𝑃) = 1)) |
| 112 | 111 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ)
→ (¬ 2 ∥ 𝑃
↔ (2 gcd 𝑃) =
1)) |
| 113 | 109, 112 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ)
→ (2 gcd 𝑃) =
1) |
| 114 | 113 | 3adant2 1132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ ℕ ∧ 1 <
𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ) → (2
gcd 𝑃) =
1) |
| 115 | 21, 114 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 gcd 𝑃) = 1) |
| 116 | 103, 115 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (-2 gcd 𝑃) = 1) |
| 117 | 99, 116 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((-2 mod 𝑃) gcd 𝑃) = 1) |
| 118 | 95, 117 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1) |
| 119 | 118 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((-1 − 1) mod 𝑃) gcd 𝑃) = 1) |
| 120 | 79, 85, 119 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1) |
| 121 | 56, 120 | jca 511 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) ∧ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)) → (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)) |
| 122 | 121 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑝 = 2) ∧ 𝑥 ∈ ℤ) → (((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
| 123 | 122 | reximdva 3168 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 = 2) → (∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
| 124 | 123 | ex 412 |
. . . . . 6
⊢ (𝜑 → (𝑝 = 2 → (∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1)))) |
| 125 | 20, 124 | mpid 44 |
. . . . 5
⊢ (𝜑 → (𝑝 = 2 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
| 126 | 125 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 = 2 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
| 127 | 19, 126 | sylbid 240 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
| 128 | 127 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ (2↑𝑁) → ∃𝑥 ∈ ℤ (((𝑥↑(𝑃 − 1)) mod 𝑃) = 1 ∧ (((𝑥↑((𝑃 − 1) / 𝑝)) − 1) gcd 𝑃) = 1))) |
| 129 | 5, 6, 7, 13, 128 | pockthg 16944 |
1
⊢ (𝜑 → 𝑃 ∈ ℙ) |