Proof of Theorem aks4d1p6
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks4d1p6.7 | . . . . . . 7
⊢ 𝐾 = (𝑃 pCnt 𝑅) | 
| 2 | 1 | a1i 11 | . . . . . 6
⊢ (𝜑 → 𝐾 = (𝑃 pCnt 𝑅)) | 
| 3 |  | aks4d1p6.5 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 4 |  | aks4d1p6.1 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) | 
| 5 |  | aks4d1p6.2 | . . . . . . . . . 10
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) | 
| 6 |  | aks4d1p6.3 | . . . . . . . . . 10
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) | 
| 7 |  | aks4d1p6.4 | . . . . . . . . . 10
⊢ 𝑅 = inf({𝑟 ∈ (1...𝐵) ∣ ¬ 𝑟 ∥ 𝐴}, ℝ, < ) | 
| 8 | 4, 5, 6, 7 | aks4d1p4 42080 | . . . . . . . . 9
⊢ (𝜑 → (𝑅 ∈ (1...𝐵) ∧ ¬ 𝑅 ∥ 𝐴)) | 
| 9 | 8 | simpld 494 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ (1...𝐵)) | 
| 10 |  | elfznn 13593 | . . . . . . . 8
⊢ (𝑅 ∈ (1...𝐵) → 𝑅 ∈ ℕ) | 
| 11 | 9, 10 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 12 | 3, 11 | pccld 16888 | . . . . . 6
⊢ (𝜑 → (𝑃 pCnt 𝑅) ∈
ℕ0) | 
| 13 | 2, 12 | eqeltrd 2841 | . . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) | 
| 14 | 13 | nn0zd 12639 | . . . 4
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 15 | 14 | zred 12722 | . . 3
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 16 |  | prmnn 16711 | . . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 17 | 3, 16 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 18 | 17 | nnred 12281 | . . . 4
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 19 | 17 | nngt0d 12315 | . . . 4
⊢ (𝜑 → 0 < 𝑃) | 
| 20 | 6 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) | 
| 21 |  | 2re 12340 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 22 | 21 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℝ) | 
| 23 |  | 2pos 12369 | . . . . . . . . . . . 12
⊢ 0 <
2 | 
| 24 | 23 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < 2) | 
| 25 |  | eluzelz 12888 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) | 
| 26 | 4, 25 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 27 | 26 | zred 12722 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 28 |  | 0red 11264 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℝ) | 
| 29 |  | 3re 12346 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℝ | 
| 30 | 29 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ∈
ℝ) | 
| 31 |  | 3pos 12371 | . . . . . . . . . . . . 13
⊢ 0 <
3 | 
| 32 | 31 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < 3) | 
| 33 |  | eluzle 12891 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) | 
| 34 | 4, 33 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ≤ 𝑁) | 
| 35 | 28, 30, 27, 32, 34 | ltletrd 11421 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝑁) | 
| 36 |  | 1red 11262 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈
ℝ) | 
| 37 |  | 1lt2 12437 | . . . . . . . . . . . . . 14
⊢ 1 <
2 | 
| 38 | 37 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 2) | 
| 39 | 36, 38 | ltned 11397 | . . . . . . . . . . . 12
⊢ (𝜑 → 1 ≠ 2) | 
| 40 | 39 | necomd 2996 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ≠ 1) | 
| 41 | 22, 24, 27, 35, 40 | relogbcld 41974 | . . . . . . . . . 10
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) | 
| 42 |  | 5nn0 12546 | . . . . . . . . . . 11
⊢ 5 ∈
ℕ0 | 
| 43 | 42 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 5 ∈
ℕ0) | 
| 44 | 41, 43 | reexpcld 14203 | . . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) | 
| 45 |  | ceilcl 13882 | . . . . . . . . 9
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ) | 
| 46 | 44, 45 | syl 17 | . . . . . . . 8
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) | 
| 47 | 20, 46 | eqeltrd 2841 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 48 | 47 | zred 12722 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 49 |  | 9re 12365 | . . . . . . . . . 10
⊢ 9 ∈
ℝ | 
| 50 | 49 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 9 ∈
ℝ) | 
| 51 |  | 9pos 12379 | . . . . . . . . . 10
⊢ 0 <
9 | 
| 52 | 51 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 0 < 9) | 
| 53 | 27, 34 | 3lexlogpow5ineq4 42057 | . . . . . . . . 9
⊢ (𝜑 → 9 < ((2 logb
𝑁)↑5)) | 
| 54 | 28, 50, 44, 52, 53 | lttrd 11422 | . . . . . . . 8
⊢ (𝜑 → 0 < ((2 logb
𝑁)↑5)) | 
| 55 |  | ceilge 13885 | . . . . . . . . . 10
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2
logb 𝑁)↑5))) | 
| 56 | 44, 55 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤
(⌈‘((2 logb 𝑁)↑5))) | 
| 57 | 56, 20 | breqtrrd 5171 | . . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤ 𝐵) | 
| 58 | 28, 44, 48, 54, 57 | ltletrd 11421 | . . . . . . 7
⊢ (𝜑 → 0 < 𝐵) | 
| 59 | 47, 58 | jca 511 | . . . . . 6
⊢ (𝜑 → (𝐵 ∈ ℤ ∧ 0 < 𝐵)) | 
| 60 |  | elnnz 12623 | . . . . . 6
⊢ (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℤ ∧ 0 <
𝐵)) | 
| 61 | 59, 60 | sylibr 234 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ ℕ) | 
| 62 | 61 | nnred 12281 | . . . 4
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 63 | 61 | nngt0d 12315 | . . . 4
⊢ (𝜑 → 0 < 𝐵) | 
| 64 |  | 2z 12649 | . . . . . . . . 9
⊢ 2 ∈
ℤ | 
| 65 | 64 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) | 
| 66 | 65 | zred 12722 | . . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) | 
| 67 |  | prmuz2 16733 | . . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) | 
| 68 | 3, 67 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) | 
| 69 |  | eluzle 12891 | . . . . . . . 8
⊢ (𝑃 ∈
(ℤ≥‘2) → 2 ≤ 𝑃) | 
| 70 | 68, 69 | syl 17 | . . . . . . 7
⊢ (𝜑 → 2 ≤ 𝑃) | 
| 71 | 36, 66, 18, 38, 70 | ltletrd 11421 | . . . . . 6
⊢ (𝜑 → 1 < 𝑃) | 
| 72 | 36, 71 | ltned 11397 | . . . . 5
⊢ (𝜑 → 1 ≠ 𝑃) | 
| 73 | 72 | necomd 2996 | . . . 4
⊢ (𝜑 → 𝑃 ≠ 1) | 
| 74 | 18, 19, 62, 63, 73 | relogbcld 41974 | . . 3
⊢ (𝜑 → (𝑃 logb 𝐵) ∈ ℝ) | 
| 75 | 66, 24, 62, 63, 40 | relogbcld 41974 | . . 3
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) | 
| 76 | 17 | nnrpd 13075 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℝ+) | 
| 77 | 76 | rpcnd 13079 | . . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 78 | 76 | rpne0d 13082 | . . . . . 6
⊢ (𝜑 → 𝑃 ≠ 0) | 
| 79 | 77, 78, 14 | cxpexpzd 26753 | . . . . 5
⊢ (𝜑 → (𝑃↑𝑐𝐾) = (𝑃↑𝐾)) | 
| 80 | 18, 13 | reexpcld 14203 | . . . . . . 7
⊢ (𝜑 → (𝑃↑𝐾) ∈ ℝ) | 
| 81 | 11 | nnred 12281 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 82 | 2 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → (𝑃↑𝐾) = (𝑃↑(𝑃 pCnt 𝑅))) | 
| 83 |  | pcdvds 16902 | . . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅) | 
| 84 | 3, 11, 83 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅) | 
| 85 | 17 | nnzd 12640 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 86 |  | zexpcl 14117 | . . . . . . . . . . 11
⊢ ((𝑃 ∈ ℤ ∧ (𝑃 pCnt 𝑅) ∈ ℕ0) → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ) | 
| 87 | 85, 12, 86 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ) | 
| 88 |  | dvdsle 16347 | . . . . . . . . . 10
⊢ (((𝑃↑(𝑃 pCnt 𝑅)) ∈ ℤ ∧ 𝑅 ∈ ℕ) → ((𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅 → (𝑃↑(𝑃 pCnt 𝑅)) ≤ 𝑅)) | 
| 89 | 87, 11, 88 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → ((𝑃↑(𝑃 pCnt 𝑅)) ∥ 𝑅 → (𝑃↑(𝑃 pCnt 𝑅)) ≤ 𝑅)) | 
| 90 | 84, 89 | mpd 15 | . . . . . . . 8
⊢ (𝜑 → (𝑃↑(𝑃 pCnt 𝑅)) ≤ 𝑅) | 
| 91 | 82, 90 | eqbrtrd 5165 | . . . . . . 7
⊢ (𝜑 → (𝑃↑𝐾) ≤ 𝑅) | 
| 92 |  | elfzle2 13568 | . . . . . . . 8
⊢ (𝑅 ∈ (1...𝐵) → 𝑅 ≤ 𝐵) | 
| 93 | 9, 92 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ≤ 𝐵) | 
| 94 | 80, 81, 62, 91, 93 | letrd 11418 | . . . . . 6
⊢ (𝜑 → (𝑃↑𝐾) ≤ 𝐵) | 
| 95 | 78, 73 | nelprd 4657 | . . . . . . . 8
⊢ (𝜑 → ¬ 𝑃 ∈ {0, 1}) | 
| 96 | 77, 95 | eldifd 3962 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ (ℂ ∖ {0,
1})) | 
| 97 | 62 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 98 | 28, 63 | ltned 11397 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ≠ 𝐵) | 
| 99 | 98 | necomd 2996 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ 0) | 
| 100 | 99 | neneqd 2945 | . . . . . . . . 9
⊢ (𝜑 → ¬ 𝐵 = 0) | 
| 101 |  | elsng 4640 | . . . . . . . . . 10
⊢ (𝐵 ∈ ℕ → (𝐵 ∈ {0} ↔ 𝐵 = 0)) | 
| 102 | 61, 101 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 ∈ {0} ↔ 𝐵 = 0)) | 
| 103 | 100, 102 | mtbird 325 | . . . . . . . 8
⊢ (𝜑 → ¬ 𝐵 ∈ {0}) | 
| 104 | 97, 103 | eldifd 3962 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (ℂ ∖
{0})) | 
| 105 |  | cxplogb 26829 | . . . . . . 7
⊢ ((𝑃 ∈ (ℂ ∖ {0, 1})
∧ 𝐵 ∈ (ℂ
∖ {0})) → (𝑃↑𝑐(𝑃 logb 𝐵)) = 𝐵) | 
| 106 | 96, 104, 105 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑃↑𝑐(𝑃 logb 𝐵)) = 𝐵) | 
| 107 | 94, 106 | breqtrrd 5171 | . . . . 5
⊢ (𝜑 → (𝑃↑𝐾) ≤ (𝑃↑𝑐(𝑃 logb 𝐵))) | 
| 108 | 79, 107 | eqbrtrd 5165 | . . . 4
⊢ (𝜑 → (𝑃↑𝑐𝐾) ≤ (𝑃↑𝑐(𝑃 logb 𝐵))) | 
| 109 | 76 | rpred 13077 | . . . . 5
⊢ (𝜑 → 𝑃 ∈ ℝ) | 
| 110 | 36, 66, 109, 38, 70 | ltletrd 11421 | . . . . 5
⊢ (𝜑 → 1 < 𝑃) | 
| 111 | 109, 110,
15, 74 | cxpled 26762 | . . . 4
⊢ (𝜑 → (𝐾 ≤ (𝑃 logb 𝐵) ↔ (𝑃↑𝑐𝐾) ≤ (𝑃↑𝑐(𝑃 logb 𝐵)))) | 
| 112 | 108, 111 | mpbird 257 | . . 3
⊢ (𝜑 → 𝐾 ≤ (𝑃 logb 𝐵)) | 
| 113 | 22, 38 | rplogcld 26671 | . . . . 5
⊢ (𝜑 → (log‘2) ∈
ℝ+) | 
| 114 | 109, 110 | rplogcld 26671 | . . . . 5
⊢ (𝜑 → (log‘𝑃) ∈
ℝ+) | 
| 115 | 61 | nnrpd 13075 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 116 | 115 | relogcld 26665 | . . . . 5
⊢ (𝜑 → (log‘𝐵) ∈
ℝ) | 
| 117 | 61 | nnge1d 12314 | . . . . . 6
⊢ (𝜑 → 1 ≤ 𝐵) | 
| 118 | 62, 117 | logge0d 26672 | . . . . 5
⊢ (𝜑 → 0 ≤ (log‘𝐵)) | 
| 119 |  | 2rp 13039 | . . . . . . . 8
⊢ 2 ∈
ℝ+ | 
| 120 | 119 | a1i 11 | . . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 121 | 120, 76 | logled 26669 | . . . . . 6
⊢ (𝜑 → (2 ≤ 𝑃 ↔ (log‘2) ≤ (log‘𝑃))) | 
| 122 | 70, 121 | mpbid 232 | . . . . 5
⊢ (𝜑 → (log‘2) ≤
(log‘𝑃)) | 
| 123 | 113, 114,
116, 118, 122 | lediv2ad 13099 | . . . 4
⊢ (𝜑 → ((log‘𝐵) / (log‘𝑃)) ≤ ((log‘𝐵) / (log‘2))) | 
| 124 |  | relogbval 26815 | . . . . . 6
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℝ+) → (𝑃 logb 𝐵) = ((log‘𝐵) / (log‘𝑃))) | 
| 125 | 68, 115, 124 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (𝑃 logb 𝐵) = ((log‘𝐵) / (log‘𝑃))) | 
| 126 | 125 | eqcomd 2743 | . . . 4
⊢ (𝜑 → ((log‘𝐵) / (log‘𝑃)) = (𝑃 logb 𝐵)) | 
| 127 | 65 | uzidd 12894 | . . . . . 6
⊢ (𝜑 → 2 ∈
(ℤ≥‘2)) | 
| 128 |  | relogbval 26815 | . . . . . 6
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐵 ∈ ℝ+) → (2
logb 𝐵) =
((log‘𝐵) /
(log‘2))) | 
| 129 | 127, 115,
128 | syl2anc 584 | . . . . 5
⊢ (𝜑 → (2 logb 𝐵) = ((log‘𝐵) /
(log‘2))) | 
| 130 | 129 | eqcomd 2743 | . . . 4
⊢ (𝜑 → ((log‘𝐵) / (log‘2)) = (2
logb 𝐵)) | 
| 131 | 123, 126,
130 | 3brtr3d 5174 | . . 3
⊢ (𝜑 → (𝑃 logb 𝐵) ≤ (2 logb 𝐵)) | 
| 132 | 15, 74, 75, 112, 131 | letrd 11418 | . 2
⊢ (𝜑 → 𝐾 ≤ (2 logb 𝐵)) | 
| 133 |  | flge 13845 | . . 3
⊢ (((2
logb 𝐵) ∈
ℝ ∧ 𝐾 ∈
ℤ) → (𝐾 ≤ (2
logb 𝐵) ↔
𝐾 ≤ (⌊‘(2
logb 𝐵)))) | 
| 134 | 75, 14, 133 | syl2anc 584 | . 2
⊢ (𝜑 → (𝐾 ≤ (2 logb 𝐵) ↔ 𝐾 ≤ (⌊‘(2 logb
𝐵)))) | 
| 135 | 132, 134 | mpbid 232 | 1
⊢ (𝜑 → 𝐾 ≤ (⌊‘(2 logb
𝐵))) |