| Step | Hyp | Ref
| Expression |
| 1 | | reelprrecn 11247 |
. . 3
⊢ ℝ
∈ {ℝ, ℂ} |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
| 3 | | 2cnd 12344 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) |
| 4 | | 2re 12340 |
. . . . . 6
⊢ 2 ∈
ℝ |
| 5 | 4 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ) |
| 6 | | 2pos 12369 |
. . . . . 6
⊢ 0 <
2 |
| 7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 2) |
| 8 | | elioore 13417 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ) |
| 9 | 8 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ) |
| 10 | | 0red 11264 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) |
| 11 | | aks4d1p1p6.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 12 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) |
| 13 | | 3re 12346 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
| 14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 3 ∈ ℝ) |
| 15 | | 3pos 12371 |
. . . . . . . . . . 11
⊢ 0 <
3 |
| 16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 3) |
| 17 | | aks4d1p1p6.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 3 ≤ 𝐴) |
| 18 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 3 ≤ 𝐴) |
| 19 | 10, 14, 12, 16, 18 | ltletrd 11421 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 𝐴) |
| 20 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
| 21 | 11 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) |
| 23 | | aks4d1p1p6.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 24 | 23 | rexrd 11311 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) |
| 26 | 9 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ*) |
| 27 | | elioo5 13444 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ ℝ*) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
| 28 | 22, 25, 26, 27 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
| 29 | 20, 28 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
| 30 | 29 | simpld 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑥) |
| 31 | 10, 12, 9, 19, 30 | lttrd 11422 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 𝑥) |
| 32 | | 1red 11262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ) |
| 33 | | 1lt2 12437 |
. . . . . . . . . . 11
⊢ 1 <
2 |
| 34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 2) |
| 35 | 32, 34 | ltned 11397 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ≠ 2) |
| 36 | 35 | necomd 2996 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 1) |
| 37 | 5, 7, 9, 31, 36 | relogbcld 41974 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb 𝑥) ∈
ℝ) |
| 38 | | 5nn0 12546 |
. . . . . . . 8
⊢ 5 ∈
ℕ0 |
| 39 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈
ℕ0) |
| 40 | 37, 39 | reexpcld 14203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑5) ∈
ℝ) |
| 41 | 40, 32 | readdcld 11290 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ∈
ℝ) |
| 42 | 10, 32 | readdcld 11290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (0 + 1) ∈
ℝ) |
| 43 | 10 | ltp1d 12198 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (0 + 1)) |
| 44 | 39 | nn0zd 12639 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈ ℤ) |
| 45 | | 2cnd 12344 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ∈ ℂ) |
| 46 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 0 ∈ ℝ) |
| 47 | 6 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 0 < 2) |
| 48 | 46, 47 | ltned 11397 |
. . . . . . . . . . . 12
⊢ (⊤
→ 0 ≠ 2) |
| 49 | 48 | necomd 2996 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ≠ 0) |
| 50 | | 1red 11262 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1 ∈ ℝ) |
| 51 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1 < 2) |
| 52 | 50, 51 | ltned 11397 |
. . . . . . . . . . . 12
⊢ (⊤
→ 1 ≠ 2) |
| 53 | 52 | necomd 2996 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ≠ 1) |
| 54 | | logb1 26812 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) =
0) |
| 55 | 45, 49, 53, 54 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (⊤
→ (2 logb 1) = 0) |
| 56 | 55 | mptru 1547 |
. . . . . . . . 9
⊢ (2
logb 1) = 0 |
| 57 | | 2lt3 12438 |
. . . . . . . . . . . . . 14
⊢ 2 <
3 |
| 58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 < 3) |
| 59 | 32, 5, 14, 34, 58 | lttrd 11422 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 3) |
| 60 | 32, 14, 12, 59, 18 | ltletrd 11421 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 𝐴) |
| 61 | 32, 12, 9, 60, 30 | lttrd 11422 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 𝑥) |
| 62 | | 2z 12649 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
| 63 | 62 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ) |
| 64 | 63 | uzidd 12894 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈
(ℤ≥‘2)) |
| 65 | | 1rp 13038 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
| 66 | 65 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈
ℝ+) |
| 67 | 9, 31 | elrpd 13074 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ+) |
| 68 | | logblt 26827 |
. . . . . . . . . . 11
⊢ ((2
∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (1 < 𝑥 ↔ (2 logb 1) < (2
logb 𝑥))) |
| 69 | 64, 66, 67, 68 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 < 𝑥 ↔ (2 logb 1) < (2
logb 𝑥))) |
| 70 | 61, 69 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb 1) < (2
logb 𝑥)) |
| 71 | 56, 70 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (2 logb 𝑥)) |
| 72 | | expgt0 14136 |
. . . . . . . 8
⊢ (((2
logb 𝑥) ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑥)) → 0 < ((2
logb 𝑥)↑5)) |
| 73 | 37, 44, 71, 72 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < ((2 logb 𝑥)↑5)) |
| 74 | 10, 40, 32, 73 | ltadd1dd 11874 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (0 + 1) < (((2 logb
𝑥)↑5) +
1)) |
| 75 | 10, 42, 41, 43, 74 | lttrd 11422 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (((2 logb 𝑥)↑5) + 1)) |
| 76 | 5, 7, 41, 75, 36 | relogbcld 41974 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb (((2
logb 𝑥)↑5)
+ 1)) ∈ ℝ) |
| 77 | | recn 11245 |
. . . 4
⊢ ((2
logb (((2 logb 𝑥)↑5) + 1)) ∈ ℝ → (2
logb (((2 logb 𝑥)↑5) + 1)) ∈
ℂ) |
| 78 | 76, 77 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb (((2
logb 𝑥)↑5)
+ 1)) ∈ ℂ) |
| 79 | 3, 78 | mulcld 11281 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) ∈
ℂ) |
| 80 | | 2rp 13039 |
. . . . . . . 8
⊢ 2 ∈
ℝ+ |
| 81 | 80 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈
ℝ+) |
| 82 | 81 | relogcld 26665 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈
ℝ) |
| 83 | 41, 82 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((2 logb 𝑥)↑5) + 1) ·
(log‘2)) ∈ ℝ) |
| 84 | 40 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑5) ∈
ℂ) |
| 85 | | 1cnd 11256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈ ℂ) |
| 86 | 84, 85 | addcld 11280 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ∈
ℂ) |
| 87 | 7 | gt0ne0d 11827 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) |
| 88 | 3, 87 | logcld 26612 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈
ℂ) |
| 89 | 75 | gt0ne0d 11827 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ≠
0) |
| 90 | | 0red 11264 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
| 91 | | loggt0b 26674 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ+ → (0 < (log‘2) ↔ 1 <
2)) |
| 92 | 80, 91 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (0 <
(log‘2) ↔ 1 < 2) |
| 93 | 33, 92 | mpbir 231 |
. . . . . . . . . 10
⊢ 0 <
(log‘2) |
| 94 | 93 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 <
(log‘2)) |
| 95 | 90, 94 | ltned 11397 |
. . . . . . . 8
⊢ (𝜑 → 0 ≠
(log‘2)) |
| 96 | 95 | necomd 2996 |
. . . . . . 7
⊢ (𝜑 → (log‘2) ≠
0) |
| 97 | 96 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ≠
0) |
| 98 | 86, 88, 89, 97 | mulne0d 11915 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((2 logb 𝑥)↑5) + 1) ·
(log‘2)) ≠ 0) |
| 99 | 32, 83, 98 | redivcld 12095 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / ((((2 logb 𝑥)↑5) + 1) ·
(log‘2))) ∈ ℝ) |
| 100 | | 5re 12353 |
. . . . . . . 8
⊢ 5 ∈
ℝ |
| 101 | 100 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈ ℝ) |
| 102 | | 4nn0 12545 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
| 103 | 102 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 4 ∈
ℕ0) |
| 104 | 37, 103 | reexpcld 14203 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑4) ∈
ℝ) |
| 105 | 101, 104 | remulcld 11291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (5 · ((2 logb
𝑥)↑4)) ∈
ℝ) |
| 106 | 9, 82 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 · (log‘2)) ∈
ℝ) |
| 107 | 9 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ) |
| 108 | 10, 31 | gtned 11396 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 0) |
| 109 | 107, 88, 108, 97 | mulne0d 11915 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 · (log‘2)) ≠
0) |
| 110 | 32, 106, 109 | redivcld 12095 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / (𝑥 · (log‘2))) ∈
ℝ) |
| 111 | 105, 110 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))) ∈ ℝ) |
| 112 | 111, 10 | readdcld 11290 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))) + 0) ∈ ℝ) |
| 113 | 99, 112 | remulcld 11291 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((1 / ((((2 logb 𝑥)↑5) + 1) ·
(log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈
ℝ) |
| 114 | 5, 113 | remulcld 11291 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) ∈ ℝ) |
| 115 | 41, 75 | elrpd 13074 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ∈
ℝ+) |
| 116 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ∈
ℝ) |
| 117 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 <
2) |
| 118 | | rpre 13043 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
| 119 | 118 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
| 120 | | rpgt0 13047 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 0 < 𝑦) |
| 121 | 120 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 <
𝑦) |
| 122 | | 1red 11262 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 1 ∈
ℝ) |
| 123 | 33 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 1 <
2) |
| 124 | 122, 123 | ltned 11397 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 1 ≠
2) |
| 125 | 124 | necomd 2996 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ≠
1) |
| 126 | 116, 117,
119, 121, 125 | relogbcld 41974 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (2
logb 𝑦) ∈
ℝ) |
| 127 | 126 | recnd 11289 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (2
logb 𝑦) ∈
ℂ) |
| 128 | 80 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ∈
ℝ+) |
| 129 | 128 | relogcld 26665 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(log‘2) ∈ ℝ) |
| 130 | 119, 129 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 · (log‘2)) ∈
ℝ) |
| 131 | 119 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℂ) |
| 132 | | 2cnd 12344 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ∈
ℂ) |
| 133 | 128 | rpne0d 13082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ≠
0) |
| 134 | 132, 133 | logcld 26612 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(log‘2) ∈ ℂ) |
| 135 | | rpne0 13051 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
| 136 | 135 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ≠ 0) |
| 137 | 96 | necomd 2996 |
. . . . . . . 8
⊢ (𝜑 → 0 ≠
(log‘2)) |
| 138 | 137 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 ≠
(log‘2)) |
| 139 | 138 | necomd 2996 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(log‘2) ≠ 0) |
| 140 | 131, 134,
136, 139 | mulne0d 11915 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 · (log‘2)) ≠
0) |
| 141 | 122, 130,
140 | redivcld 12095 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (1 /
(𝑦 · (log‘2)))
∈ ℝ) |
| 142 | | cnelprrecn 11248 |
. . . . . . 7
⊢ ℂ
∈ {ℝ, ℂ} |
| 143 | 142 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
| 144 | 37 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb 𝑥) ∈
ℂ) |
| 145 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
| 146 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 5 ∈
ℕ0) |
| 147 | 145, 146 | expcld 14186 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑5) ∈ ℂ) |
| 148 | | 5cn 12354 |
. . . . . . . 8
⊢ 5 ∈
ℂ |
| 149 | 148 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 5 ∈
ℂ) |
| 150 | 102 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 4 ∈
ℕ0) |
| 151 | 145, 150 | expcld 14186 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑4) ∈ ℂ) |
| 152 | 149, 151 | mulcld 11281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 · (𝑧↑4)) ∈
ℂ) |
| 153 | 13 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 3 ∈
ℝ) |
| 154 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 3) |
| 155 | 90, 153, 11, 154, 17 | ltletrd 11421 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝐴) |
| 156 | 90, 11, 155 | ltled 11409 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐴) |
| 157 | | aks4d1p1p6.4 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 158 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥)) |
| 159 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))) |
| 160 | 21, 24, 156, 157, 158, 159 | dvrelog2b 42067 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2))))) |
| 161 | | 5nn 12352 |
. . . . . . . 8
⊢ 5 ∈
ℕ |
| 162 | | dvexp 25991 |
. . . . . . . 8
⊢ (5 ∈
ℕ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑(5 −
1))))) |
| 163 | 161, 162 | ax-mp 5 |
. . . . . . 7
⊢ (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5
· (𝑧↑(5 −
1)))) |
| 164 | | 5m1e4 12396 |
. . . . . . . . . . 11
⊢ (5
− 1) = 4 |
| 165 | 164 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 − 1) =
4) |
| 166 | 165 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑(5 − 1)) = (𝑧↑4)) |
| 167 | 166 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 · (𝑧↑(5 − 1))) = (5
· (𝑧↑4))) |
| 168 | 167 | mpteq2dva 5242 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (5 · (𝑧↑(5 − 1)))) = (𝑧 ∈ ℂ ↦ (5
· (𝑧↑4)))) |
| 169 | 163, 168 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑4)))) |
| 170 | | oveq1 7438 |
. . . . . 6
⊢ (𝑧 = (2 logb 𝑥) → (𝑧↑5) = ((2 logb 𝑥)↑5)) |
| 171 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑧 = (2 logb 𝑥) → (𝑧↑4) = ((2 logb 𝑥)↑4)) |
| 172 | 171 | oveq2d 7447 |
. . . . . 6
⊢ (𝑧 = (2 logb 𝑥) → (5 · (𝑧↑4)) = (5 · ((2
logb 𝑥)↑4))) |
| 173 | 2, 143, 144, 110, 147, 152, 160, 169, 170, 172 | dvmptco 26010 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑5))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))))) |
| 174 | | 1cnd 11256 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
| 175 | 174 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
| 176 | | 0red 11264 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈
ℝ) |
| 177 | 2, 174 | dvmptc 25996 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ 1)) =
(𝑥 ∈ ℝ ↦
0)) |
| 178 | | ioossre 13448 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 179 | 178 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
| 180 | | tgioo4 24826 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
| 181 | | eqid 2737 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 182 | | iooretop 24786 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
| 183 | 182 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
| 184 | 2, 175, 176, 177, 179, 180, 181, 183 | dvmptres 26001 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 1)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)) |
| 185 | 2, 84, 111, 173, 85, 10, 184 | dvmptadd 25998 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (((2 logb 𝑥)↑5) + 1))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))) + 0))) |
| 186 | | dfrp2 13436 |
. . . . . . . 8
⊢
ℝ+ = (0(,)+∞) |
| 187 | 186 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ+ =
(0(,)+∞)) |
| 188 | 187 | mpteq1d 5237 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦ (2
logb 𝑦)) =
(𝑦 ∈ (0(,)+∞)
↦ (2 logb 𝑦))) |
| 189 | 188 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ+
↦ (2 logb 𝑦))) = (ℝ D (𝑦 ∈ (0(,)+∞) ↦ (2
logb 𝑦)))) |
| 190 | 90 | rexrd 11311 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ*) |
| 191 | | pnfxr 11315 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
| 192 | 191 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 193 | 90 | leidd 11829 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 0) |
| 194 | | 0lepnf 13175 |
. . . . . . . 8
⊢ 0 ≤
+∞ |
| 195 | 194 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ≤
+∞) |
| 196 | | eqid 2737 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)+∞) ↦
(2 logb 𝑦)) =
(𝑦 ∈ (0(,)+∞)
↦ (2 logb 𝑦)) |
| 197 | | eqid 2737 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)+∞) ↦
(1 / (𝑦 ·
(log‘2)))) = (𝑦
∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2)))) |
| 198 | 190, 192,
193, 195, 196, 197 | dvrelog2b 42067 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ (0(,)+∞) ↦
(2 logb 𝑦))) =
(𝑦 ∈ (0(,)+∞)
↦ (1 / (𝑦 ·
(log‘2))))) |
| 199 | 187 | eqcomd 2743 |
. . . . . . 7
⊢ (𝜑 → (0(,)+∞) =
ℝ+) |
| 200 | 199 | mpteq1d 5237 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2)))) =
(𝑦 ∈
ℝ+ ↦ (1 / (𝑦 · (log‘2))))) |
| 201 | 198, 200 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ (0(,)+∞) ↦
(2 logb 𝑦))) =
(𝑦 ∈
ℝ+ ↦ (1 / (𝑦 · (log‘2))))) |
| 202 | 189, 201 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ+
↦ (2 logb 𝑦))) = (𝑦 ∈ ℝ+ ↦ (1 /
(𝑦 ·
(log‘2))))) |
| 203 | | oveq2 7439 |
. . . 4
⊢ (𝑦 = (((2 logb 𝑥)↑5) + 1) → (2
logb 𝑦) = (2
logb (((2 logb 𝑥)↑5) + 1))) |
| 204 | | oveq1 7438 |
. . . . 5
⊢ (𝑦 = (((2 logb 𝑥)↑5) + 1) → (𝑦 · (log‘2)) = ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) |
| 205 | 204 | oveq2d 7447 |
. . . 4
⊢ (𝑦 = (((2 logb 𝑥)↑5) + 1) → (1 /
(𝑦 · (log‘2)))
= (1 / ((((2 logb 𝑥)↑5) + 1) ·
(log‘2)))) |
| 206 | 2, 2, 115, 112, 127, 141, 185, 202, 203, 205 | dvmptco 26010 |
. . 3
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb (((2
logb 𝑥)↑5)
+ 1)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((1 / ((((2 logb 𝑥)↑5) + 1) ·
(log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0)))) |
| 207 | 4 | a1i 11 |
. . . 4
⊢ (𝜑 → 2 ∈
ℝ) |
| 208 | 207 | recnd 11289 |
. . 3
⊢ (𝜑 → 2 ∈
ℂ) |
| 209 | 2, 78, 113, 206, 208 | dvmptcmul 26002 |
. 2
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 · (2 logb
(((2 logb 𝑥)↑5) + 1))))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))))) |
| 210 | 144 | sqcld 14184 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑2) ∈
ℂ) |
| 211 | 82 | resqcld 14165 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘2)↑2) ∈
ℝ) |
| 212 | 81 | rpne0d 13082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) |
| 213 | 3, 212 | logcld 26612 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈
ℂ) |
| 214 | 213, 97, 63 | expne0d 14192 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘2)↑2) ≠
0) |
| 215 | 5, 211, 214 | redivcld 12095 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 / ((log‘2)↑2))
∈ ℝ) |
| 216 | 67 | relogcld 26665 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘𝑥) ∈ ℝ) |
| 217 | | 2m1e1 12392 |
. . . . . . 7
⊢ (2
− 1) = 1 |
| 218 | | 1nn0 12542 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
| 219 | 217, 218 | eqeltri 2837 |
. . . . . 6
⊢ (2
− 1) ∈ ℕ0 |
| 220 | 219 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 − 1) ∈
ℕ0) |
| 221 | 216, 220 | reexpcld 14203 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘𝑥)↑(2 − 1)) ∈
ℝ) |
| 222 | 67 | rpne0d 13082 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 0) |
| 223 | 221, 9, 222 | redivcld 12095 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈ ℝ) |
| 224 | 215, 223 | remulcld 11291 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ) |
| 225 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑2)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑2)) |
| 226 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥))) |
| 227 | | eqid 2737 |
. . 3
⊢ (2 /
((log‘2)↑2)) = (2 / ((log‘2)↑2)) |
| 228 | | 2nn 12339 |
. . . 4
⊢ 2 ∈
ℕ |
| 229 | 228 | a1i 11 |
. . 3
⊢ (𝜑 → 2 ∈
ℕ) |
| 230 | 11, 23, 155, 157, 225, 226, 227, 229 | dvrelogpow2b 42069 |
. 2
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑2))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥)))) |
| 231 | 2, 79, 114, 209, 210, 224, 230 | dvmptadd 25998 |
1
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) + ((2 logb 𝑥)↑2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝑥)↑(2 − 1)) / 𝑥))))) |