| Step | Hyp | Ref
| Expression |
| 1 | | aks6d1c7lem1.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘3)) |
| 2 | | eluzelz 12888 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘3) → 𝑁 ∈ ℤ) |
| 3 | 1, 2 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 4 | | 0red 11264 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) |
| 5 | | 3re 12346 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
| 6 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 3 ∈
ℝ) |
| 7 | 3 | zred 12722 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 8 | | 3pos 12371 |
. . . . . . . . . . 11
⊢ 0 <
3 |
| 9 | 8 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 3) |
| 10 | | eluzle 12891 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘3) → 3 ≤ 𝑁) |
| 11 | 1, 10 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 3 ≤ 𝑁) |
| 12 | 4, 6, 7, 9, 11 | ltletrd 11421 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑁) |
| 13 | 3, 12 | jca 511 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 0 < 𝑁)) |
| 14 | | elnnz 12623 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℤ ∧ 0 <
𝑁)) |
| 15 | 13, 14 | sylibr 234 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 16 | 15 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 17 | | aks6d1c7lem1.8 |
. . . . . . . . . . . . 13
⊢ 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 18 | 17 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 = (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 19 | | aks6d1c7lem1.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 20 | | aks6d1c7lem1.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∥ 𝑁) |
| 21 | | aks6d1c7lem1.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ ℕ) |
| 22 | | aks6d1c7lem1.5 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 gcd 𝑅) = 1) |
| 23 | | aks6d1c7lem1.6 |
. . . . . . . . . . . . 13
⊢ 𝐸 = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0
↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) |
| 24 | | aks6d1c7lem1.7 |
. . . . . . . . . . . . 13
⊢ 𝐿 =
(ℤRHom‘(ℤ/nℤ‘𝑅)) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(ℤ/nℤ‘𝑅) = (ℤ/nℤ‘𝑅) |
| 26 | 15, 19, 20, 21, 22, 23, 24, 25 | hashscontpowcl 42121 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0) |
| 27 | 18, 26 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
| 28 | 27 | nn0red 12588 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 29 | 27 | nn0ge0d 12590 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐷) |
| 30 | 28, 29 | resqrtcld 15456 |
. . . . . . . . 9
⊢ (𝜑 → (√‘𝐷) ∈
ℝ) |
| 31 | 30 | flcld 13838 |
. . . . . . . 8
⊢ (𝜑 →
(⌊‘(√‘𝐷)) ∈ ℤ) |
| 32 | 28, 29 | sqrtge0d 15459 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤
(√‘𝐷)) |
| 33 | | 0zd 12625 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
| 34 | | flge 13845 |
. . . . . . . . . 10
⊢
(((√‘𝐷)
∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤ (√‘𝐷) ↔ 0 ≤
(⌊‘(√‘𝐷)))) |
| 35 | 30, 33, 34 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤
(√‘𝐷) ↔ 0
≤ (⌊‘(√‘𝐷)))) |
| 36 | 32, 35 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤
(⌊‘(√‘𝐷))) |
| 37 | 31, 36 | jca 511 |
. . . . . . 7
⊢ (𝜑 →
((⌊‘(√‘𝐷)) ∈ ℤ ∧ 0 ≤
(⌊‘(√‘𝐷)))) |
| 38 | | elnn0z 12626 |
. . . . . . 7
⊢
((⌊‘(√‘𝐷)) ∈ ℕ0 ↔
((⌊‘(√‘𝐷)) ∈ ℤ ∧ 0 ≤
(⌊‘(√‘𝐷)))) |
| 39 | 37, 38 | sylibr 234 |
. . . . . 6
⊢ (𝜑 →
(⌊‘(√‘𝐷)) ∈
ℕ0) |
| 40 | 16, 39 | reexpcld 14203 |
. . . . 5
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) ∈
ℝ) |
| 41 | | 2re 12340 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ) |
| 43 | | 2pos 12369 |
. . . . . . . . . . . . . . 15
⊢ 0 <
2 |
| 44 | 43 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 2) |
| 45 | 15 | nngt0d 12315 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 𝑁) |
| 46 | | 1ne2 12474 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≠
2 |
| 47 | 46 | necomi 2995 |
. . . . . . . . . . . . . . 15
⊢ 2 ≠
1 |
| 48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≠ 1) |
| 49 | 42, 44, 16, 45, 48 | relogbcld 41974 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 𝑁) ∈
ℝ) |
| 50 | 18, 28 | eqeltrrd 2842 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℝ) |
| 51 | 29, 18 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤
(♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0))))) |
| 52 | 50, 51 | resqrtcld 15456 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ) |
| 53 | 49, 52 | remulcld 11291 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℝ) |
| 54 | 53 | flcld 13838 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℤ) |
| 55 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) |
| 56 | | 0le1 11786 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
1 |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 1) |
| 58 | 42 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ∈
ℂ) |
| 59 | 4, 44 | gtned 11396 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ≠ 0) |
| 60 | | logbid1 26811 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 2) =
1) |
| 61 | 58, 59, 48, 60 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 logb 2) =
1) |
| 62 | 61 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 = (2 logb
2)) |
| 63 | | 2z 12649 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℤ |
| 64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ∈
ℤ) |
| 65 | 42 | leidd 11829 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≤ 2) |
| 66 | | 1nn0 12542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℕ0 |
| 67 | 41, 66 | nn0addge1i 12574 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≤ (2
+ 1) |
| 68 | | 2p1e3 12408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 + 1) =
3 |
| 69 | 67, 68 | breqtri 5168 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ≤
3 |
| 70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 ≤ 3) |
| 71 | 42, 6, 7, 70, 11 | letrd 11418 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≤ 𝑁) |
| 72 | 64, 65, 42, 44, 7, 12, 71 | logblebd 41977 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 2) ≤
(2 logb 𝑁)) |
| 73 | 62, 72 | eqbrtrd 5165 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≤ (2 logb
𝑁)) |
| 74 | 4, 55, 49, 57, 73 | letrd 11418 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (2 logb
𝑁)) |
| 75 | 50, 51 | sqrtge0d 15459 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 76 | 49, 52, 74, 75 | mulge0d 11840 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ ((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 77 | | flge 13845 |
. . . . . . . . . . . . 13
⊢ ((((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℝ ∧ 0 ∈ ℤ) → (0 ≤
((2 logb 𝑁)
· (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ↔ 0 ≤ (⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 78 | 53, 33, 77 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ ((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ↔ 0 ≤ (⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 79 | 76, 78 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 80 | 54, 79 | jca 511 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℤ ∧ 0 ≤ (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 81 | | elnn0z 12626 |
. . . . . . . . . 10
⊢
((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℕ0 ↔
((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℤ ∧ 0 ≤ (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 82 | 80, 81 | sylibr 234 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℕ0) |
| 83 | 66 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℕ0) |
| 84 | 82, 83 | nn0addcld 12591 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ∈ ℕ0) |
| 85 | 21 | phicld 16809 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ϕ‘𝑅) ∈
ℕ) |
| 86 | 85 | nnred 12281 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (ϕ‘𝑅) ∈
ℝ) |
| 87 | 85 | nnnn0d 12587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ϕ‘𝑅) ∈
ℕ0) |
| 88 | 87 | nn0ge0d 12590 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (ϕ‘𝑅)) |
| 89 | 86, 88 | resqrtcld 15456 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(√‘(ϕ‘𝑅)) ∈ ℝ) |
| 90 | 89, 49 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (𝜑 →
((√‘(ϕ‘𝑅)) · (2 logb 𝑁)) ∈
ℝ) |
| 91 | 90 | flcld 13838 |
. . . . . . . . . 10
⊢ (𝜑 →
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) ∈
ℤ) |
| 92 | 86, 88 | sqrtge0d 15459 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤
(√‘(ϕ‘𝑅))) |
| 93 | 89, 49, 92, 74 | mulge0d 11840 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤
((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) |
| 94 | | flge 13845 |
. . . . . . . . . . . 12
⊢
((((√‘(ϕ‘𝑅)) · (2 logb 𝑁)) ∈ ℝ ∧ 0 ∈
ℤ) → (0 ≤ ((√‘(ϕ‘𝑅)) · (2 logb 𝑁)) ↔ 0 ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))) |
| 95 | 90, 33, 94 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ≤
((√‘(ϕ‘𝑅)) · (2 logb 𝑁)) ↔ 0 ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))) |
| 96 | 93, 95 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) |
| 97 | 91, 96 | jca 511 |
. . . . . . . . 9
⊢ (𝜑 →
((⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) ∈ ℤ ∧ 0 ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))) |
| 98 | | elnn0z 12626 |
. . . . . . . . 9
⊢
((⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) ∈ ℕ0
↔ ((⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) ∈ ℤ ∧ 0 ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))) |
| 99 | 97, 98 | sylibr 234 |
. . . . . . . 8
⊢ (𝜑 →
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) ∈
ℕ0) |
| 100 | 84, 99 | nn0addcld 12591 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) ∈
ℕ0) |
| 101 | 54 | peano2zd 12725 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ∈ ℤ) |
| 102 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
| 103 | 102 | znegcld 12724 |
. . . . . . . 8
⊢ (𝜑 → -1 ∈
ℤ) |
| 104 | 101, 103 | zaddcld 12726 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1) ∈ ℤ) |
| 105 | | bccl 14361 |
. . . . . . 7
⊢
(((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) ∈ ℕ0
∧ (((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1) ∈ ℤ) →
((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1)) ∈
ℕ0) |
| 106 | 100, 104,
105 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1)) ∈
ℕ0) |
| 107 | 106 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1)) ∈ ℝ) |
| 108 | 26, 99 | nn0addcld 12591 |
. . . . . . 7
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁)))) ∈
ℕ0) |
| 109 | 26 | nn0zd 12639 |
. . . . . . . 8
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℤ) |
| 110 | 109, 103 | zaddcld 12726 |
. . . . . . 7
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1) ∈ ℤ) |
| 111 | | bccl 14361 |
. . . . . . 7
⊢
((((♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0)))) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) ∈ ℕ0
∧ ((♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0)))) + -1) ∈ ℤ)
→ (((♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0)))) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1)) ∈ ℕ0) |
| 112 | 108, 110,
111 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1)) ∈ ℕ0) |
| 113 | 112 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1)) ∈ ℝ) |
| 114 | 52, 49 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ∈ ℝ) |
| 115 | 114 | flcld 13838 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ∈ ℤ) |
| 116 | 52, 49, 75, 74 | mulge0d 11840 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) |
| 117 | | flge 13845 |
. . . . . . . . . . . . . 14
⊢
((((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ∈ ℝ ∧ 0 ∈ ℤ)
→ (0 ≤ ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ↔ 0 ≤
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))) |
| 118 | 114, 33, 117 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 ≤
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ↔ 0 ≤
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))) |
| 119 | 116, 118 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)))) |
| 120 | 115, 119 | jca 511 |
. . . . . . . . . . 11
⊢ (𝜑 →
((⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ∈ ℤ ∧ 0 ≤
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))) |
| 121 | | elnn0z 12626 |
. . . . . . . . . . 11
⊢
((⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ∈ ℕ0 ↔
((⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ∈ ℤ ∧ 0 ≤
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))) |
| 122 | 120, 121 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝜑 →
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ∈
ℕ0) |
| 123 | 84, 122 | nn0addcld 12591 |
. . . . . . . . 9
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)))) ∈
ℕ0) |
| 124 | | bccl 14361 |
. . . . . . . . 9
⊢
(((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)))) ∈ ℕ0 ∧
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℤ) → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))C(⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℕ0) |
| 125 | 123, 54, 124 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))C(⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℕ0) |
| 126 | 125 | nn0red 12588 |
. . . . . . 7
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))C(⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℝ) |
| 127 | | bccl 14361 |
. . . . . . . . 9
⊢
(((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) ∈ ℕ0
∧ (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℤ) → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℕ0) |
| 128 | 100, 54, 127 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℕ0) |
| 129 | 128 | nn0red 12588 |
. . . . . . 7
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℝ) |
| 130 | 42, 84 | reexpcld 14203 |
. . . . . . . . . . 11
⊢ (𝜑 →
(2↑((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) ∈ ℝ) |
| 131 | | 2nn0 12543 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℕ0 |
| 132 | 131 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℕ0) |
| 133 | 132, 82 | nn0mulcld 12592 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℕ0) |
| 134 | 133, 83 | nn0addcld 12591 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1) ∈ ℕ0) |
| 135 | | bccl 14361 |
. . . . . . . . . . . . 13
⊢ ((((2
· (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1) ∈ ℕ0 ∧
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℤ) → (((2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℕ0) |
| 136 | 134, 54, 135 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℕ0) |
| 137 | 136 | nn0red 12588 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ∈ ℝ) |
| 138 | 4, 42, 44 | ltled 11409 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ 2) |
| 139 | 42, 138, 53 | recxpcld 26765 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℝ) |
| 140 | | reflcl 13836 |
. . . . . . . . . . . . . . . 16
⊢ (((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℝ → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℝ) |
| 141 | 53, 140 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℝ) |
| 142 | 141, 55 | readdcld 11290 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ∈ ℝ) |
| 143 | 42, 138, 142 | recxpcld 26765 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(2↑𝑐((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) ∈ ℝ) |
| 144 | | 1le2 12475 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ≤
2 |
| 145 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≤ 2) |
| 146 | 55, 42, 7, 145, 71 | letrd 11418 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ≤ 𝑁) |
| 147 | | reflcl 13836 |
. . . . . . . . . . . . . . . . 17
⊢
((√‘𝐷)
∈ ℝ → (⌊‘(√‘𝐷)) ∈ ℝ) |
| 148 | 30, 147 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(⌊‘(√‘𝐷)) ∈ ℝ) |
| 149 | 18 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (√‘𝐷) =
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 150 | 149 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(⌊‘(√‘𝐷)) =
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 151 | | flle 13839 |
. . . . . . . . . . . . . . . . . 18
⊢
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ →
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 152 | 52, 151 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(⌊‘(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 153 | 150, 152 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(⌊‘(√‘𝐷)) ≤ (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 154 | 7, 146, 148, 52, 153 | cxplead 26763 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁↑𝑐(⌊‘(√‘𝐷))) ≤ (𝑁↑𝑐(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 155 | 7 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 156 | 4, 12 | gtned 11396 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ≠ 0) |
| 157 | 155, 156,
31 | cxpexpzd 26753 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁↑𝑐(⌊‘(√‘𝐷))) = (𝑁↑(⌊‘(√‘𝐷)))) |
| 158 | 59, 48 | nelprd 4657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ 2 ∈ {0,
1}) |
| 159 | 58, 158 | eldifd 3962 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ∈ (ℂ ∖
{0, 1})) |
| 160 | 156 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ¬ 𝑁 = 0) |
| 161 | | elsng 4640 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ {0} ↔ 𝑁 = 0)) |
| 162 | 15, 161 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑁 ∈ {0} ↔ 𝑁 = 0)) |
| 163 | 160, 162 | mtbird 325 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ¬ 𝑁 ∈ {0}) |
| 164 | 155, 163 | eldifd 3962 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ (ℂ ∖
{0})) |
| 165 | | cxplogb 26829 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ (ℂ ∖ {0, 1}) ∧ 𝑁 ∈ (ℂ ∖ {0})) →
(2↑𝑐(2 logb 𝑁)) = 𝑁) |
| 166 | 159, 164,
165 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(2↑𝑐(2 logb 𝑁)) = 𝑁) |
| 167 | 166 | eqcomd 2743 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 = (2↑𝑐(2
logb 𝑁))) |
| 168 | 167 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁↑𝑐(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = ((2↑𝑐(2 logb 𝑁))↑𝑐(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 169 | 154, 157,
168 | 3brtr3d 5174 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) ≤
((2↑𝑐(2 logb 𝑁))↑𝑐(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 170 | 42, 44 | elrpd 13074 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ∈
ℝ+) |
| 171 | 52 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℂ) |
| 172 | | cxpmul 26730 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℝ+ ∧ (2 logb 𝑁) ∈ ℝ ∧
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℂ) → (2↑𝑐((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) = ((2↑𝑐(2 logb
𝑁))↑𝑐(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 173 | 170, 49, 171, 172 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) = ((2↑𝑐(2 logb
𝑁))↑𝑐(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 174 | 169, 173 | breqtrrd 5171 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) ≤
(2↑𝑐((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 175 | | fllep1 13841 |
. . . . . . . . . . . . . . 15
⊢ (((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℝ → ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ≤ ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) |
| 176 | 53, 175 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ≤ ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) |
| 177 | 55, 42, 145, 48 | leneltd 11415 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < 2) |
| 178 | 84 | nn0red 12588 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ∈ ℝ) |
| 179 | 42, 177, 53, 178 | cxpled 26762 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ≤ ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ↔ (2↑𝑐((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ≤ (2↑𝑐((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)))) |
| 180 | 176, 179 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(2↑𝑐((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ≤ (2↑𝑐((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1))) |
| 181 | 40, 139, 143, 174, 180 | letrd 11418 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) ≤
(2↑𝑐((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1))) |
| 182 | | cxpexpz 26709 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ∈ ℤ) →
(2↑𝑐((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) = (2↑((⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1))) |
| 183 | 58, 59, 101, 182 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(2↑𝑐((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) = (2↑((⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1))) |
| 184 | 181, 183 | breqtrd 5169 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) ≤
(2↑((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1))) |
| 185 | 49, 49 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2 logb 𝑁) ∈ ℝ ∧ (2
logb 𝑁) ∈
ℝ)) |
| 186 | | remulcl 11240 |
. . . . . . . . . . . . . . 15
⊢ (((2
logb 𝑁) ∈
ℝ ∧ (2 logb 𝑁) ∈ ℝ) → ((2 logb
𝑁) · (2
logb 𝑁)) ∈
ℝ) |
| 187 | 185, 186 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb 𝑁) · (2 logb
𝑁)) ∈
ℝ) |
| 188 | | reflcl 13836 |
. . . . . . . . . . . . . 14
⊢ (((2
logb 𝑁) ·
(2 logb 𝑁))
∈ ℝ → (⌊‘((2 logb 𝑁) · (2 logb 𝑁))) ∈
ℝ) |
| 189 | 187, 188 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(2 logb 𝑁)))
∈ ℝ) |
| 190 | 82 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℝ) |
| 191 | 42, 44, 6, 9, 48 | relogbcld 41974 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 logb 3)
∈ ℝ) |
| 192 | 191 | resqcld 14165 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 logb
3)↑2) ∈ ℝ) |
| 193 | 49 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (2 logb 𝑁) ∈
ℂ) |
| 194 | 193 | sqvald 14183 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 logb 𝑁)↑2) = ((2 logb
𝑁) · (2
logb 𝑁))) |
| 195 | 194, 187 | eqeltrd 2841 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 logb 𝑁)↑2) ∈
ℝ) |
| 196 | | 3lexlogpow2ineq2 42060 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 <
((2 logb 3)↑2) ∧ ((2 logb 3)↑2) <
3) |
| 197 | 196 | simpli 483 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 <
((2 logb 3)↑2) |
| 198 | 197 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 2 < ((2 logb
3)↑2)) |
| 199 | 42, 192, 198 | ltled 11409 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 2 ≤ ((2 logb
3)↑2)) |
| 200 | 6, 42, 59 | redivcld 12095 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (3 / 2) ∈
ℝ) |
| 201 | | 2rp 13039 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℝ+ |
| 202 | 201 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 2 ∈
ℝ+) |
| 203 | 4, 6, 9 | ltled 11409 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≤ 3) |
| 204 | 6, 202, 203 | divge0d 13117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 0 ≤ (3 /
2)) |
| 205 | | 3lexlogpow2ineq1 42059 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((3 / 2)
< (2 logb 3) ∧ (2 logb 3) < (5 /
3)) |
| 206 | 205 | simpli 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (3 / 2)
< (2 logb 3) |
| 207 | 206 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (3 / 2) < (2
logb 3)) |
| 208 | 200, 191,
207 | ltled 11409 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (3 / 2) ≤ (2
logb 3)) |
| 209 | 4, 200, 191, 204, 208 | letrd 11418 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤ (2 logb
3)) |
| 210 | 64, 65, 6, 9, 7, 12,
11 | logblebd 41977 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2 logb 3) ≤
(2 logb 𝑁)) |
| 211 | 191, 49, 132, 209, 210 | leexp1ad 41973 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 logb
3)↑2) ≤ ((2 logb 𝑁)↑2)) |
| 212 | 42, 192, 195, 199, 211 | letrd 11418 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 2 ≤ ((2 logb
𝑁)↑2)) |
| 213 | 212, 194 | breqtrd 5169 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ≤ ((2 logb
𝑁) · (2
logb 𝑁))) |
| 214 | | flge 13845 |
. . . . . . . . . . . . . . 15
⊢ ((((2
logb 𝑁) ·
(2 logb 𝑁))
∈ ℝ ∧ 2 ∈ ℤ) → (2 ≤ ((2 logb 𝑁) · (2 logb
𝑁)) ↔ 2 ≤
(⌊‘((2 logb 𝑁) · (2 logb 𝑁))))) |
| 215 | 187, 64, 214 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 ≤ ((2
logb 𝑁) ·
(2 logb 𝑁))
↔ 2 ≤ (⌊‘((2 logb 𝑁) · (2 logb 𝑁))))) |
| 216 | 213, 215 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ≤ (⌊‘((2
logb 𝑁) ·
(2 logb 𝑁)))) |
| 217 | 49, 49 | remulcld 11291 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb 𝑁) · (2 logb
𝑁)) ∈
ℝ) |
| 218 | | aks6d1c7lem1.10 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((2 logb 𝑁)↑2) <
((odℤ‘𝑅)‘𝑁)) |
| 219 | 15, 19, 20, 21, 22, 23, 24, 25, 218 | aks6d1c3 42124 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 logb 𝑁)↑2) <
(♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0))))) |
| 220 | 171 | sqvald 14183 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))↑2) = ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 221 | 26 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℂ) |
| 222 | 221 | msqsqrtd 15479 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 223 | 220, 222 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) = ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))↑2)) |
| 224 | 219, 223 | breqtrd 5169 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 logb 𝑁)↑2) <
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))↑2)) |
| 225 | 49, 52, 74, 75 | lt2sqd 14295 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 logb 𝑁) <
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ↔ ((2 logb 𝑁)↑2) <
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))↑2))) |
| 226 | 224, 225 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 logb 𝑁) <
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 227 | 49, 52, 226 | ltled 11409 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (2 logb 𝑁) ≤
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 228 | 49, 52, 49, 74, 227 | lemul2ad 12208 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb 𝑁) · (2 logb
𝑁)) ≤ ((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 229 | | flwordi 13852 |
. . . . . . . . . . . . . 14
⊢ ((((2
logb 𝑁) ·
(2 logb 𝑁))
∈ ℝ ∧ ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℝ ∧ ((2 logb 𝑁) · (2 logb
𝑁)) ≤ ((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) → (⌊‘((2 logb 𝑁) · (2 logb
𝑁))) ≤
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 230 | 217, 53, 228, 229 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(2 logb 𝑁)))
≤ (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 231 | 42, 189, 190, 216, 230 | letrd 11418 |
. . . . . . . . . . . 12
⊢ (𝜑 → 2 ≤ (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 232 | 54, 231 | 2ap1caineq 42146 |
. . . . . . . . . . 11
⊢ (𝜑 →
(2↑((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) < (((2 · (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 233 | 40, 130, 137, 184, 232 | lelttrd 11419 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < (((2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 234 | 82 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) ∈ ℂ) |
| 235 | 234 | 2timesd 12509 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) = ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 236 | 235 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1) = (((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)) |
| 237 | 236 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (((2 ·
(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) = ((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 238 | 233, 237 | breqtrd 5169 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 239 | | 1cnd 11256 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
| 240 | 234, 234,
239 | addassd 11283 |
. . . . . . . . . . 11
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1) = ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1))) |
| 241 | 84 | nn0cnd 12589 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ∈ ℂ) |
| 242 | 234, 241 | addcomd 11463 |
. . . . . . . . . . 11
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1)) = (((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 243 | 240, 242 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1) = (((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 244 | 243 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) + 1)C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) = ((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 245 | 238, 244 | breqtrd 5169 |
. . . . . . . 8
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 246 | 193, 171 | mulcomd 11282 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) |
| 247 | 246 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) =
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)))) |
| 248 | 247 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) = (((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))) |
| 249 | 248 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))C(⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) = ((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))C(⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 250 | 245, 249 | breqtrd 5169 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))C(⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 251 | 122 | nn0red 12588 |
. . . . . . . . 9
⊢ (𝜑 →
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ∈ ℝ) |
| 252 | 99 | nn0red 12588 |
. . . . . . . . 9
⊢ (𝜑 →
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) ∈
ℝ) |
| 253 | 17, 27 | eqeltrrid 2846 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0) |
| 254 | 253 | nn0red 12588 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℝ) |
| 255 | 253 | nn0ge0d 12590 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤
(♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0))))) |
| 256 | 254, 255 | resqrtcld 15456 |
. . . . . . . . . . 11
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ) |
| 257 | 256, 49 | remulcld 11291 |
. . . . . . . . . 10
⊢ (𝜑 →
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ∈ ℝ) |
| 258 | 15, 19, 20, 21, 22, 23, 24 | aks6d1c4 42125 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≤ (ϕ‘𝑅)) |
| 259 | 50, 51, 86, 88 | sqrtled 15465 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≤ (ϕ‘𝑅) ↔
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ≤ (√‘(ϕ‘𝑅)))) |
| 260 | 258, 259 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ≤ (√‘(ϕ‘𝑅))) |
| 261 | 256, 89, 49, 74, 260 | lemul1ad 12207 |
. . . . . . . . . 10
⊢ (𝜑 →
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ≤ ((√‘(ϕ‘𝑅)) · (2 logb
𝑁))) |
| 262 | | flwordi 13852 |
. . . . . . . . . 10
⊢
((((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ∈ ℝ ∧
((√‘(ϕ‘𝑅)) · (2 logb 𝑁)) ∈ ℝ ∧
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)) ≤ ((√‘(ϕ‘𝑅)) · (2 logb
𝑁))) →
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) |
| 263 | 257, 90, 261, 262 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 →
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))) ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) |
| 264 | 251, 252,
142, 263 | leadd2dd 11878 |
. . . . . . . 8
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁)))) ≤ (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))) |
| 265 | 123, 100,
54, 264 | bcled 42179 |
. . . . . . 7
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (2 logb 𝑁))))C(⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) ≤ ((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 266 | 40, 126, 129, 250, 265 | ltletrd 11421 |
. . . . . 6
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))))) |
| 267 | 234, 239 | pncand 11621 |
. . . . . . . . 9
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) − 1) = (⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) |
| 268 | 267 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) = (((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) − 1)) |
| 269 | 241, 239 | negsubd 11626 |
. . . . . . . . 9
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1) = (((⌊‘((2 logb
𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) − 1)) |
| 270 | 269 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝜑 → (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) − 1) = (((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1)) |
| 271 | 268, 270 | eqtrd 2777 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) = (((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1)) |
| 272 | 271 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))))) = ((((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1))) |
| 273 | 266, 272 | breqtrd 5169 |
. . . . 5
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1))) |
| 274 | 21 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑅 ∈
ℕ0) |
| 275 | 25 | zncrng 21563 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 ∈ ℕ0
→ (ℤ/nℤ‘𝑅) ∈ CRing) |
| 276 | 274, 275 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(ℤ/nℤ‘𝑅) ∈ CRing) |
| 277 | | crngring 20242 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ/nℤ‘𝑅) ∈ CRing →
(ℤ/nℤ‘𝑅) ∈ Ring) |
| 278 | 24 | zrhrhm 21522 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ/nℤ‘𝑅) ∈ Ring → 𝐿 ∈ (ℤring RingHom
(ℤ/nℤ‘𝑅))) |
| 279 | | zringbas 21464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℤ =
(Base‘ℤring) |
| 280 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘(ℤ/nℤ‘𝑅)) =
(Base‘(ℤ/nℤ‘𝑅)) |
| 281 | 279, 280 | rhmf 20485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐿 ∈ (ℤring
RingHom (ℤ/nℤ‘𝑅)) → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) |
| 282 | 276, 277,
278, 281 | 4syl 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘(ℤ/nℤ‘𝑅))) |
| 283 | 282 | ffnd 6737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐿 Fn ℤ) |
| 284 | 15, 19, 20, 23 | aks6d1c2p1 42119 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸:(ℕ0 ×
ℕ0)⟶ℕ) |
| 285 | | nnssz 12635 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ℕ
⊆ ℤ |
| 286 | 285 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ℕ ⊆
ℤ) |
| 287 | 284, 286 | fssd 6753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸:(ℕ0 ×
ℕ0)⟶ℤ) |
| 288 | | frn 6743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐸:(ℕ0 ×
ℕ0)⟶ℤ → ran 𝐸 ⊆ ℤ) |
| 289 | 287, 288 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran 𝐸 ⊆ ℤ) |
| 290 | 284 | ffnd 6737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐸 Fn (ℕ0 ×
ℕ0)) |
| 291 | | fnima 6698 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐸 Fn (ℕ0 ×
ℕ0) → (𝐸 “ (ℕ0 ×
ℕ0)) = ran 𝐸) |
| 292 | 290, 291 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) = ran 𝐸) |
| 293 | 292 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ)) |
| 294 | 289, 293 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐸 “ (ℕ0 ×
ℕ0)) ⊆ ℤ) |
| 295 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑘 ∈ V |
| 296 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑙 ∈ V |
| 297 | 295, 296 | op1std 8024 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = 〈𝑘, 𝑙〉 → (1st ‘𝑣) = 𝑘) |
| 298 | 297 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 〈𝑘, 𝑙〉 → (𝑃↑(1st ‘𝑣)) = (𝑃↑𝑘)) |
| 299 | 295, 296 | op2ndd 8025 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = 〈𝑘, 𝑙〉 → (2nd ‘𝑣) = 𝑙) |
| 300 | 299 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 〈𝑘, 𝑙〉 → ((𝑁 / 𝑃)↑(2nd ‘𝑣)) = ((𝑁 / 𝑃)↑𝑙)) |
| 301 | 298, 300 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = 〈𝑘, 𝑙〉 → ((𝑃↑(1st ‘𝑣)) · ((𝑁 / 𝑃)↑(2nd ‘𝑣))) = ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) |
| 302 | 301 | mpompt 7547 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∈ (ℕ0
× ℕ0) ↦ ((𝑃↑(1st ‘𝑣)) · ((𝑁 / 𝑃)↑(2nd ‘𝑣)))) = (𝑘 ∈ ℕ0, 𝑙 ∈ ℕ0
↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) |
| 303 | 302 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ0,
𝑙 ∈
ℕ0 ↦ ((𝑃↑𝑘) · ((𝑁 / 𝑃)↑𝑙))) = (𝑣 ∈ (ℕ0 ×
ℕ0) ↦ ((𝑃↑(1st ‘𝑣)) · ((𝑁 / 𝑃)↑(2nd ‘𝑣)))) |
| 304 | 23, 303 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐸 = (𝑣 ∈ (ℕ0 ×
ℕ0) ↦ ((𝑃↑(1st ‘𝑣)) · ((𝑁 / 𝑃)↑(2nd ‘𝑣)))) |
| 305 | 304 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐸 = (𝑣 ∈ (ℕ0 ×
ℕ0) ↦ ((𝑃↑(1st ‘𝑣)) · ((𝑁 / 𝑃)↑(2nd ‘𝑣))))) |
| 306 | | c0ex 11255 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
V |
| 307 | 306, 306 | op1std 8024 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = 〈0, 0〉 →
(1st ‘𝑣) =
0) |
| 308 | 307 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑣 = 〈0, 0〉) → (1st
‘𝑣) =
0) |
| 309 | 308 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑣 = 〈0, 0〉) → (𝑃↑(1st
‘𝑣)) = (𝑃↑0)) |
| 310 | 306, 306 | op2ndd 8025 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = 〈0, 0〉 →
(2nd ‘𝑣) =
0) |
| 311 | 310 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑣 = 〈0, 0〉) → (2nd
‘𝑣) =
0) |
| 312 | 311 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑣 = 〈0, 0〉) → ((𝑁 / 𝑃)↑(2nd ‘𝑣)) = ((𝑁 / 𝑃)↑0)) |
| 313 | 309, 312 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑣 = 〈0, 0〉) → ((𝑃↑(1st
‘𝑣)) · ((𝑁 / 𝑃)↑(2nd ‘𝑣))) = ((𝑃↑0) · ((𝑁 / 𝑃)↑0))) |
| 314 | | prmnn 16711 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 315 | 19, 314 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 316 | 315 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 317 | 316 | exp0d 14180 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑃↑0) = 1) |
| 318 | 315 | nnne0d 12316 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑃 ≠ 0) |
| 319 | 155, 316,
318 | divcld 12043 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑁 / 𝑃) ∈ ℂ) |
| 320 | 319 | exp0d 14180 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝑁 / 𝑃)↑0) = 1) |
| 321 | 317, 320 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑃↑0) · ((𝑁 / 𝑃)↑0)) = (1 ·
1)) |
| 322 | 239 | mulridd 11278 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 · 1) =
1) |
| 323 | 321, 322 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑃↑0) · ((𝑁 / 𝑃)↑0)) = 1) |
| 324 | 323 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑣 = 〈0, 0〉) → ((𝑃↑0) · ((𝑁 / 𝑃)↑0)) = 1) |
| 325 | 313, 324 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑣 = 〈0, 0〉) → ((𝑃↑(1st
‘𝑣)) · ((𝑁 / 𝑃)↑(2nd ‘𝑣))) = 1) |
| 326 | | 0nn0 12541 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ∈
ℕ0 |
| 327 | 326 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 0 ∈
ℕ0) |
| 328 | 327, 327 | opelxpd 5724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 〈0, 0〉 ∈
(ℕ0 × ℕ0)) |
| 329 | | 1nn 12277 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℕ |
| 330 | 329 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℕ) |
| 331 | 305, 325,
328, 330 | fvmptd 7023 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸‘〈0, 0〉) =
1) |
| 332 | | ssidd 4007 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ℕ0
× ℕ0) ⊆ (ℕ0 ×
ℕ0)) |
| 333 | | fnfvima 7253 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐸 Fn (ℕ0 ×
ℕ0) ∧ (ℕ0 × ℕ0)
⊆ (ℕ0 × ℕ0) ∧ 〈0,
0〉 ∈ (ℕ0 × ℕ0)) → (𝐸‘〈0, 0〉) ∈
(𝐸 “
(ℕ0 × ℕ0))) |
| 334 | 290, 332,
328, 333 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐸‘〈0, 0〉) ∈ (𝐸 “ (ℕ0
× ℕ0))) |
| 335 | 331, 334 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈ (𝐸 “ (ℕ0
× ℕ0))) |
| 336 | | fnfvima 7253 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐿 Fn ℤ ∧ (𝐸 “ (ℕ0
× ℕ0)) ⊆ ℤ ∧ 1 ∈ (𝐸 “ (ℕ0 ×
ℕ0))) → (𝐿‘1) ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 337 | 283, 294,
335, 336 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿‘1) ∈ (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) |
| 338 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐿 =
(ℤRHom‘(ℤ/nℤ‘𝑅))) |
| 339 | | fvexd 6921 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤRHom‘(ℤ/nℤ‘𝑅)) ∈ V) |
| 340 | 338, 339 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐿 ∈ V) |
| 341 | 340 | imaexd 7938 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))) ∈ V) |
| 342 | 337, 341 | hashelne0d 14407 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬
(♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0)))) = 0) |
| 343 | 342 | neqned 2947 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≠ 0) |
| 344 | 26, 343 | jca 511 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ0 ∧ (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ≠ 0)) |
| 345 | | elnnne0 12540 |
. . . . . . . . . . . . . 14
⊢
((♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0)))) ∈ ℕ ↔
((♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0)))) ∈ ℕ0
∧ (♯‘(𝐿
“ (𝐸 “
(ℕ0 × ℕ0)))) ≠ 0)) |
| 346 | 344, 345 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℕ) |
| 347 | 346 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℝ+) |
| 348 | 347 | rpsqrtcld 15450 |
. . . . . . . . . . 11
⊢ (𝜑 →
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) ∈ ℝ+) |
| 349 | 49, 52, 348, 226 | ltmul1dd 13132 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) < ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 350 | 50, 51, 50, 51 | sqrtmuld 15463 |
. . . . . . . . . . 11
⊢ (𝜑 →
(√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = ((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 351 | 350 | eqcomd 2743 |
. . . . . . . . . 10
⊢ (𝜑 →
((√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) · (√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 352 | 349, 351 | breqtrd 5169 |
. . . . . . . . 9
⊢ (𝜑 → ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) < (√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) |
| 353 | 350, 222 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 →
(√‘((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) · (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) = (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 354 | 352, 353 | breqtrd 5169 |
. . . . . . . 8
⊢ (𝜑 → ((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 355 | | fllt 13846 |
. . . . . . . . 9
⊢ ((((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) ∈ ℝ ∧ (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ∈ ℤ) → (((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ↔ (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 356 | 53, 109, 355 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → (((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ↔ (⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 357 | 354, 356 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 358 | 54, 109 | zltp1led 41980 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) < (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) ↔ ((⌊‘((2 logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))))) |
| 359 | 357, 358 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) ≤ (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))) |
| 360 | 55 | renegcld 11690 |
. . . . . . 7
⊢ (𝜑 → -1 ∈
ℝ) |
| 361 | | df-neg 11495 |
. . . . . . . . 9
⊢ -1 = (0
− 1) |
| 362 | 361 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → -1 = (0 −
1)) |
| 363 | 4 | lem1d 12201 |
. . . . . . . 8
⊢ (𝜑 → (0 − 1) ≤
0) |
| 364 | 362, 363 | eqbrtrd 5165 |
. . . . . . 7
⊢ (𝜑 → -1 ≤
0) |
| 365 | 360, 4, 252, 364, 96 | letrd 11418 |
. . . . . 6
⊢ (𝜑 → -1 ≤
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁)))) |
| 366 | 84, 26, 99, 103, 359, 365 | bcle2d 42180 |
. . . . 5
⊢ (𝜑 → ((((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) +
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))))C(((⌊‘((2
logb 𝑁) ·
(√‘(♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0))))))) + 1) + -1)) ≤ (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1))) |
| 367 | 40, 107, 113, 273, 366 | ltletrd 11421 |
. . . 4
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1))) |
| 368 | 221, 239 | negsubd 11626 |
. . . . 5
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1) = ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1)) |
| 369 | 368 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + -1)) = (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1))) |
| 370 | 367, 369 | breqtrd 5169 |
. . 3
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1))) |
| 371 | | aks6d1c7lem1.9 |
. . . . . . 7
⊢ 𝐴 =
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) |
| 372 | 371 | eqcomi 2746 |
. . . . . 6
⊢
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) = 𝐴 |
| 373 | 372 | a1i 11 |
. . . . 5
⊢ (𝜑 →
(⌊‘((√‘(ϕ‘𝑅)) · (2 logb 𝑁))) = 𝐴) |
| 374 | 373 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁)))) =
((♯‘(𝐿 “
(𝐸 “
(ℕ0 × ℕ0)))) + 𝐴)) |
| 375 | 374 | oveq1d 7446 |
. . 3
⊢ (𝜑 → (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + (⌊‘((√‘(ϕ‘𝑅)) · (2 logb
𝑁))))C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1)) = (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + 𝐴)C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1))) |
| 376 | 370, 375 | breqtrd 5169 |
. 2
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + 𝐴)C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1))) |
| 377 | 18 | eqcomd 2743 |
. . . 4
⊢ (𝜑 → (♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) = 𝐷) |
| 378 | 377 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + 𝐴) = (𝐷 + 𝐴)) |
| 379 | 377 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1) = (𝐷 − 1)) |
| 380 | 378, 379 | oveq12d 7449 |
. 2
⊢ (𝜑 → (((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) + 𝐴)C((♯‘(𝐿 “ (𝐸 “ (ℕ0 ×
ℕ0)))) − 1)) = ((𝐷 + 𝐴)C(𝐷 − 1))) |
| 381 | 376, 380 | breqtrd 5169 |
1
⊢ (𝜑 → (𝑁↑(⌊‘(√‘𝐷))) < ((𝐷 + 𝐴)C(𝐷 − 1))) |