| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | aks4d1p1p5.1 | . 2
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 2 |  | aks4d1p1p5.2 | . 2
⊢ 𝐴 = ((𝑁↑(⌊‘(2 logb
𝐵))) · ∏𝑘 ∈ (1...(⌊‘((2
logb 𝑁)↑2)))((𝑁↑𝑘) − 1)) | 
| 3 |  | aks4d1p1p5.3 | . 2
⊢ 𝐵 = (⌈‘((2
logb 𝑁)↑5)) | 
| 4 |  | 3re 12346 | . . . 4
⊢ 3 ∈
ℝ | 
| 5 | 4 | a1i 11 | . . 3
⊢ (𝜑 → 3 ∈
ℝ) | 
| 6 |  | 4re 12350 | . . . 4
⊢ 4 ∈
ℝ | 
| 7 | 6 | a1i 11 | . . 3
⊢ (𝜑 → 4 ∈
ℝ) | 
| 8 | 1 | nnred 12281 | . . 3
⊢ (𝜑 → 𝑁 ∈ ℝ) | 
| 9 | 5 | lep1d 12199 | . . . 4
⊢ (𝜑 → 3 ≤ (3 +
1)) | 
| 10 |  | 3p1e4 12411 | . . . 4
⊢ (3 + 1) =
4 | 
| 11 | 9, 10 | breqtrdi 5184 | . . 3
⊢ (𝜑 → 3 ≤ 4) | 
| 12 |  | aks4d1p1p5.4 | . . 3
⊢ (𝜑 → 4 ≤ 𝑁) | 
| 13 | 5, 7, 8, 11, 12 | letrd 11418 | . 2
⊢ (𝜑 → 3 ≤ 𝑁) | 
| 14 |  | aks4d1p1p5.5 | . 2
⊢ 𝐶 = (2 logb (((2
logb 𝑁)↑5)
+ 1)) | 
| 15 |  | aks4d1p1p5.6 | . 2
⊢ 𝐷 = ((2 logb 𝑁)↑2) | 
| 16 |  | aks4d1p1p5.7 | . 2
⊢ 𝐸 = ((2 logb 𝑁)↑4) | 
| 17 |  | 2re 12340 | . . . . . . . 8
⊢ 2 ∈
ℝ | 
| 18 | 17 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℝ) | 
| 19 |  | 2pos 12369 | . . . . . . . . 9
⊢ 0 <
2 | 
| 20 | 19 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 2) | 
| 21 |  | elicc2 13452 | . . . . . . . . . . . . . . 15
⊢ ((4
∈ ℝ ∧ 𝑁
∈ ℝ) → (𝑥
∈ (4[,]𝑁) ↔
(𝑥 ∈ ℝ ∧ 4
≤ 𝑥 ∧ 𝑥 ≤ 𝑁))) | 
| 22 | 7, 8, 21 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))) | 
| 23 | 22 | biimpd 229 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))) | 
| 24 | 23 | imp 406 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)) | 
| 25 | 24 | simp1d 1143 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ) | 
| 26 |  | 0red 11264 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) | 
| 27 | 26 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ) | 
| 28 | 6 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈ ℝ) | 
| 29 |  | 4pos 12373 | . . . . . . . . . . . . 13
⊢ 0 <
4 | 
| 30 | 29 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 4) | 
| 31 | 24 | simp2d 1144 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥) | 
| 32 | 27, 28, 25, 30, 31 | ltletrd 11421 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥) | 
| 33 |  | 1red 11262 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℝ) | 
| 34 |  | 1lt2 12437 | . . . . . . . . . . . . . . 15
⊢ 1 <
2 | 
| 35 | 34 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 < 2) | 
| 36 | 33, 35 | ltned 11397 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≠ 2) | 
| 37 | 36 | necomd 2996 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 ≠ 1) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 1) | 
| 39 | 18, 20, 25, 32, 38 | relogbcld 41974 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈
ℝ) | 
| 40 |  | 5nn0 12546 | . . . . . . . . . . 11
⊢ 5 ∈
ℕ0 | 
| 41 | 40 | a1i 11 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈
ℕ0) | 
| 42 | 39, 41 | reexpcld 14203 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑5) ∈
ℝ) | 
| 43 |  | 1red 11262 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈ ℝ) | 
| 44 | 42, 43 | readdcld 11290 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (((2 logb 𝑥)↑5) + 1) ∈
ℝ) | 
| 45 | 27, 43 | readdcld 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) ∈
ℝ) | 
| 46 | 27 | ltp1d 12198 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (0 + 1)) | 
| 47 | 41 | nn0zd 12639 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 5 ∈ ℤ) | 
| 48 |  | ax-resscn 11212 | . . . . . . . . . . . . . 14
⊢ ℝ
⊆ ℂ | 
| 49 | 48, 18 | sselid 3981 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℂ) | 
| 50 | 27, 20 | gtned 11396 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ≠ 0) | 
| 51 |  | logb1 26812 | . . . . . . . . . . . . 13
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) =
0) | 
| 52 | 49, 50, 38, 51 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) =
0) | 
| 53 |  | 1lt4 12442 | . . . . . . . . . . . . . . 15
⊢ 1 <
4 | 
| 54 | 53 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 4) | 
| 55 | 43, 28, 25, 54, 31 | ltletrd 11421 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 < 𝑥) | 
| 56 |  | 2z 12649 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ | 
| 57 | 56 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈ ℤ) | 
| 58 | 57 | uzidd 12894 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 2 ∈
(ℤ≥‘2)) | 
| 59 |  | 1rp 13038 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ+ | 
| 60 | 59 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 1 ∈
ℝ+) | 
| 61 | 25, 32 | elrpd 13074 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ ℝ+) | 
| 62 |  | logblt 26827 | . . . . . . . . . . . . . 14
⊢ ((2
∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (1 < 𝑥 ↔ (2 logb 1) < (2
logb 𝑥))) | 
| 63 | 58, 60, 61, 62 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (1 < 𝑥 ↔ (2 logb 1) < (2
logb 𝑥))) | 
| 64 | 55, 63 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 1) < (2
logb 𝑥)) | 
| 65 | 52, 64 | eqbrtrrd 5167 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (2 logb 𝑥)) | 
| 66 |  | expgt0 14136 | . . . . . . . . . . 11
⊢ (((2
logb 𝑥) ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑥)) → 0 < ((2
logb 𝑥)↑5)) | 
| 67 | 39, 47, 65, 66 | syl3anc 1373 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < ((2 logb 𝑥)↑5)) | 
| 68 | 27, 42, 43, 67 | ltadd1dd 11874 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (0 + 1) < (((2 logb
𝑥)↑5) +
1)) | 
| 69 | 27, 45, 44, 46, 68 | lttrd 11422 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < (((2 logb 𝑥)↑5) + 1)) | 
| 70 | 18, 20, 44, 69, 38 | relogbcld 41974 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb (((2
logb 𝑥)↑5)
+ 1)) ∈ ℝ) | 
| 71 | 18, 70 | remulcld 11291 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) ∈
ℝ) | 
| 72 |  | 0red 11264 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 ∈ ℝ) | 
| 73 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 𝑥 ∈ (4[,]𝑁)) | 
| 74 | 7, 8 | jca 511 | . . . . . . . . . . . . 13
⊢ (𝜑 → (4 ∈ ℝ ∧
𝑁 ∈
ℝ)) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (4 ∈ ℝ ∧ 𝑁 ∈
ℝ)) | 
| 76 | 75, 21 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ (4[,]𝑁) ↔ (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁))) | 
| 77 | 73, 76 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (𝑥 ∈ ℝ ∧ 4 ≤ 𝑥 ∧ 𝑥 ≤ 𝑁)) | 
| 78 | 77 | simp2d 1144 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ≤ 𝑥) | 
| 79 | 72, 28, 25, 30, 78 | ltletrd 11421 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 0 < 𝑥) | 
| 80 | 18, 20, 25, 79, 38 | relogbcld 41974 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → (2 logb 𝑥) ∈
ℝ) | 
| 81 | 80 | resqcld 14165 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑2) ∈
ℝ) | 
| 82 | 71, 81 | readdcld 11290 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈
ℝ) | 
| 83 | 82 | fmpttd 7135 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ) | 
| 84 | 48 | a1i 11 | . . . . 5
⊢ (𝜑 → ℝ ⊆
ℂ) | 
| 85 |  | 3lt4 12440 | . . . . . . . . . . 11
⊢ 3 <
4 | 
| 86 | 85 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 3 < 4) | 
| 87 | 8, 33 | readdcld 11290 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ ℝ) | 
| 88 | 8 | ltp1d 12198 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 < (𝑁 + 1)) | 
| 89 | 7, 8, 87, 12, 88 | lelttrd 11419 | . . . . . . . . . 10
⊢ (𝜑 → 4 < (𝑁 + 1)) | 
| 90 | 86, 89 | jca 511 | . . . . . . . . 9
⊢ (𝜑 → (3 < 4 ∧ 4 <
(𝑁 + 1))) | 
| 91 | 5 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 3 ∈
ℝ*) | 
| 92 | 87 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 1) ∈
ℝ*) | 
| 93 | 7 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 4 ∈
ℝ*) | 
| 94 |  | elioo5 13444 | . . . . . . . . . 10
⊢ ((3
∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 4
∈ ℝ*) → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4 < (𝑁 + 1)))) | 
| 95 | 91, 92, 93, 94 | syl3anc 1373 | . . . . . . . . 9
⊢ (𝜑 → (4 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 4 ∧ 4
< (𝑁 +
1)))) | 
| 96 | 90, 95 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 4 ∈ (3(,)(𝑁 + 1))) | 
| 97 | 5, 7, 8, 86, 12 | ltletrd 11421 | . . . . . . . . . 10
⊢ (𝜑 → 3 < 𝑁) | 
| 98 | 97, 88 | jca 511 | . . . . . . . . 9
⊢ (𝜑 → (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1))) | 
| 99 | 8 | rexrd 11311 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℝ*) | 
| 100 |  | elioo5 13444 | . . . . . . . . . 10
⊢ ((3
∈ ℝ* ∧ (𝑁 + 1) ∈ ℝ* ∧ 𝑁 ∈ ℝ*)
→ (𝑁 ∈
(3(,)(𝑁 + 1)) ↔ (3
< 𝑁 ∧ 𝑁 < (𝑁 + 1)))) | 
| 101 | 91, 92, 99, 100 | syl3anc 1373 | . . . . . . . . 9
⊢ (𝜑 → (𝑁 ∈ (3(,)(𝑁 + 1)) ↔ (3 < 𝑁 ∧ 𝑁 < (𝑁 + 1)))) | 
| 102 | 98, 101 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (3(,)(𝑁 + 1))) | 
| 103 |  | iccssioo2 13460 | . . . . . . . 8
⊢ ((4
∈ (3(,)(𝑁 + 1)) ∧
𝑁 ∈ (3(,)(𝑁 + 1))) → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1))) | 
| 104 | 96, 102, 103 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (4[,]𝑁) ⊆ (3(,)(𝑁 + 1))) | 
| 105 | 104 | resmptd 6058 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) | 
| 106 |  | 2cnd 12344 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈
ℂ) | 
| 107 | 17 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈
ℝ) | 
| 108 | 19 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 2) | 
| 109 |  | elioore 13417 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 𝑥 ∈ ℝ) | 
| 110 | 109 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ) | 
| 111 |  | 0red 11264 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 ∈
ℝ) | 
| 112 | 4 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 ∈
ℝ) | 
| 113 |  | 3pos 12371 | . . . . . . . . . . . . . . . . . . 19
⊢ 0 <
3 | 
| 114 | 113 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 3) | 
| 115 |  | eliooord 13446 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → (3 < 𝑥 ∧ 𝑥 < (𝑁 + 1))) | 
| 116 |  | simpl 482 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((3 <
𝑥 ∧ 𝑥 < (𝑁 + 1)) → 3 < 𝑥) | 
| 117 | 115, 116 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) → 3 < 𝑥) | 
| 118 | 117 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 3 < 𝑥) | 
| 119 | 111, 112,
110, 114, 118 | lttrd 11422 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < 𝑥) | 
| 120 | 37 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1) | 
| 121 | 107, 108,
110, 119, 120 | relogbcld 41974 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈
ℝ) | 
| 122 | 40 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈
ℕ0) | 
| 123 | 121, 122 | reexpcld 14203 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈
ℝ) | 
| 124 |  | 1red 11262 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈
ℝ) | 
| 125 | 123, 124 | readdcld 11290 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈
ℝ) | 
| 126 | 111, 124 | readdcld 11290 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) ∈
ℝ) | 
| 127 | 111 | ltp1d 12198 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (0 +
1)) | 
| 128 | 122 | nn0zd 12639 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈
ℤ) | 
| 129 | 34 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 2) | 
| 130 |  | 2lt3 12438 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 2 <
3 | 
| 131 | 130 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 < 3) | 
| 132 | 124, 107,
112, 129, 131 | lttrd 11422 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 3) | 
| 133 | 124, 112,
110, 132, 118 | lttrd 11422 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 < 𝑥) | 
| 134 | 110, 119 | elrpd 13074 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℝ+) | 
| 135 |  | 2rp 13039 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
ℝ+ | 
| 136 | 135 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈
ℝ+) | 
| 137 | 134, 136,
129 | jca32 515 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 ∈ ℝ+ ∧ (2 ∈
ℝ+ ∧ 1 < 2))) | 
| 138 |  | logbgt0b 26836 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2
logb 𝑥) ↔ 1
< 𝑥)) | 
| 139 | 137, 138 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 < (2 logb
𝑥) ↔ 1 < 𝑥)) | 
| 140 | 133, 139 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (2 logb
𝑥)) | 
| 141 | 121, 128,
140, 66 | syl3anc 1373 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < ((2 logb
𝑥)↑5)) | 
| 142 | 111, 123,
124, 141 | ltadd1dd 11874 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (0 + 1) < (((2
logb 𝑥)↑5)
+ 1)) | 
| 143 | 111, 126,
125, 127, 142 | lttrd 11422 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 0 < (((2 logb
𝑥)↑5) +
1)) | 
| 144 | 124, 129 | ltned 11397 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ≠ 2) | 
| 145 | 144 | necomd 2996 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 1) | 
| 146 | 107, 108,
125, 143, 145 | relogbcld 41974 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2
logb 𝑥)↑5)
+ 1)) ∈ ℝ) | 
| 147 | 146 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb (((2
logb 𝑥)↑5)
+ 1)) ∈ ℂ) | 
| 148 | 106, 147 | mulcld 11281 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · (2
logb (((2 logb 𝑥)↑5) + 1))) ∈
ℂ) | 
| 149 | 48, 121 | sselid 3981 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 logb 𝑥) ∈
ℂ) | 
| 150 | 149 | sqcld 14184 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑2) ∈
ℂ) | 
| 151 | 148, 150 | addcld 11280 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) ∈
ℂ) | 
| 152 | 151 | fmpttd 7135 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 +
1))⟶ℂ) | 
| 153 |  | ioossre 13448 | . . . . . . . . . 10
⊢
(3(,)(𝑁 + 1))
⊆ ℝ | 
| 154 | 153 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → (3(,)(𝑁 + 1)) ⊆ ℝ) | 
| 155 | 84, 152, 154 | 3jca 1129 | . . . . . . . 8
⊢ (𝜑 → (ℝ ⊆ ℂ
∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧
(3(,)(𝑁 + 1)) ⊆
ℝ)) | 
| 156 | 136 | relogcld 26665 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈
ℝ) | 
| 157 | 125, 156 | remulcld 11291 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) ·
(log‘2)) ∈ ℝ) | 
| 158 | 48, 123 | sselid 3981 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑5) ∈
ℂ) | 
| 159 |  | 1cnd 11256 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 1 ∈
ℂ) | 
| 160 | 158, 159 | addcld 11280 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ∈
ℂ) | 
| 161 | 111, 108 | gtned 11396 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ≠ 0) | 
| 162 | 106, 161 | logcld 26612 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ∈
ℂ) | 
| 163 | 111, 143 | gtned 11396 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((2 logb 𝑥)↑5) + 1) ≠
0) | 
| 164 |  | loggt0b 26674 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
ℝ+ → (0 < (log‘2) ↔ 1 <
2)) | 
| 165 | 135, 164 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (0 <
(log‘2) ↔ 1 < 2) | 
| 166 | 35, 165 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 0 <
(log‘2)) | 
| 167 | 26, 166 | ltned 11397 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ≠
(log‘2)) | 
| 168 | 167 | necomd 2996 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (log‘2) ≠
0) | 
| 169 | 168 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘2) ≠
0) | 
| 170 | 160, 162,
163, 169 | mulne0d 11915 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((((2 logb 𝑥)↑5) + 1) ·
(log‘2)) ≠ 0) | 
| 171 | 124, 157,
170 | redivcld 12095 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / ((((2 logb
𝑥)↑5) + 1) ·
(log‘2))) ∈ ℝ) | 
| 172 |  | 5re 12353 | . . . . . . . . . . . . . . . . . . 19
⊢ 5 ∈
ℝ | 
| 173 | 172 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 5 ∈
ℝ) | 
| 174 |  | 4nn0 12545 | . . . . . . . . . . . . . . . . . . . 20
⊢ 4 ∈
ℕ0 | 
| 175 | 174 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈
ℕ0) | 
| 176 | 121, 175 | reexpcld 14203 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈
ℝ) | 
| 177 | 173, 176 | remulcld 11291 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (5 · ((2
logb 𝑥)↑4))
∈ ℝ) | 
| 178 | 110, 156 | remulcld 11291 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ∈
ℝ) | 
| 179 | 48, 110 | sselid 3981 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ∈ ℂ) | 
| 180 | 111, 119 | gtned 11396 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 𝑥 ≠ 0) | 
| 181 | 179, 162,
180, 169 | mulne0d 11915 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (𝑥 · (log‘2)) ≠
0) | 
| 182 | 124, 178,
181 | redivcld 12095 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (1 / (𝑥 · (log‘2))) ∈
ℝ) | 
| 183 | 177, 182 | remulcld 11291 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((5 · ((2
logb 𝑥)↑4))
· (1 / (𝑥 ·
(log‘2)))) ∈ ℝ) | 
| 184 | 183, 111 | readdcld 11290 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((5 · ((2
logb 𝑥)↑4))
· (1 / (𝑥 ·
(log‘2)))) + 0) ∈ ℝ) | 
| 185 | 171, 184 | remulcld 11291 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((1 / ((((2 logb
𝑥)↑5) + 1) ·
(log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈
ℝ) | 
| 186 | 107, 185 | remulcld 11291 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) ∈ ℝ) | 
| 187 | 156 | resqcld 14165 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ∈
ℝ) | 
| 188 | 56 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 2 ∈
ℤ) | 
| 189 | 162, 169,
188 | expne0d 14192 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑2) ≠
0) | 
| 190 | 107, 187,
189 | redivcld 12095 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 / ((log‘2)↑2))
∈ ℝ) | 
| 191 | 134 | relogcld 26665 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (log‘𝑥) ∈ ℝ) | 
| 192 |  | 2m1e1 12392 | . . . . . . . . . . . . . . . . . 18
⊢ (2
− 1) = 1 | 
| 193 |  | 1nn0 12542 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ0 | 
| 194 | 192, 193 | eqeltri 2837 | . . . . . . . . . . . . . . . . 17
⊢ (2
− 1) ∈ ℕ0 | 
| 195 | 194 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (2 − 1) ∈
ℕ0) | 
| 196 | 191, 195 | reexpcld 14203 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(2 − 1)) ∈
ℝ) | 
| 197 | 196, 110,
180 | redivcld 12095 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈
ℝ) | 
| 198 | 190, 197 | remulcld 11291 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ) | 
| 199 | 186, 198 | readdcld 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ) | 
| 200 | 199 | ralrimiva 3146 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ) | 
| 201 |  | nfcv 2905 | . . . . . . . . . . . 12
⊢
Ⅎ𝑥(3(,)(𝑁 + 1)) | 
| 202 | 201 | fnmptf 6704 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
(3(,)(𝑁 + 1))((2 ·
((1 / ((((2 logb 𝑥)↑5) + 1) · (log‘2)))
· (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0))) + ((2 /
((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ∈ ℝ → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))) Fn (3(,)(𝑁 + 1))) | 
| 203 | 200, 202 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))) Fn (3(,)(𝑁 + 1))) | 
| 204 | 5 | leidd 11829 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ≤ 3) | 
| 205 | 8 | lep1d 12199 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ≤ (𝑁 + 1)) | 
| 206 | 5, 8, 87, 13, 205 | letrd 11418 | . . . . . . . . . . . 12
⊢ (𝜑 → 3 ≤ (𝑁 + 1)) | 
| 207 | 5, 87, 204, 206 | aks4d1p1p6 42074 | . . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))))) | 
| 208 | 207 | fneq1d 6661 | . . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) Fn (3(,)(𝑁 + 1)) ↔ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥)))) Fn (3(,)(𝑁 + 1)))) | 
| 209 | 203, 208 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) Fn (3(,)(𝑁 + 1))) | 
| 210 | 209 | fndmd 6673 | . . . . . . . 8
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (3(,)(𝑁 + 1))) | 
| 211 |  | dvcn 25957 | . . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(3(,)(𝑁 + 1))⟶ℂ ∧
(3(,)(𝑁 + 1)) ⊆
ℝ) ∧ dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (3(,)(𝑁 + 1))) → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ)) | 
| 212 | 155, 210,
211 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ)) | 
| 213 |  | rescncf 24923 | . . . . . . . 8
⊢
((4[,]𝑁) ⊆
(3(,)(𝑁 + 1)) →
((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))) | 
| 214 | 104, 213 | syl 17 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))) | 
| 215 | 212, 214 | mpd 15 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)) | 
| 216 | 105, 215 | eqeltrrd 2842 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ)) | 
| 217 |  | cncfcdm 24924 | . . . . 5
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ (4[,]𝑁) ↦ ((2
· (2 logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ)) | 
| 218 | 84, 216, 217 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))):(4[,]𝑁)⟶ℝ)) | 
| 219 | 83, 218 | mpbird 257 | . . 3
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2))) ∈ ((4[,]𝑁)–cn→ℝ)) | 
| 220 | 174 | a1i 11 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → 4 ∈
ℕ0) | 
| 221 | 39, 220 | reexpcld 14203 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (4[,]𝑁)) → ((2 logb 𝑥)↑4) ∈
ℝ) | 
| 222 | 221 | fmpttd 7135 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ) | 
| 223 | 104 | resmptd 6058 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) = (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4))) | 
| 224 | 48, 176 | sselid 3981 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((2 logb 𝑥)↑4) ∈
ℂ) | 
| 225 | 224 | fmpttd 7135 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 +
1))⟶ℂ) | 
| 226 | 84, 225, 154 | 3jca 1129 | . . . . . . . 8
⊢ (𝜑 → (ℝ ⊆ ℂ
∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2
logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧ (3(,)(𝑁 + 1)) ⊆
ℝ)) | 
| 227 | 6 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈
ℝ) | 
| 228 | 156, 175 | reexpcld 14203 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ∈
ℝ) | 
| 229 |  | 4z 12651 | . . . . . . . . . . . . . . . 16
⊢ 4 ∈
ℤ | 
| 230 | 229 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → 4 ∈
ℤ) | 
| 231 | 162, 169,
230 | expne0d 14192 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘2)↑4) ≠
0) | 
| 232 | 227, 228,
231 | redivcld 12095 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 / ((log‘2)↑4))
∈ ℝ) | 
| 233 |  | 4m1e3 12395 | . . . . . . . . . . . . . . . . 17
⊢ (4
− 1) = 3 | 
| 234 |  | 3nn0 12544 | . . . . . . . . . . . . . . . . 17
⊢ 3 ∈
ℕ0 | 
| 235 | 233, 234 | eqeltri 2837 | . . . . . . . . . . . . . . . 16
⊢ (4
− 1) ∈ ℕ0 | 
| 236 | 235 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (4 − 1) ∈
ℕ0) | 
| 237 | 191, 236 | reexpcld 14203 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((log‘𝑥)↑(4 − 1)) ∈
ℝ) | 
| 238 | 237, 110,
180 | redivcld 12095 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → (((log‘𝑥)↑(4 − 1)) / 𝑥) ∈
ℝ) | 
| 239 | 232, 238 | remulcld 11291 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (3(,)(𝑁 + 1))) → ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ) | 
| 240 | 239 | ralrimiva 3146 | . . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ (3(,)(𝑁 + 1))((4 / ((log‘2)↑4)) ·
(((log‘𝑥)↑(4
− 1)) / 𝑥)) ∈
ℝ) | 
| 241 | 201 | fnmptf 6704 | . . . . . . . . . . 11
⊢
(∀𝑥 ∈
(3(,)(𝑁 + 1))((4 /
((log‘2)↑4)) · (((log‘𝑥)↑(4 − 1)) / 𝑥)) ∈ ℝ → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) Fn (3(,)(𝑁 + 1))) | 
| 242 | 240, 241 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) Fn (3(,)(𝑁 + 1))) | 
| 243 | 113 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < 3) | 
| 244 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) | 
| 245 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) | 
| 246 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (4 /
((log‘2)↑4)) = (4 / ((log‘2)↑4)) | 
| 247 |  | 4nn 12349 | . . . . . . . . . . . . 13
⊢ 4 ∈
ℕ | 
| 248 | 247 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 4 ∈
ℕ) | 
| 249 | 5, 87, 243, 206, 244, 245, 246, 248 | dvrelogpow2b 42069 | . . . . . . . . . . 11
⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥)))) | 
| 250 | 249 | fneq1d 6661 | . . . . . . . . . 10
⊢ (𝜑 → ((ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) Fn (3(,)(𝑁 + 1)) ↔ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) Fn (3(,)(𝑁 + 1)))) | 
| 251 | 242, 250 | mpbird 257 | . . . . . . . . 9
⊢ (𝜑 → (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) Fn (3(,)(𝑁 + 1))) | 
| 252 | 251 | fndmd 6673 | . . . . . . . 8
⊢ (𝜑 → dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (3(,)(𝑁 + 1))) | 
| 253 |  | dvcn 25957 | . . . . . . . 8
⊢
(((ℝ ⊆ ℂ ∧ (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)):(3(,)(𝑁 + 1))⟶ℂ ∧
(3(,)(𝑁 + 1)) ⊆
ℝ) ∧ dom (ℝ D (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4))) = (3(,)(𝑁 + 1))) → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ)) | 
| 254 | 226, 252,
253 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ)) | 
| 255 |  | rescncf 24923 | . . . . . . . 8
⊢
((4[,]𝑁) ⊆
(3(,)(𝑁 + 1)) →
((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2
logb 𝑥)↑4))
∈ ((3(,)(𝑁 +
1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))) | 
| 256 | 104, 255 | syl 17 | . . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ∈ ((3(,)(𝑁 + 1))–cn→ℂ) → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ))) | 
| 257 | 254, 256 | mpd 15 | . . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (3(,)(𝑁 + 1)) ↦ ((2 logb 𝑥)↑4)) ↾ (4[,]𝑁)) ∈ ((4[,]𝑁)–cn→ℂ)) | 
| 258 | 223, 257 | eqeltrrd 2842 | . . . . 5
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℂ)) | 
| 259 |  | cncfcdm 24924 | . . . . 5
⊢ ((ℝ
⊆ ℂ ∧ (𝑥
∈ (4[,]𝑁) ↦ ((2
logb 𝑥)↑4))
∈ ((4[,]𝑁)–cn→ℂ)) → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ)) | 
| 260 | 84, 258, 259 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ) ↔ (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)):(4[,]𝑁)⟶ℝ)) | 
| 261 | 222, 260 | mpbird 257 | . . 3
⊢ (𝜑 → (𝑥 ∈ (4[,]𝑁) ↦ ((2 logb 𝑥)↑4)) ∈ ((4[,]𝑁)–cn→ℝ)) | 
| 262 | 7, 8, 11, 12 | aks4d1p1p6 42074 | . . 3
⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))))) | 
| 263 | 29 | a1i 11 | . . . . 5
⊢ (𝜑 → 0 < 4) | 
| 264 |  | eqid 2737 | . . . . 5
⊢ (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4)) = (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4)) | 
| 265 |  | eqid 2737 | . . . . 5
⊢ (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) | 
| 266 | 7, 8, 263, 12, 264, 265, 246, 248 | dvrelogpow2b 42069 | . . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥)))) | 
| 267 | 233 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (4 − 1) =
3) | 
| 268 | 267 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((log‘𝑥)↑(4 − 1)) = ((log‘𝑥)↑3)) | 
| 269 | 268 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → (((log‘𝑥)↑(4 − 1)) / 𝑥) = (((log‘𝑥)↑3) / 𝑥)) | 
| 270 | 269 | oveq2d 7447 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥)) = ((4 / ((log‘2)↑4)) ·
(((log‘𝑥)↑3) /
𝑥))) | 
| 271 | 270 | mpteq2dva 5242 | . . . 4
⊢ (𝜑 → (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑(4 − 1)) / 𝑥))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑3) / 𝑥)))) | 
| 272 | 266, 271 | eqtrd 2777 | . . 3
⊢ (𝜑 → (ℝ D (𝑥 ∈ (4(,)𝑁) ↦ ((2 logb 𝑥)↑4))) = (𝑥 ∈ (4(,)𝑁) ↦ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑3) / 𝑥)))) | 
| 273 |  | elioore 13417 | . . . . 5
⊢ (𝑥 ∈ (4(,)𝑁) → 𝑥 ∈ ℝ) | 
| 274 | 273 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 𝑥 ∈ ℝ) | 
| 275 | 6 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ∈ ℝ) | 
| 276 |  | eliooord 13446 | . . . . . . 7
⊢ (𝑥 ∈ (4(,)𝑁) → (4 < 𝑥 ∧ 𝑥 < 𝑁)) | 
| 277 | 276 | simpld 494 | . . . . . 6
⊢ (𝑥 ∈ (4(,)𝑁) → 4 < 𝑥) | 
| 278 | 277 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 < 𝑥) | 
| 279 | 275, 274,
278 | ltled 11409 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → 4 ≤ 𝑥) | 
| 280 | 274, 279 | aks4d1p1p7 42075 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (4(,)𝑁)) → ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))) ≤ ((4 / ((log‘2)↑4))
· (((log‘𝑥)↑3) / 𝑥))) | 
| 281 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑥 = 4 → (2 logb
𝑥) = (2 logb
4)) | 
| 282 | 281 | oveq1d 7446 | . . . . . . 7
⊢ (𝑥 = 4 → ((2 logb
𝑥)↑5) = ((2
logb 4)↑5)) | 
| 283 | 282 | oveq1d 7446 | . . . . . 6
⊢ (𝑥 = 4 → (((2 logb
𝑥)↑5) + 1) = (((2
logb 4)↑5) + 1)) | 
| 284 | 283 | oveq2d 7447 | . . . . 5
⊢ (𝑥 = 4 → (2 logb
(((2 logb 𝑥)↑5) + 1)) = (2 logb (((2
logb 4)↑5) + 1))) | 
| 285 | 284 | oveq2d 7447 | . . . 4
⊢ (𝑥 = 4 → (2 · (2
logb (((2 logb 𝑥)↑5) + 1))) = (2 · (2
logb (((2 logb 4)↑5) + 1)))) | 
| 286 | 281 | oveq1d 7446 | . . . 4
⊢ (𝑥 = 4 → ((2 logb
𝑥)↑2) = ((2
logb 4)↑2)) | 
| 287 | 285, 286 | oveq12d 7449 | . . 3
⊢ (𝑥 = 4 → ((2 · (2
logb (((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)) = ((2 · (2
logb (((2 logb 4)↑5) + 1))) + ((2 logb
4)↑2))) | 
| 288 | 281 | oveq1d 7446 | . . 3
⊢ (𝑥 = 4 → ((2 logb
𝑥)↑4) = ((2
logb 4)↑4)) | 
| 289 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = 𝑁 → (2 logb 𝑥) = (2 logb 𝑁)) | 
| 290 | 289 | oveq1d 7446 | . . . . . . . 8
⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑5) = ((2 logb
𝑁)↑5)) | 
| 291 | 290 | oveq1d 7446 | . . . . . . 7
⊢ (𝑥 = 𝑁 → (((2 logb 𝑥)↑5) + 1) = (((2
logb 𝑁)↑5)
+ 1)) | 
| 292 | 291 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑁 → (2 logb (((2
logb 𝑥)↑5)
+ 1)) = (2 logb (((2 logb 𝑁)↑5) + 1))) | 
| 293 | 292 | oveq2d 7447 | . . . . 5
⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2
logb 𝑥)↑5)
+ 1))) = (2 · (2 logb (((2 logb 𝑁)↑5) + 1)))) | 
| 294 | 14 | a1i 11 | . . . . . . 7
⊢ (𝑥 = 𝑁 → 𝐶 = (2 logb (((2 logb
𝑁)↑5) +
1))) | 
| 295 | 294 | oveq2d 7447 | . . . . . 6
⊢ (𝑥 = 𝑁 → (2 · 𝐶) = (2 · (2 logb (((2
logb 𝑁)↑5)
+ 1)))) | 
| 296 | 295 | eqcomd 2743 | . . . . 5
⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2
logb 𝑁)↑5)
+ 1))) = (2 · 𝐶)) | 
| 297 | 293, 296 | eqtrd 2777 | . . . 4
⊢ (𝑥 = 𝑁 → (2 · (2 logb (((2
logb 𝑥)↑5)
+ 1))) = (2 · 𝐶)) | 
| 298 | 289 | oveq1d 7446 | . . . . 5
⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = ((2 logb
𝑁)↑2)) | 
| 299 | 15 | a1i 11 | . . . . . 6
⊢ (𝑥 = 𝑁 → 𝐷 = ((2 logb 𝑁)↑2)) | 
| 300 | 299 | eqcomd 2743 | . . . . 5
⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑2) = 𝐷) | 
| 301 | 298, 300 | eqtrd 2777 | . . . 4
⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑2) = 𝐷) | 
| 302 | 297, 301 | oveq12d 7449 | . . 3
⊢ (𝑥 = 𝑁 → ((2 · (2 logb (((2
logb 𝑥)↑5)
+ 1))) + ((2 logb 𝑥)↑2)) = ((2 · 𝐶) + 𝐷)) | 
| 303 | 289 | oveq1d 7446 | . . . 4
⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = ((2 logb
𝑁)↑4)) | 
| 304 | 16 | a1i 11 | . . . . 5
⊢ (𝑥 = 𝑁 → 𝐸 = ((2 logb 𝑁)↑4)) | 
| 305 | 304 | eqcomd 2743 | . . . 4
⊢ (𝑥 = 𝑁 → ((2 logb 𝑁)↑4) = 𝐸) | 
| 306 | 303, 305 | eqtrd 2777 | . . 3
⊢ (𝑥 = 𝑁 → ((2 logb 𝑥)↑4) = 𝐸) | 
| 307 |  | sq2 14236 | . . . . . . . . . . . . . . . 16
⊢
(2↑2) = 4 | 
| 308 | 307 | oveq2i 7442 | . . . . . . . . . . . . . . 15
⊢ (2
logb (2↑2)) = (2 logb 4) | 
| 309 | 308 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb
(2↑2)) = (2 logb 4)) | 
| 310 | 309 | eqcomd 2743 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb 4) = (2
logb (2↑2))) | 
| 311 | 135 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℝ+) | 
| 312 | 56 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 2 ∈
ℤ) | 
| 313 |  | relogbexp 26823 | . . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ+ ∧ 2 ≠ 1 ∧ 2 ∈ ℤ) → (2
logb (2↑2)) = 2) | 
| 314 | 311, 37, 312, 313 | syl3anc 1373 | . . . . . . . . . . . . 13
⊢ (𝜑 → (2 logb
(2↑2)) = 2) | 
| 315 | 310, 314 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ (𝜑 → (2 logb 4) =
2) | 
| 316 | 315 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝜑 → ((2 logb
4)↑5) = (2↑5)) | 
| 317 | 316 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → (((2 logb
4)↑5) + 1) = ((2↑5) + 1)) | 
| 318 | 317 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → (2 logb (((2
logb 4)↑5) + 1)) = (2 logb ((2↑5) +
1))) | 
| 319 | 17 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ) | 
| 320 | 319 | leidd 11829 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ 2) | 
| 321 | 315, 319 | eqeltrd 2841 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2 logb 4)
∈ ℝ) | 
| 322 | 40 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 5 ∈
ℕ0) | 
| 323 | 321, 322 | reexpcld 14203 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2 logb
4)↑5) ∈ ℝ) | 
| 324 | 316, 323 | eqeltrrd 2842 | . . . . . . . . . . . 12
⊢ (𝜑 → (2↑5) ∈
ℝ) | 
| 325 | 324, 33 | readdcld 11290 | . . . . . . . . . . 11
⊢ (𝜑 → ((2↑5) + 1) ∈
ℝ) | 
| 326 | 322 | nn0zd 12639 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 5 ∈
ℤ) | 
| 327 | 19 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 < 2) | 
| 328 | 327, 315 | breqtrrd 5171 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 0 < (2 logb
4)) | 
| 329 | 321, 326,
328 | 3jca 1129 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 logb 4)
∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb
4))) | 
| 330 |  | expgt0 14136 | . . . . . . . . . . . . . 14
⊢ (((2
logb 4) ∈ ℝ ∧ 5 ∈ ℤ ∧ 0 < (2
logb 4)) → 0 < ((2 logb
4)↑5)) | 
| 331 | 329, 330 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((2 logb
4)↑5)) | 
| 332 | 331, 316 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 <
(2↑5)) | 
| 333 | 324 | ltp1d 12198 | . . . . . . . . . . . 12
⊢ (𝜑 → (2↑5) <
((2↑5) + 1)) | 
| 334 | 26, 324, 325, 332, 333 | lttrd 11422 | . . . . . . . . . . 11
⊢ (𝜑 → 0 < ((2↑5) +
1)) | 
| 335 |  | 6nn0 12547 | . . . . . . . . . . . . 13
⊢ 6 ∈
ℕ0 | 
| 336 | 335 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 6 ∈
ℕ0) | 
| 337 | 319, 336 | reexpcld 14203 | . . . . . . . . . . 11
⊢ (𝜑 → (2↑6) ∈
ℝ) | 
| 338 | 336 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ (𝜑 → 6 ∈
ℤ) | 
| 339 |  | expgt0 14136 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ 6 ∈ ℤ ∧ 0 < 2) → 0 <
(2↑6)) | 
| 340 | 319, 338,
327, 339 | syl3anc 1373 | . . . . . . . . . . 11
⊢ (𝜑 → 0 <
(2↑6)) | 
| 341 | 324, 324 | readdcld 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2↑5) + (2↑5))
∈ ℝ) | 
| 342 | 33, 319, 35 | ltled 11409 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ≤ 2) | 
| 343 | 319, 322,
342 | expge1d 14205 | . . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≤
(2↑5)) | 
| 344 | 33, 324, 324, 343 | leadd2dd 11878 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2↑5) + 1) ≤
((2↑5) + (2↑5))) | 
| 345 | 341 | leidd 11829 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2↑5) + (2↑5))
≤ ((2↑5) + (2↑5))) | 
| 346 |  | df-6 12333 | . . . . . . . . . . . . . . . . . . 19
⊢ 6 = (5 +
1) | 
| 347 | 346 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 6 = (5 +
1)) | 
| 348 | 347 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2↑6) = (2↑(5 +
1))) | 
| 349 |  | 2cn 12341 | . . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℂ | 
| 350 | 349 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 2 ∈
ℂ) | 
| 351 | 193 | a1i 11 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 352 | 350, 351,
322 | expaddd 14188 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2↑(5 + 1)) =
((2↑5) · (2↑1))) | 
| 353 | 348, 352 | eqtrd 2777 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑6) = ((2↑5)
· (2↑1))) | 
| 354 | 350 | exp1d 14181 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (2↑1) =
2) | 
| 355 | 354 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2↑5) ·
(2↑1)) = ((2↑5) · 2)) | 
| 356 | 353, 355 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (2↑6) = ((2↑5)
· 2)) | 
| 357 | 48, 324 | sselid 3981 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2↑5) ∈
ℂ) | 
| 358 | 357 | times2d 12510 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((2↑5) · 2) =
((2↑5) + (2↑5))) | 
| 359 | 356, 358 | eqtrd 2777 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (2↑6) = ((2↑5) +
(2↑5))) | 
| 360 | 359 | eqcomd 2743 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((2↑5) + (2↑5))
= (2↑6)) | 
| 361 | 345, 360 | breqtrd 5169 | . . . . . . . . . . . 12
⊢ (𝜑 → ((2↑5) + (2↑5))
≤ (2↑6)) | 
| 362 | 325, 341,
337, 344, 361 | letrd 11418 | . . . . . . . . . . 11
⊢ (𝜑 → ((2↑5) + 1) ≤
(2↑6)) | 
| 363 | 312, 320,
325, 334, 337, 340, 362 | logblebd 41977 | . . . . . . . . . 10
⊢ (𝜑 → (2 logb
((2↑5) + 1)) ≤ (2 logb (2↑6))) | 
| 364 | 311, 37, 338 | relogbexpd 41975 | . . . . . . . . . 10
⊢ (𝜑 → (2 logb
(2↑6)) = 6) | 
| 365 | 363, 364 | breqtrd 5169 | . . . . . . . . 9
⊢ (𝜑 → (2 logb
((2↑5) + 1)) ≤ 6) | 
| 366 | 318, 365 | eqbrtrd 5165 | . . . . . . . 8
⊢ (𝜑 → (2 logb (((2
logb 4)↑5) + 1)) ≤ 6) | 
| 367 |  | 6t2e12 12837 | . . . . . . . . 9
⊢ (6
· 2) = ;12 | 
| 368 |  | 6cn 12357 | . . . . . . . . . . 11
⊢ 6 ∈
ℂ | 
| 369 | 368 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 6 ∈
ℂ) | 
| 370 |  | 2nn 12339 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ | 
| 371 | 193, 370 | decnncl 12753 | . . . . . . . . . . . . 13
⊢ ;12 ∈ ℕ | 
| 372 | 371 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ;12 ∈ ℕ) | 
| 373 | 372 | nnred 12281 | . . . . . . . . . . 11
⊢ (𝜑 → ;12 ∈ ℝ) | 
| 374 | 373 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → ;12 ∈ ℂ) | 
| 375 | 26, 327 | gtned 11396 | . . . . . . . . . 10
⊢ (𝜑 → 2 ≠ 0) | 
| 376 | 369, 350,
374, 375 | ldiv 12101 | . . . . . . . . 9
⊢ (𝜑 → ((6 · 2) = ;12 ↔ 6 = (;12 / 2))) | 
| 377 | 367, 376 | mpbii 233 | . . . . . . . 8
⊢ (𝜑 → 6 = (;12 / 2)) | 
| 378 | 366, 377 | breqtrd 5169 | . . . . . . 7
⊢ (𝜑 → (2 logb (((2
logb 4)↑5) + 1)) ≤ (;12 / 2)) | 
| 379 | 323, 33 | readdcld 11290 | . . . . . . . . 9
⊢ (𝜑 → (((2 logb
4)↑5) + 1) ∈ ℝ) | 
| 380 | 26, 33 | readdcld 11290 | . . . . . . . . . 10
⊢ (𝜑 → (0 + 1) ∈
ℝ) | 
| 381 | 26 | ltp1d 12198 | . . . . . . . . . 10
⊢ (𝜑 → 0 < (0 +
1)) | 
| 382 | 26, 323, 33, 331 | ltadd1dd 11874 | . . . . . . . . . 10
⊢ (𝜑 → (0 + 1) < (((2
logb 4)↑5) + 1)) | 
| 383 | 26, 380, 379, 381, 382 | lttrd 11422 | . . . . . . . . 9
⊢ (𝜑 → 0 < (((2
logb 4)↑5) + 1)) | 
| 384 | 319, 327,
379, 383, 37 | relogbcld 41974 | . . . . . . . 8
⊢ (𝜑 → (2 logb (((2
logb 4)↑5) + 1)) ∈ ℝ) | 
| 385 | 384, 373,
311 | lemuldiv2d 13127 | . . . . . . 7
⊢ (𝜑 → ((2 · (2
logb (((2 logb 4)↑5) + 1))) ≤ ;12 ↔ (2 logb (((2 logb
4)↑5) + 1)) ≤ (;12 /
2))) | 
| 386 | 378, 385 | mpbird 257 | . . . . . 6
⊢ (𝜑 → (2 · (2
logb (((2 logb 4)↑5) + 1))) ≤ ;12) | 
| 387 | 315 | oveq1d 7446 | . . . . . . . . . 10
⊢ (𝜑 → ((2 logb
4)↑2) = (2↑2)) | 
| 388 | 387, 307 | eqtrdi 2793 | . . . . . . . . 9
⊢ (𝜑 → ((2 logb
4)↑2) = 4) | 
| 389 | 388 | oveq2d 7447 | . . . . . . . 8
⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = (;16 − 4)) | 
| 390 |  | 2nn0 12543 | . . . . . . . . . 10
⊢ 2 ∈
ℕ0 | 
| 391 |  | eqid 2737 | . . . . . . . . . 10
⊢ ;12 = ;12 | 
| 392 |  | 4cn 12351 | . . . . . . . . . . 11
⊢ 4 ∈
ℂ | 
| 393 |  | 4p2e6 12419 | . . . . . . . . . . 11
⊢ (4 + 2) =
6 | 
| 394 | 392, 349,
393 | addcomli 11453 | . . . . . . . . . 10
⊢ (2 + 4) =
6 | 
| 395 | 193, 390,
174, 391, 394 | decaddi 12793 | . . . . . . . . 9
⊢ (;12 + 4) = ;16 | 
| 396 | 392 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 4 ∈
ℂ) | 
| 397 |  | 6nn 12355 | . . . . . . . . . . . . . 14
⊢ 6 ∈
ℕ | 
| 398 | 193, 397 | decnncl 12753 | . . . . . . . . . . . . 13
⊢ ;16 ∈ ℕ | 
| 399 | 398 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → ;16 ∈ ℕ) | 
| 400 | 399 | nnred 12281 | . . . . . . . . . . 11
⊢ (𝜑 → ;16 ∈ ℝ) | 
| 401 | 48, 400 | sselid 3981 | . . . . . . . . . 10
⊢ (𝜑 → ;16 ∈ ℂ) | 
| 402 | 374, 396,
401 | addlsub 11679 | . . . . . . . . 9
⊢ (𝜑 → ((;12 + 4) = ;16 ↔ ;12 = (;16 − 4))) | 
| 403 | 395, 402 | mpbii 233 | . . . . . . . 8
⊢ (𝜑 → ;12 = (;16 − 4)) | 
| 404 | 389, 403 | eqtr4d 2780 | . . . . . . 7
⊢ (𝜑 → (;16 − ((2 logb 4)↑2)) = ;12) | 
| 405 | 404 | eqcomd 2743 | . . . . . 6
⊢ (𝜑 → ;12 = (;16 − ((2 logb
4)↑2))) | 
| 406 | 386, 405 | breqtrd 5169 | . . . . 5
⊢ (𝜑 → (2 · (2
logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb
4)↑2))) | 
| 407 | 319, 384 | remulcld 11291 | . . . . . 6
⊢ (𝜑 → (2 · (2
logb (((2 logb 4)↑5) + 1))) ∈
ℝ) | 
| 408 | 321 | resqcld 14165 | . . . . . 6
⊢ (𝜑 → ((2 logb
4)↑2) ∈ ℝ) | 
| 409 |  | leaddsub 11739 | . . . . . 6
⊢ (((2
· (2 logb (((2 logb 4)↑5) + 1))) ∈
ℝ ∧ ((2 logb 4)↑2) ∈ ℝ ∧ ;16 ∈ ℝ) → (((2 ·
(2 logb (((2 logb 4)↑5) + 1))) + ((2 logb
4)↑2)) ≤ ;16 ↔ (2
· (2 logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb
4)↑2)))) | 
| 410 | 407, 408,
400, 409 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → (((2 · (2
logb (((2 logb 4)↑5) + 1))) + ((2 logb
4)↑2)) ≤ ;16 ↔ (2
· (2 logb (((2 logb 4)↑5) + 1))) ≤ (;16 − ((2 logb
4)↑2)))) | 
| 411 | 406, 410 | mpbird 257 | . . . 4
⊢ (𝜑 → ((2 · (2
logb (((2 logb 4)↑5) + 1))) + ((2 logb
4)↑2)) ≤ ;16) | 
| 412 | 315 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → ((2 logb
4)↑4) = (2↑4)) | 
| 413 |  | 2exp4 17122 | . . . . . 6
⊢
(2↑4) = ;16 | 
| 414 | 412, 413 | eqtrdi 2793 | . . . . 5
⊢ (𝜑 → ((2 logb
4)↑4) = ;16) | 
| 415 | 414 | eqcomd 2743 | . . . 4
⊢ (𝜑 → ;16 = ((2 logb
4)↑4)) | 
| 416 | 411, 415 | breqtrd 5169 | . . 3
⊢ (𝜑 → ((2 · (2
logb (((2 logb 4)↑5) + 1))) + ((2 logb
4)↑2)) ≤ ((2 logb 4)↑4)) | 
| 417 | 7, 8, 219, 261, 262, 272, 280, 287, 288, 302, 306, 416, 12 | dvle2 42073 | . 2
⊢ (𝜑 → ((2 · 𝐶) + 𝐷) ≤ 𝐸) | 
| 418 | 1, 2, 3, 13, 14, 15, 16, 417 | aks4d1p1p4 42072 | 1
⊢ (𝜑 → 𝐴 < (2↑𝐵)) |