| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks4d1p8d2.3 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 2 |  | prmnn 16712 | . . . . 5
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 3 | 1, 2 | syl 17 | . . . 4
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 4 | 3 | nnred 12282 | . . 3
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 5 |  | aks4d1p8d2.1 | . . . 4
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 6 | 1, 5 | pccld 16889 | . . 3
⊢ (𝜑 → (𝑃 pCnt 𝑅) ∈
ℕ0) | 
| 7 | 4, 6 | reexpcld 14204 | . 2
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℝ) | 
| 8 |  | aks4d1p8d2.4 | . . . . 5
⊢ (𝜑 → 𝑄 ∈ ℙ) | 
| 9 |  | prmnn 16712 | . . . . 5
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) | 
| 10 | 8, 9 | syl 17 | . . . 4
⊢ (𝜑 → 𝑄 ∈ ℕ) | 
| 11 | 10 | nnred 12282 | . . 3
⊢ (𝜑 → 𝑄 ∈ ℝ) | 
| 12 | 7, 11 | remulcld 11292 | . 2
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ∈ ℝ) | 
| 13 | 5 | nnred 12282 | . 2
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 14 | 7 | recnd 11290 | . . . 4
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℂ) | 
| 15 | 14 | mulridd 11279 | . . 3
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) · 1) = (𝑃↑(𝑃 pCnt 𝑅))) | 
| 16 |  | 1red 11263 | . . . 4
⊢ (𝜑 → 1 ∈
ℝ) | 
| 17 | 3 | nnrpd 13076 | . . . . 5
⊢ (𝜑 → 𝑃 ∈
ℝ+) | 
| 18 | 6 | nn0zd 12641 | . . . . 5
⊢ (𝜑 → (𝑃 pCnt 𝑅) ∈ ℤ) | 
| 19 | 17, 18 | rpexpcld 14287 | . . . 4
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∈
ℝ+) | 
| 20 |  | prmgt1 16735 | . . . . 5
⊢ (𝑄 ∈ ℙ → 1 <
𝑄) | 
| 21 | 8, 20 | syl 17 | . . . 4
⊢ (𝜑 → 1 < 𝑄) | 
| 22 | 16, 11, 19, 21 | ltmul2dd 13134 | . . 3
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) · 1) < ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄)) | 
| 23 | 15, 22 | eqbrtrrd 5166 | . 2
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) < ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄)) | 
| 24 | 3 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 25 | 24, 6 | zexpcld 14129 | . . . 4
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ) | 
| 26 | 10 | nnzd 12642 | . . . 4
⊢ (𝜑 → 𝑄 ∈ ℤ) | 
| 27 | 5 | nnzd 12642 | . . . 4
⊢ (𝜑 → 𝑅 ∈ ℤ) | 
| 28 | 25, 26 | gcdcomd 16552 | . . . . 5
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) gcd 𝑄) = (𝑄 gcd (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 29 |  | 0lt1 11786 | . . . . . . . . . . . . . 14
⊢ 0 <
1 | 
| 30 | 29 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 1) | 
| 31 |  | 0red 11265 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈
ℝ) | 
| 32 | 31, 16 | ltnled 11409 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0 < 1 ↔ ¬ 1
≤ 0)) | 
| 33 | 30, 32 | mpbid 232 | . . . . . . . . . . . 12
⊢ (𝜑 → ¬ 1 ≤
0) | 
| 34 | 11 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑄 ∈ ℂ) | 
| 35 | 34 | exp1d 14182 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑄↑1) = 𝑄) | 
| 36 | 35 | eqcomd 2742 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑄 = (𝑄↑1)) | 
| 37 | 36 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 pCnt 𝑄) = (𝑄 pCnt (𝑄↑1))) | 
| 38 |  | 1zzd 12650 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℤ) | 
| 39 |  | pcid 16912 | . . . . . . . . . . . . . . . 16
⊢ ((𝑄 ∈ ℙ ∧ 1 ∈
ℤ) → (𝑄 pCnt
(𝑄↑1)) =
1) | 
| 40 | 8, 38, 39 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑄 pCnt (𝑄↑1)) = 1) | 
| 41 | 37, 40 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄 pCnt 𝑄) = 1) | 
| 42 |  | aks4d1p8d2.8 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑄 ∥ 𝑁) | 
| 43 | 42 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → 𝑄 ∥ 𝑁) | 
| 44 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 = 𝑄 → (𝑃 ∥ 𝑁 ↔ 𝑄 ∥ 𝑁)) | 
| 45 | 44 | adantl 481 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (𝑃 ∥ 𝑁 ↔ 𝑄 ∥ 𝑁)) | 
| 46 | 45 | bicomd 223 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (𝑄 ∥ 𝑁 ↔ 𝑃 ∥ 𝑁)) | 
| 47 | 46 | biimpd 229 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → (𝑄 ∥ 𝑁 → 𝑃 ∥ 𝑁)) | 
| 48 | 43, 47 | mpd 15 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → 𝑃 ∥ 𝑁) | 
| 49 |  | aks4d1p8d2.7 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ 𝑃 ∥ 𝑁) | 
| 50 | 49 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑃 = 𝑄) → ¬ 𝑃 ∥ 𝑁) | 
| 51 | 48, 50 | pm2.65da 816 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ 𝑃 = 𝑄) | 
| 52 | 51 | neqcomd 2746 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ 𝑄 = 𝑃) | 
| 53 |  | aks4d1p8d2.5 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑃 ∥ 𝑅) | 
| 54 |  | pcelnn 16909 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℕ) → ((𝑃 pCnt 𝑅) ∈ ℕ ↔ 𝑃 ∥ 𝑅)) | 
| 55 | 1, 5, 54 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑃 pCnt 𝑅) ∈ ℕ ↔ 𝑃 ∥ 𝑅)) | 
| 56 | 53, 55 | mpbird 257 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 pCnt 𝑅) ∈ ℕ) | 
| 57 |  | prmdvdsexpb 16754 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑄 ∈ ℙ ∧ 𝑃 ∈ ℙ ∧ (𝑃 pCnt 𝑅) ∈ ℕ) → (𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ 𝑄 = 𝑃)) | 
| 58 | 8, 1, 56, 57 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ 𝑄 = 𝑃)) | 
| 59 | 58 | notbid 318 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ ¬ 𝑄 = 𝑃)) | 
| 60 | 52, 59 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅))) | 
| 61 | 3, 6 | nnexpcld 14285 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℕ) | 
| 62 |  | pceq0 16910 | . . . . . . . . . . . . . . . 16
⊢ ((𝑄 ∈ ℙ ∧ (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℕ) → ((𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅))) = 0 ↔ ¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 63 | 8, 61, 62 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅))) = 0 ↔ ¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 64 | 60, 63 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅))) = 0) | 
| 65 | 41, 64 | breq12d 5155 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄 pCnt 𝑄) ≤ (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅))) ↔ 1 ≤ 0)) | 
| 66 | 65 | notbid 318 | . . . . . . . . . . . 12
⊢ (𝜑 → (¬ (𝑄 pCnt 𝑄) ≤ (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅))) ↔ ¬ 1 ≤ 0)) | 
| 67 | 33, 66 | mpbird 257 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ (𝑄 pCnt 𝑄) ≤ (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 68 | 67 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 = 𝑄) → ¬ (𝑄 pCnt 𝑄) ≤ (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 69 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 = 𝑄) → 𝑝 = 𝑄) | 
| 70 | 69 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 = 𝑄) → (𝑝 pCnt 𝑄) = (𝑄 pCnt 𝑄)) | 
| 71 | 69 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 = 𝑄) → (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))) = (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 72 | 70, 71 | breq12d 5155 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 = 𝑄) → ((𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))) ↔ (𝑄 pCnt 𝑄) ≤ (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅))))) | 
| 73 | 72 | notbid 318 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 = 𝑄) → (¬ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))) ↔ ¬ (𝑄 pCnt 𝑄) ≤ (𝑄 pCnt (𝑃↑(𝑃 pCnt 𝑅))))) | 
| 74 | 68, 73 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 = 𝑄) → ¬ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 75 | 74, 8 | rspcime 3626 | . . . . . . . 8
⊢ (𝜑 → ∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 76 |  | rexnal 3099 | . . . . . . . . 9
⊢
(∃𝑝 ∈
ℙ ¬ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))) ↔ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 77 | 76 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (∃𝑝 ∈ ℙ ¬ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))) ↔ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))))) | 
| 78 | 75, 77 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅)))) | 
| 79 |  | pc2dvds 16918 | . . . . . . . . 9
⊢ ((𝑄 ∈ ℤ ∧ (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ) → (𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))))) | 
| 80 | 26, 25, 79 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))))) | 
| 81 | 80 | notbid 318 | . . . . . . 7
⊢ (𝜑 → (¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ ¬ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝑄) ≤ (𝑝 pCnt (𝑃↑(𝑃 pCnt 𝑅))))) | 
| 82 | 78, 81 | mpbird 257 | . . . . . 6
⊢ (𝜑 → ¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅))) | 
| 83 |  | coprm 16749 | . . . . . . 7
⊢ ((𝑄 ∈ ℙ ∧ (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ) → (¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ (𝑄 gcd (𝑃↑(𝑃 pCnt 𝑅))) = 1)) | 
| 84 | 8, 25, 83 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (¬ 𝑄 ∥ (𝑃↑(𝑃 pCnt 𝑅)) ↔ (𝑄 gcd (𝑃↑(𝑃 pCnt 𝑅))) = 1)) | 
| 85 | 82, 84 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝑄 gcd (𝑃↑(𝑃 pCnt 𝑅))) = 1) | 
| 86 | 28, 85 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) gcd 𝑄) = 1) | 
| 87 |  | pcdvds 16903 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅) | 
| 88 | 1, 5, 87 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅) | 
| 89 |  | aks4d1p8d2.6 | . . . 4
⊢ (𝜑 → 𝑄 ∥ 𝑅) | 
| 90 | 25, 26, 27, 86, 88, 89 | coprmdvds2d 42003 | . . 3
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ∥ 𝑅) | 
| 91 | 25, 26 | zmulcld 12730 | . . . 4
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ∈ ℤ) | 
| 92 |  | dvdsle 16348 | . . . 4
⊢ ((((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ∈ ℤ ∧ 𝑅 ∈ ℕ) → (((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ∥ 𝑅 → ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ≤ 𝑅)) | 
| 93 | 91, 5, 92 | syl2anc 584 | . . 3
⊢ (𝜑 → (((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ∥ 𝑅 → ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ≤ 𝑅)) | 
| 94 | 90, 93 | mpd 15 | . 2
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) · 𝑄) ≤ 𝑅) | 
| 95 | 7, 12, 13, 23, 94 | ltletrd 11422 | 1
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) < 𝑅) |