Proof of Theorem pockthlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pockthlem.7 | . . . . . 6
⊢ (𝜑 → 𝑄 ∈ ℙ) | 
| 2 |  | prmnn 16711 | . . . . . 6
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) | 
| 3 | 1, 2 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑄 ∈ ℕ) | 
| 4 |  | pockthlem.8 | . . . . . 6
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) | 
| 5 | 4 | nnnn0d 12587 | . . . . 5
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈
ℕ0) | 
| 6 | 3, 5 | nnexpcld 14284 | . . . 4
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ) | 
| 7 | 6 | nnzd 12640 | . . 3
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ) | 
| 8 |  | pockthlem.5 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 9 |  | prmnn 16711 | . . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 10 | 8, 9 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 11 |  | pockthlem.9 | . . . . 5
⊢ (𝜑 → 𝐶 ∈ ℤ) | 
| 12 | 10 | nnzd 12640 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 13 |  | gcddvds 16540 | . . . . . . . . . 10
⊢ ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃)) | 
| 14 | 11, 12, 13 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃)) | 
| 15 | 14 | simpld 494 | . . . . . . . 8
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶) | 
| 16 | 11, 12 | gcdcld 16545 | . . . . . . . . . 10
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈
ℕ0) | 
| 17 | 16 | nn0zd 12639 | . . . . . . . . 9
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ) | 
| 18 |  | pockthg.4 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) | 
| 19 |  | pockthg.1 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℕ) | 
| 20 |  | pockthg.2 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ℕ) | 
| 21 | 19, 20 | nnmulcld 12319 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) | 
| 22 |  | nnuz 12921 | . . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) | 
| 23 | 21, 22 | eleqtrdi 2851 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 · 𝐵) ∈
(ℤ≥‘1)) | 
| 24 |  | eluzp1p1 12906 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 · 𝐵) ∈ (ℤ≥‘1)
→ ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) | 
| 26 | 18, 25 | eqeltrd 2841 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(1 +
1))) | 
| 27 |  | df-2 12329 | . . . . . . . . . . . . . 14
⊢ 2 = (1 +
1) | 
| 28 | 27 | fveq2i 6909 | . . . . . . . . . . . . 13
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) | 
| 29 | 26, 28 | eleqtrrdi 2852 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) | 
| 30 |  | eluz2b2 12963 | . . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) | 
| 31 | 29, 30 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) | 
| 32 | 31 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 33 | 32 | nnzd 12640 | . . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 34 | 14 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃) | 
| 35 |  | pockthlem.6 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ∥ 𝑁) | 
| 36 | 17, 12, 33, 34, 35 | dvdstrd 16332 | . . . . . . . 8
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁) | 
| 37 | 32 | nnne0d 12316 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ≠ 0) | 
| 38 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) | 
| 39 | 38 | necon3ai 2965 | . . . . . . . . . 10
⊢ (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0)) | 
| 40 | 37, 39 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0)) | 
| 41 |  | dvdslegcd 16541 | . . . . . . . . 9
⊢ ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))) | 
| 42 | 17, 11, 33, 40, 41 | syl31anc 1375 | . . . . . . . 8
⊢ (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))) | 
| 43 | 15, 36, 42 | mp2and 699 | . . . . . . 7
⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)) | 
| 44 |  | pockthlem.10 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) | 
| 45 | 44 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁)) | 
| 46 |  | 1z 12647 | . . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ | 
| 47 |  | eluzp1m1 12904 | . . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝑁
∈ (ℤ≥‘(1 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘1)) | 
| 48 | 46, 26, 47 | sylancr 587 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘1)) | 
| 49 | 48, 22 | eleqtrrdi 2852 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) | 
| 50 | 49 | nnnn0d 12587 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) | 
| 51 |  | zexpcl 14117 | . . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈
ℕ0) → (𝐶↑(𝑁 − 1)) ∈
ℤ) | 
| 52 | 11, 50, 51 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈
ℤ) | 
| 53 |  | modgcd 16569 | . . . . . . . . . 10
⊢ (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁)) | 
| 54 | 52, 32, 53 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁)) | 
| 55 |  | gcdcom 16550 | . . . . . . . . . . 11
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1)) | 
| 56 | 46, 33, 55 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1)) | 
| 57 |  | gcd1 16565 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1) | 
| 58 | 33, 57 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁 gcd 1) = 1) | 
| 59 | 56, 58 | eqtrd 2777 | . . . . . . . . 9
⊢ (𝜑 → (1 gcd 𝑁) = 1) | 
| 60 | 45, 54, 59 | 3eqtr3d 2785 | . . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1) | 
| 61 |  | rpexp 16759 | . . . . . . . . 9
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ)
→ (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1)) | 
| 62 | 11, 33, 49, 61 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1)) | 
| 63 | 60, 62 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → (𝐶 gcd 𝑁) = 1) | 
| 64 | 43, 63 | breqtrd 5169 | . . . . . 6
⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ 1) | 
| 65 | 10 | nnne0d 12316 | . . . . . . . . 9
⊢ (𝜑 → 𝑃 ≠ 0) | 
| 66 |  | simpr 484 | . . . . . . . . . 10
⊢ ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0) | 
| 67 | 66 | necon3ai 2965 | . . . . . . . . 9
⊢ (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0)) | 
| 68 | 65, 67 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0)) | 
| 69 |  | gcdn0cl 16539 | . . . . . . . 8
⊢ (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬
(𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ) | 
| 70 | 11, 12, 68, 69 | syl21anc 838 | . . . . . . 7
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ) | 
| 71 |  | nnle1eq1 12296 | . . . . . . 7
⊢ ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1)) | 
| 72 | 70, 71 | syl 17 | . . . . . 6
⊢ (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1)) | 
| 73 | 64, 72 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝐶 gcd 𝑃) = 1) | 
| 74 |  | odzcl 16831 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) →
((odℤ‘𝑃)‘𝐶) ∈ ℕ) | 
| 75 | 10, 11, 73, 74 | syl3anc 1373 | . . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∈ ℕ) | 
| 76 | 75 | nnzd 12640 | . . 3
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∈ ℤ) | 
| 77 |  | prmuz2 16733 | . . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 78 | 8, 77 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) | 
| 79 | 78, 28 | eleqtrdi 2851 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(1 +
1))) | 
| 80 |  | eluzp1m1 12904 | . . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑃
∈ (ℤ≥‘(1 + 1))) → (𝑃 − 1) ∈
(ℤ≥‘1)) | 
| 81 | 46, 79, 80 | sylancr 587 | . . . . 5
⊢ (𝜑 → (𝑃 − 1) ∈
(ℤ≥‘1)) | 
| 82 | 81, 22 | eleqtrrdi 2852 | . . . 4
⊢ (𝜑 → (𝑃 − 1) ∈ ℕ) | 
| 83 | 82 | nnzd 12640 | . . 3
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) | 
| 84 | 19 | nnzd 12640 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 85 | 49 | nnzd 12640 | . . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) | 
| 86 |  | pcdvds 16902 | . . . . . . 7
⊢ ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴) | 
| 87 | 1, 19, 86 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴) | 
| 88 | 20 | nnzd 12640 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 89 |  | dvdsmul1 16315 | . . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵)) | 
| 90 | 84, 88, 89 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∥ (𝐴 · 𝐵)) | 
| 91 | 18 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1)) | 
| 92 | 21 | nncnd 12282 | . . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) | 
| 93 |  | ax-1cn 11213 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 94 |  | pncan 11514 | . . . . . . . . 9
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵)) | 
| 95 | 92, 93, 94 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵)) | 
| 96 | 91, 95 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵)) | 
| 97 | 90, 96 | breqtrrd 5171 | . . . . . 6
⊢ (𝜑 → 𝐴 ∥ (𝑁 − 1)) | 
| 98 | 7, 84, 85, 87, 97 | dvdstrd 16332 | . . . . 5
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) | 
| 99 | 6 | nnne0d 12316 | . . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0) | 
| 100 |  | dvdsval2 16293 | . . . . . 6
⊢ (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)) | 
| 101 | 7, 99, 85, 100 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)) | 
| 102 | 98, 101 | mpbid 232 | . . . 4
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ) | 
| 103 |  | peano2zm 12660 | . . . . . . . 8
⊢ ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈
ℤ) | 
| 104 | 52, 103 | syl 17 | . . . . . . 7
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈
ℤ) | 
| 105 | 32 | nnred 12281 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 106 | 31 | simprd 495 | . . . . . . . . . 10
⊢ (𝜑 → 1 < 𝑁) | 
| 107 |  | 1mod 13943 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) | 
| 108 | 105, 106,
107 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (1 mod 𝑁) = 1) | 
| 109 | 44, 108 | eqtr4d 2780 | . . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)) | 
| 110 |  | 1zzd 12648 | . . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) | 
| 111 |  | moddvds 16301 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))) | 
| 112 | 32, 52, 110, 111 | syl3anc 1373 | . . . . . . . 8
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))) | 
| 113 | 109, 112 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) | 
| 114 | 12, 33, 104, 35, 113 | dvdstrd 16332 | . . . . . 6
⊢ (𝜑 → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1)) | 
| 115 |  | odzdvds 16833 | . . . . . . 7
⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ0)
→ (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))) | 
| 116 | 10, 11, 73, 50, 115 | syl31anc 1375 | . . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))) | 
| 117 | 114, 116 | mpbid 232 | . . . . 5
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1)) | 
| 118 | 49 | nncnd 12282 | . . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) | 
| 119 | 6 | nncnd 12282 | . . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ) | 
| 120 | 118, 119,
99 | divcan1d 12044 | . . . . 5
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1)) | 
| 121 | 117, 120 | breqtrrd 5171 | . . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴)))) | 
| 122 |  | nprmdvds1 16743 | . . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ∥
1) | 
| 123 | 8, 122 | syl 17 | . . . . 5
⊢ (𝜑 → ¬ 𝑃 ∥ 1) | 
| 124 | 3 | nnzd 12640 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ ℤ) | 
| 125 |  | iddvdsexp 16317 | . . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴))) | 
| 126 | 124, 4, 125 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴))) | 
| 127 | 124, 7, 85, 126, 98 | dvdstrd 16332 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∥ (𝑁 − 1)) | 
| 128 | 3 | nnne0d 12316 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ≠ 0) | 
| 129 |  | dvdsval2 16293 | . . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ)) | 
| 130 | 124, 128,
85, 129 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ)) | 
| 131 | 127, 130 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ) | 
| 132 | 50 | nn0ge0d 12590 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁 − 1)) | 
| 133 | 49 | nnred 12281 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) | 
| 134 | 3 | nnred 12281 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ ℝ) | 
| 135 | 3 | nngt0d 12315 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝑄) | 
| 136 |  | ge0div 12135 | . . . . . . . . . . . . 13
⊢ (((𝑁 − 1) ∈ ℝ ∧
𝑄 ∈ ℝ ∧ 0
< 𝑄) → (0 ≤
(𝑁 − 1) ↔ 0 ≤
((𝑁 − 1) / 𝑄))) | 
| 137 | 133, 134,
135, 136 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄))) | 
| 138 | 132, 137 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄)) | 
| 139 |  | elnn0z 12626 | . . . . . . . . . . 11
⊢ (((𝑁 − 1) / 𝑄) ∈ ℕ0 ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄))) | 
| 140 | 131, 138,
139 | sylanbrc 583 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈
ℕ0) | 
| 141 |  | zexpcl 14117 | . . . . . . . . . 10
⊢ ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ) | 
| 142 | 11, 140, 141 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ) | 
| 143 |  | peano2zm 12660 | . . . . . . . . 9
⊢ ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈
ℤ) | 
| 144 | 142, 143 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈
ℤ) | 
| 145 |  | dvdsgcd 16581 | . . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) | 
| 146 | 12, 144, 33, 145 | syl3anc 1373 | . . . . . . 7
⊢ (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) | 
| 147 | 35, 146 | mpan2d 694 | . . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) | 
| 148 |  | odzdvds 16833 | . . . . . . . 8
⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) | 
| 149 | 10, 11, 73, 140, 148 | syl31anc 1375 | . . . . . . 7
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) | 
| 150 | 3 | nncnd 12282 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℂ) | 
| 151 | 4 | nnzd 12640 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ) | 
| 152 | 150, 128,
151 | expm1d 14196 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)) | 
| 153 | 152 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))) | 
| 154 | 133, 6 | nndivred 12320 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ) | 
| 155 | 154 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ) | 
| 156 | 155, 119,
150, 128 | divassd 12078 | . . . . . . . . 9
⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))) | 
| 157 | 120 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄)) | 
| 158 | 153, 156,
157 | 3eqtr2d 2783 | . . . . . . . 8
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄)) | 
| 159 | 158 | breq2d 5155 | . . . . . . 7
⊢ (𝜑 →
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) | 
| 160 | 149, 159 | bitr4d 282 | . . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) | 
| 161 |  | pockthlem.11 | . . . . . . 7
⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) | 
| 162 | 161 | breq2d 5155 | . . . . . 6
⊢ (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1)) | 
| 163 | 147, 160,
162 | 3imtr3d 293 | . . . . 5
⊢ (𝜑 →
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1)) | 
| 164 | 123, 163 | mtod 198 | . . . 4
⊢ (𝜑 → ¬
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))) | 
| 165 |  | prmpwdvds 16942 | . . . 4
⊢
(((((𝑁 − 1) /
(𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧
((odℤ‘𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶)) | 
| 166 | 102, 76, 1, 4, 121, 164, 165 | syl222anc 1388 | . . 3
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶)) | 
| 167 |  | odzphi 16834 | . . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) →
((odℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃)) | 
| 168 | 10, 11, 73, 167 | syl3anc 1373 | . . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃)) | 
| 169 |  | phiprm 16814 | . . . . 5
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) | 
| 170 | 8, 169 | syl 17 | . . . 4
⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1)) | 
| 171 | 168, 170 | breqtrd 5169 | . . 3
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (𝑃 − 1)) | 
| 172 | 7, 76, 83, 166, 171 | dvdstrd 16332 | . 2
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)) | 
| 173 |  | pcdvdsb 16907 | . . 3
⊢ ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧
(𝑄 pCnt 𝐴) ∈ ℕ0) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) | 
| 174 | 1, 83, 5, 173 | syl3anc 1373 | . 2
⊢ (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) | 
| 175 | 172, 174 | mpbird 257 | 1
⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) |