| Step | Hyp | Ref
| Expression |
| 1 | | pockthg.4 |
. . 3
⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) |
| 2 | | pockthg.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℕ) |
| 3 | | pockthg.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℕ) |
| 4 | 2, 3 | nnmulcld 12319 |
. . . . . 6
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
| 5 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 6 | 4, 5 | eleqtrdi 2851 |
. . . . 5
⊢ (𝜑 → (𝐴 · 𝐵) ∈
(ℤ≥‘1)) |
| 7 | | eluzp1p1 12906 |
. . . . 5
⊢ ((𝐴 · 𝐵) ∈ (ℤ≥‘1)
→ ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) |
| 8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) |
| 9 | | df-2 12329 |
. . . . 5
⊢ 2 = (1 +
1) |
| 10 | 9 | fveq2i 6909 |
. . . 4
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
| 11 | 8, 10 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘2)) |
| 12 | 1, 11 | eqeltrd 2841 |
. 2
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
| 13 | | eluzelre 12889 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘2) → 𝑁 ∈ ℝ) |
| 14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝑁 ∈ ℝ) |
| 16 | 2 | nnred 12281 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 17 | 16 | resqcld 14165 |
. . . . . . . 8
⊢ (𝜑 → (𝐴↑2) ∈ ℝ) |
| 18 | 17 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝐴↑2) ∈ ℝ) |
| 19 | | prmnn 16711 |
. . . . . . . . . 10
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
| 20 | 19 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝑞 ∈ ℕ) |
| 21 | 20 | nnred 12281 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝑞 ∈ ℝ) |
| 22 | 21 | resqcld 14165 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝑞↑2) ∈ ℝ) |
| 23 | | pockthg.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 < 𝐴) |
| 24 | 3 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 25 | 2 | nngt0d 12315 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 < 𝐴) |
| 26 | | ltmul2 12118 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → (𝐵 < 𝐴 ↔ (𝐴 · 𝐵) < (𝐴 · 𝐴))) |
| 27 | 24, 16, 16, 25, 26 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 < 𝐴 ↔ (𝐴 · 𝐵) < (𝐴 · 𝐴))) |
| 28 | 23, 27 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 · 𝐵) < (𝐴 · 𝐴)) |
| 29 | 2, 2 | nnmulcld 12319 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐴) ∈ ℕ) |
| 30 | | nnltp1le 12674 |
. . . . . . . . . . 11
⊢ (((𝐴 · 𝐵) ∈ ℕ ∧ (𝐴 · 𝐴) ∈ ℕ) → ((𝐴 · 𝐵) < (𝐴 · 𝐴) ↔ ((𝐴 · 𝐵) + 1) ≤ (𝐴 · 𝐴))) |
| 31 | 4, 29, 30 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 · 𝐵) < (𝐴 · 𝐴) ↔ ((𝐴 · 𝐵) + 1) ≤ (𝐴 · 𝐴))) |
| 32 | 28, 31 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ≤ (𝐴 · 𝐴)) |
| 33 | 2 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 34 | 33 | sqvald 14183 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
| 35 | 32, 1, 34 | 3brtr4d 5175 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ≤ (𝐴↑2)) |
| 36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝑁 ≤ (𝐴↑2)) |
| 37 | | pockthg.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) |
| 39 | | prmnn 16711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 40 | 39 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → 𝑝 ∈ ℕ) |
| 41 | 40 | nncnd 12282 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → 𝑝 ∈ ℂ) |
| 42 | 41 | exp1d 14181 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → (𝑝↑1) = 𝑝) |
| 43 | | nnge1 12294 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 pCnt 𝐴) ∈ ℕ → 1 ≤ (𝑝 pCnt 𝐴)) |
| 44 | 43 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → 1 ≤ (𝑝 pCnt 𝐴)) |
| 45 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → 𝑝 ∈ ℙ) |
| 46 | 2 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ∈ ℤ) |
| 47 | 46 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → 𝐴 ∈ ℤ) |
| 48 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
| 49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → 1 ∈
ℕ0) |
| 50 | | pcdvdsb 16907 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 1 ∈
ℕ0) → (1 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝↑1) ∥ 𝐴)) |
| 51 | 45, 47, 49, 50 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → (1 ≤ (𝑝 pCnt 𝐴) ↔ (𝑝↑1) ∥ 𝐴)) |
| 52 | 44, 51 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → (𝑝↑1) ∥ 𝐴) |
| 53 | 42, 52 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → 𝑝 ∥ 𝐴) |
| 54 | | simpl1 1192 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝜑) |
| 55 | 54, 2 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝐴 ∈ ℕ) |
| 56 | 54, 3 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝐵 ∈ ℕ) |
| 57 | 54, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝐵 < 𝐴) |
| 58 | 54, 1 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝑁 = ((𝐴 · 𝐵) + 1)) |
| 59 | | simpl2l 1227 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝑞 ∈ ℙ) |
| 60 | | simpl2r 1228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝑞 ∥ 𝑁) |
| 61 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝑝 ∈ ℙ) |
| 62 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → (𝑝 pCnt 𝐴) ∈ ℕ) |
| 63 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → 𝑥 ∈ ℤ) |
| 64 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → ((𝑥↑(𝑁 − 1)) mod 𝑁) = 1) |
| 65 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1) |
| 66 | 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65 | pockthlem 16943 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) ∧ (𝑥 ∈ ℤ ∧ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1))) |
| 67 | 66 | rexlimdvaa 3156 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → (∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 68 | 67 | 3expa 1119 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → (∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 69 | 53, 68 | embantd 59 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ (𝑝 ∈ ℙ ∧ (𝑝 pCnt 𝐴) ∈ ℕ)) → ((𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 70 | 69 | expr 456 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐴) ∈ ℕ → ((𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1))))) |
| 71 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℙ) |
| 72 | | prmuz2 16733 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
(ℤ≥‘2)) |
| 73 | | uz2m1nn 12965 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈
(ℤ≥‘2) → (𝑞 − 1) ∈ ℕ) |
| 74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ∈ ℙ → (𝑞 − 1) ∈
ℕ) |
| 75 | 74 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝑞 − 1) ∈ ℕ) |
| 76 | | pccl 16887 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ∈ ℙ ∧ (𝑞 − 1) ∈ ℕ)
→ (𝑝 pCnt (𝑞 − 1)) ∈
ℕ0) |
| 77 | 71, 75, 76 | syl2anr 597 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt (𝑞 − 1)) ∈
ℕ0) |
| 78 | 77 | nn0ge0d 12590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → 0 ≤ (𝑝 pCnt (𝑞 − 1))) |
| 79 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 pCnt 𝐴) = 0 → ((𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)) ↔ 0 ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 80 | 78, 79 | syl5ibrcom 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐴) = 0 → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 81 | 80 | a1dd 50 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐴) = 0 → ((𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1))))) |
| 82 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → 𝑝 ∈ ℙ) |
| 83 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → 𝐴 ∈ ℕ) |
| 84 | 82, 83 | pccld 16888 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → (𝑝 pCnt 𝐴) ∈
ℕ0) |
| 85 | | elnn0 12528 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 pCnt 𝐴) ∈ ℕ0 ↔ ((𝑝 pCnt 𝐴) ∈ ℕ ∨ (𝑝 pCnt 𝐴) = 0)) |
| 86 | 84, 85 | sylib 218 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → ((𝑝 pCnt 𝐴) ∈ ℕ ∨ (𝑝 pCnt 𝐴) = 0)) |
| 87 | 70, 81, 86 | mpjaod 861 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) ∧ 𝑝 ∈ ℙ) → ((𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1)) → (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 88 | 87 | ralimdva 3167 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1)) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 89 | 38, 88 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1))) |
| 90 | 75 | nnzd 12640 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝑞 − 1) ∈ ℤ) |
| 91 | | pc2dvds 16917 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ (𝑞 − 1) ∈ ℤ)
→ (𝐴 ∥ (𝑞 − 1) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 92 | 46, 90, 91 | syl2an2r 685 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝐴 ∥ (𝑞 − 1) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt (𝑞 − 1)))) |
| 93 | 89, 92 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝐴 ∥ (𝑞 − 1)) |
| 94 | | dvdsle 16347 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℤ ∧ (𝑞 − 1) ∈ ℕ)
→ (𝐴 ∥ (𝑞 − 1) → 𝐴 ≤ (𝑞 − 1))) |
| 95 | 46, 75, 94 | syl2an2r 685 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝐴 ∥ (𝑞 − 1) → 𝐴 ≤ (𝑞 − 1))) |
| 96 | 93, 95 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝐴 ≤ (𝑞 − 1)) |
| 97 | 2 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℕ0) |
| 98 | 20 | nnnn0d 12587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝑞 ∈ ℕ0) |
| 99 | | nn0ltlem1 12678 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑞 ∈
ℕ0) → (𝐴 < 𝑞 ↔ 𝐴 ≤ (𝑞 − 1))) |
| 100 | 97, 98, 99 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝐴 < 𝑞 ↔ 𝐴 ≤ (𝑞 − 1))) |
| 101 | 96, 100 | mpbird 257 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝐴 < 𝑞) |
| 102 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝐴 ∈ ℝ) |
| 103 | 97 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐴) |
| 104 | 103 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 0 ≤ 𝐴) |
| 105 | 98 | nn0ge0d 12590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 0 ≤ 𝑞) |
| 106 | 102, 21, 104, 105 | lt2sqd 14295 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝐴 < 𝑞 ↔ (𝐴↑2) < (𝑞↑2))) |
| 107 | 101, 106 | mpbid 232 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝐴↑2) < (𝑞↑2)) |
| 108 | 15, 18, 22, 36, 107 | lelttrd 11419 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → 𝑁 < (𝑞↑2)) |
| 109 | 15, 22 | ltnled 11408 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → (𝑁 < (𝑞↑2) ↔ ¬ (𝑞↑2) ≤ 𝑁)) |
| 110 | 108, 109 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑁)) → ¬ (𝑞↑2) ≤ 𝑁) |
| 111 | 110 | expr 456 |
. . . 4
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → (𝑞 ∥ 𝑁 → ¬ (𝑞↑2) ≤ 𝑁)) |
| 112 | 111 | con2d 134 |
. . 3
⊢ ((𝜑 ∧ 𝑞 ∈ ℙ) → ((𝑞↑2) ≤ 𝑁 → ¬ 𝑞 ∥ 𝑁)) |
| 113 | 112 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑞 ∈ ℙ ((𝑞↑2) ≤ 𝑁 → ¬ 𝑞 ∥ 𝑁)) |
| 114 | | isprm5 16744 |
. 2
⊢ (𝑁 ∈ ℙ ↔ (𝑁 ∈
(ℤ≥‘2) ∧ ∀𝑞 ∈ ℙ ((𝑞↑2) ≤ 𝑁 → ¬ 𝑞 ∥ 𝑁))) |
| 115 | 12, 113, 114 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑁 ∈ ℙ) |