| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks4d1p3.1 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) | 
| 2 |  | aks4d1p3.2 | . . . . . 6
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) | 
| 3 |  | aks4d1p3.3 | . . . . . 6
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) | 
| 4 | 1, 2, 3 | aks4d1p1 42077 | . . . . 5
⊢ (𝜑 → 𝐴 < (2↑𝐵)) | 
| 5 | 4 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 < (2↑𝐵)) | 
| 6 |  | 2re 12340 | . . . . . . . . 9
⊢ 2 ∈
ℝ | 
| 7 | 6 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) | 
| 8 | 3 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 = (⌈‘((2 logb 𝑁)↑5))) | 
| 9 |  | 2pos 12369 | . . . . . . . . . . . . . . 15
⊢ 0 <
2 | 
| 10 | 9 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 2) | 
| 11 |  | eluzelz 12888 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) | 
| 12 | 1, 11 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 13 | 12 | zred 12722 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 14 |  | 0red 11264 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℝ) | 
| 15 |  | 3re 12346 | . . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ | 
| 16 | 15 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 ∈
ℝ) | 
| 17 |  | 3pos 12371 | . . . . . . . . . . . . . . . 16
⊢ 0 <
3 | 
| 18 | 17 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < 3) | 
| 19 |  | eluzle 12891 | . . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) | 
| 20 | 1, 19 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 3 ≤ 𝑁) | 
| 21 | 14, 16, 13, 18, 20 | ltletrd 11421 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) | 
| 22 |  | 1red 11262 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℝ) | 
| 23 |  | 1lt2 12437 | . . . . . . . . . . . . . . . . 17
⊢ 1 <
2 | 
| 24 | 23 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 < 2) | 
| 25 | 22, 24 | ltned 11397 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≠ 2) | 
| 26 | 25 | necomd 2996 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 1) | 
| 27 | 7, 10, 13, 21, 26 | relogbcld 41974 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) | 
| 28 |  | 5nn0 12546 | . . . . . . . . . . . . . 14
⊢ 5 ∈
ℕ0 | 
| 29 | 28 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → 5 ∈
ℕ0) | 
| 30 | 27, 29 | reexpcld 14203 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁)↑5) ∈
ℝ) | 
| 31 |  | ceilcl 13882 | . . . . . . . . . . . 12
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → (⌈‘((2 logb 𝑁)↑5)) ∈ ℤ) | 
| 32 | 30, 31 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℤ) | 
| 33 | 8, 32 | eqeltrd 2841 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 34 | 32 | zred 12722 | . . . . . . . . . . . 12
⊢ (𝜑 → (⌈‘((2
logb 𝑁)↑5))
∈ ℝ) | 
| 35 | 8, 34 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 36 |  | 7re 12359 | . . . . . . . . . . . . . . 15
⊢ 7 ∈
ℝ | 
| 37 | 36 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 7 ∈
ℝ) | 
| 38 |  | 7pos 12377 | . . . . . . . . . . . . . . 15
⊢ 0 <
7 | 
| 39 | 38 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 7) | 
| 40 | 13, 20 | 3lexlogpow5ineq3 42058 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 7 < ((2 logb
𝑁)↑5)) | 
| 41 | 14, 37, 30, 39, 40 | lttrd 11422 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((2 logb
𝑁)↑5)) | 
| 42 |  | ceilge 13885 | . . . . . . . . . . . . . 14
⊢ (((2
logb 𝑁)↑5)
∈ ℝ → ((2 logb 𝑁)↑5) ≤ (⌈‘((2
logb 𝑁)↑5))) | 
| 43 | 30, 42 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2 logb 𝑁)↑5) ≤
(⌈‘((2 logb 𝑁)↑5))) | 
| 44 | 14, 30, 34, 41, 43 | ltletrd 11421 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < (⌈‘((2
logb 𝑁)↑5))) | 
| 45 | 44, 8 | breqtrrd 5171 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐵) | 
| 46 | 14, 35, 45 | ltled 11409 | . . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐵) | 
| 47 | 33, 46 | jca 511 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 ∈ ℤ ∧ 0 ≤ 𝐵)) | 
| 48 |  | elnn0z 12626 | . . . . . . . . 9
⊢ (𝐵 ∈ ℕ0
↔ (𝐵 ∈ ℤ
∧ 0 ≤ 𝐵)) | 
| 49 | 47, 48 | sylibr 234 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℕ0) | 
| 50 | 7, 49 | reexpcld 14203 | . . . . . . 7
⊢ (𝜑 → (2↑𝐵) ∈ ℝ) | 
| 51 | 50 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (2↑𝐵) ∈ ℝ) | 
| 52 |  | elfznn 13593 | . . . . . . . . . . . . 13
⊢ (𝑞 ∈ (1...𝐵) → 𝑞 ∈ ℕ) | 
| 53 | 52 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑞 ∈ (1...𝐵)) → 𝑞 ∈ ℕ) | 
| 54 | 53 | nnzd 12640 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑞 ∈ (1...𝐵)) → 𝑞 ∈ ℤ) | 
| 55 | 54 | ex 412 | . . . . . . . . . 10
⊢ (𝜑 → (𝑞 ∈ (1...𝐵) → 𝑞 ∈ ℤ)) | 
| 56 | 55 | ssrdv 3989 | . . . . . . . . 9
⊢ (𝜑 → (1...𝐵) ⊆ ℤ) | 
| 57 |  | fzfid 14014 | . . . . . . . . 9
⊢ (𝜑 → (1...𝐵) ∈ Fin) | 
| 58 |  | lcmfcl 16665 | . . . . . . . . 9
⊢
(((1...𝐵) ⊆
ℤ ∧ (1...𝐵)
∈ Fin) → (lcm‘(1...𝐵)) ∈
ℕ0) | 
| 59 | 56, 57, 58 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 →
(lcm‘(1...𝐵))
∈ ℕ0) | 
| 60 | 59 | nn0red 12588 | . . . . . . 7
⊢ (𝜑 →
(lcm‘(1...𝐵))
∈ ℝ) | 
| 61 | 60 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ∈
ℝ) | 
| 62 | 2 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1))) | 
| 63 |  | elnnz 12623 | . . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) | 
| 64 | 12, 21, 63 | sylanbrc 583 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 65 | 7, 10, 35, 45, 26 | relogbcld 41974 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 𝐵) ∈
ℝ) | 
| 66 | 65 | flcld 13838 | . . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℤ) | 
| 67 | 7, 10, 7, 10, 26 | relogbcld 41974 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 2)
∈ ℝ) | 
| 68 |  | 0le1 11786 | . . . . . . . . . . . . . . . . 17
⊢ 0 ≤
1 | 
| 69 | 68 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 1) | 
| 70 | 7 | recnd 11289 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ∈
ℂ) | 
| 71 | 14, 10 | gtned 11396 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ≠ 0) | 
| 72 |  | logbid1 26811 | . . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) =
1) | 
| 73 | 70, 71, 26, 72 | syl3anc 1373 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 logb 2) =
1) | 
| 74 | 73 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 = (2 logb
2)) | 
| 75 | 69, 74 | breqtrd 5169 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ≤ (2 logb
2)) | 
| 76 |  | 2z 12649 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ | 
| 77 | 76 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ∈
ℤ) | 
| 78 | 7 | leidd 11829 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≤ 2) | 
| 79 |  | 2lt7 12456 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 <
7 | 
| 80 | 79 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 < 7) | 
| 81 | 7, 37, 80 | ltled 11409 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ≤ 7) | 
| 82 | 37, 30, 34, 40, 43 | ltletrd 11421 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 7 < (⌈‘((2
logb 𝑁)↑5))) | 
| 83 | 82, 8 | breqtrrd 5171 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 7 < 𝐵) | 
| 84 | 37, 35, 83 | ltled 11409 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 7 ≤ 𝐵) | 
| 85 | 7, 37, 35, 81, 84 | letrd 11418 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≤ 𝐵) | 
| 86 | 77, 78, 7, 10, 35, 45, 85 | logblebd 41977 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 2) ≤
(2 logb 𝐵)) | 
| 87 | 14, 67, 65, 75, 86 | letrd 11418 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (2 logb
𝐵)) | 
| 88 |  | 0zd 12625 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 ∈
ℤ) | 
| 89 |  | flge 13845 | . . . . . . . . . . . . . . 15
⊢ (((2
logb 𝐵) ∈
ℝ ∧ 0 ∈ ℤ) → (0 ≤ (2 logb 𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) | 
| 90 | 65, 88, 89 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (0 ≤ (2 logb
𝐵) ↔ 0 ≤
(⌊‘(2 logb 𝐵)))) | 
| 91 | 87, 90 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (⌊‘(2
logb 𝐵))) | 
| 92 | 66, 91 | jca 511 | . . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘(2
logb 𝐵)) ∈
ℤ ∧ 0 ≤ (⌊‘(2 logb 𝐵)))) | 
| 93 |  | elnn0z 12626 | . . . . . . . . . . . 12
⊢
((⌊‘(2 logb 𝐵)) ∈ ℕ0 ↔
((⌊‘(2 logb 𝐵)) ∈ ℤ ∧ 0 ≤
(⌊‘(2 logb 𝐵)))) | 
| 94 | 92, 93 | sylibr 234 | . . . . . . . . . . 11
⊢ (𝜑 → (⌊‘(2
logb 𝐵)) ∈
ℕ0) | 
| 95 | 64, 94 | nnexpcld 14284 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁↑(⌊‘(2 logb
𝐵))) ∈
ℕ) | 
| 96 |  | fzfid 14014 | . . . . . . . . . . 11
⊢ (𝜑 → (1...(⌊‘((2
logb 𝑁)↑2))) ∈ Fin) | 
| 97 | 12 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℤ) | 
| 98 |  | elfznn 13593 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈ ℕ) | 
| 99 | 98 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ) | 
| 100 | 99 | nnnn0d 12587 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈ ℕ0) | 
| 101 |  | zexpcl 14117 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (𝑁↑𝑘) ∈
ℤ) | 
| 102 | 97, 100, 101 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℤ) | 
| 103 |  | 1zzd 12648 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℤ) | 
| 104 | 102, 103 | zsubcld 12727 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℤ) | 
| 105 |  | 1cnd 11256 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℂ) | 
| 106 | 105 | addridd 11461 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (1 + 0) =
1) | 
| 107 | 22 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ∈
ℝ) | 
| 108 |  | 1nn0 12542 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℕ0 | 
| 109 | 108 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 110 | 13, 109 | reexpcld 14203 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑁↑1) ∈ ℝ) | 
| 111 | 110 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑1) ∈ ℝ) | 
| 112 | 102 | zred 12722 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑𝑘) ∈ ℝ) | 
| 113 |  | 1lt3 12439 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
3 | 
| 114 | 113 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 1 < 3) | 
| 115 | 22, 16, 13, 114, 20 | ltletrd 11421 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 < 𝑁) | 
| 116 | 13 | recnd 11289 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑁 ∈ ℂ) | 
| 117 | 116 | exp1d 14181 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑁↑1) = 𝑁) | 
| 118 | 117 | eqcomd 2743 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 = (𝑁↑1)) | 
| 119 | 115, 118 | breqtrd 5169 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 < (𝑁↑1)) | 
| 120 | 119 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 < (𝑁↑1)) | 
| 121 | 13 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑁 ∈ ℝ) | 
| 122 | 64 | nnge1d 12314 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ≤ 𝑁) | 
| 123 | 122 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 ≤ 𝑁) | 
| 124 |  | elfzuz 13560 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2))) → 𝑘 ∈
(ℤ≥‘1)) | 
| 125 | 124 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 𝑘 ∈
(ℤ≥‘1)) | 
| 126 | 121, 123,
125 | leexp2ad 14293 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (𝑁↑1) ≤ (𝑁↑𝑘)) | 
| 127 | 107, 111,
112, 120, 126 | ltletrd 11421 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 1 < (𝑁↑𝑘)) | 
| 128 | 106, 127 | eqbrtrd 5165 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (1 + 0) < (𝑁↑𝑘)) | 
| 129 | 14 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 0 ∈
ℝ) | 
| 130 | 107, 129,
112 | ltaddsub2d 11864 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((1 + 0) < (𝑁↑𝑘) ↔ 0 < ((𝑁↑𝑘) − 1))) | 
| 131 | 128, 130 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → 0 < ((𝑁↑𝑘) − 1)) | 
| 132 | 104, 131 | jca 511 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → (((𝑁↑𝑘) − 1) ∈ ℤ ∧ 0 <
((𝑁↑𝑘) − 1))) | 
| 133 |  | elnnz 12623 | . . . . . . . . . . . 12
⊢ (((𝑁↑𝑘) − 1) ∈ ℕ ↔ (((𝑁↑𝑘) − 1) ∈ ℤ ∧ 0 <
((𝑁↑𝑘) − 1))) | 
| 134 | 132, 133 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))) → ((𝑁↑𝑘) − 1) ∈ ℕ) | 
| 135 | 96, 134 | fprodnncl 15991 | . . . . . . . . . 10
⊢ (𝜑 → ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1) ∈ ℕ) | 
| 136 | 95, 135 | nnmulcld 12319 | . . . . . . . . 9
⊢ (𝜑 → ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) ∈
ℕ) | 
| 137 | 62, 136 | eqeltrd 2841 | . . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℕ) | 
| 138 | 137 | nnred 12281 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 139 | 138 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 ∈ ℝ) | 
| 140 | 1, 2, 3 | aks4d1p2 42078 | . . . . . . 7
⊢ (𝜑 → (2↑𝐵) ≤ (lcm‘(1...𝐵))) | 
| 141 | 140 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (2↑𝐵) ≤ (lcm‘(1...𝐵))) | 
| 142 | 137 | nnzd 12640 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 143 | 142 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 ∈ ℤ) | 
| 144 | 56 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (1...𝐵) ⊆ ℤ) | 
| 145 |  | fzfid 14014 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (1...𝐵) ∈ Fin) | 
| 146 |  | lcmfdvdsb 16680 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ (1...𝐵) ⊆ ℤ ∧
(1...𝐵) ∈ Fin) →
(∀𝑟 ∈
(1...𝐵)𝑟 ∥ 𝐴 ↔ (lcm‘(1...𝐵)) ∥ 𝐴)) | 
| 147 | 143, 144,
145, 146 | syl3anc 1373 | . . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴 ↔ (lcm‘(1...𝐵)) ∥ 𝐴)) | 
| 148 | 147 | biimpd 229 | . . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴 → (lcm‘(1...𝐵)) ∥ 𝐴)) | 
| 149 | 148 | syldbl2 842 | . . . . . . 7
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ∥ 𝐴) | 
| 150 | 59 | nn0zd 12639 | . . . . . . . . 9
⊢ (𝜑 →
(lcm‘(1...𝐵))
∈ ℤ) | 
| 151 | 150 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ∈
ℤ) | 
| 152 | 137 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → 𝐴 ∈ ℕ) | 
| 153 |  | dvdsle 16347 | . . . . . . . 8
⊢
(((lcm‘(1...𝐵)) ∈ ℤ ∧ 𝐴 ∈ ℕ) →
((lcm‘(1...𝐵))
∥ 𝐴 →
(lcm‘(1...𝐵))
≤ 𝐴)) | 
| 154 | 151, 152,
153 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ((lcm‘(1...𝐵)) ∥ 𝐴 → (lcm‘(1...𝐵)) ≤ 𝐴)) | 
| 155 | 149, 154 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (lcm‘(1...𝐵)) ≤ 𝐴) | 
| 156 | 51, 61, 139, 141, 155 | letrd 11418 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → (2↑𝐵) ≤ 𝐴) | 
| 157 | 51, 139 | lenltd 11407 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ((2↑𝐵) ≤ 𝐴 ↔ ¬ 𝐴 < (2↑𝐵))) | 
| 158 | 156, 157 | mpbid 232 | . . . 4
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ¬ 𝐴 < (2↑𝐵)) | 
| 159 | 5, 158 | pm2.21dd 195 | . . 3
⊢ ((𝜑 ∧ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) | 
| 160 |  | simpr 484 | . . 3
⊢ ((𝜑 ∧ ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) → ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) | 
| 161 | 159, 160 | pm2.61dan 813 | . 2
⊢ (𝜑 → ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) | 
| 162 |  | rexnal 3100 | . 2
⊢
(∃𝑟 ∈
(1...𝐵) ¬ 𝑟 ∥ 𝐴 ↔ ¬ ∀𝑟 ∈ (1...𝐵)𝑟 ∥ 𝐴) | 
| 163 | 161, 162 | sylibr 234 | 1
⊢ (𝜑 → ∃𝑟 ∈ (1...𝐵) ¬ 𝑟 ∥ 𝐴) |