Step | Hyp | Ref
| Expression |
1 | | reelprrecn 10710 |
. . 3
⊢ ℝ
∈ {ℝ, ℂ} |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → ℝ ∈ {ℝ,
ℂ}) |
3 | | 2cnd 11797 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℂ) |
4 | | 2re 11793 |
. . . . . 6
⊢ 2 ∈
ℝ |
5 | 4 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℝ) |
6 | | 2pos 11822 |
. . . . . 6
⊢ 0 <
2 |
7 | 6 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 2) |
8 | | elioore 12854 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴(,)𝐵) → 𝑥 ∈ ℝ) |
9 | 8 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ) |
10 | | 0red 10725 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 ∈ ℝ) |
11 | | aks4d1p1p6.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
12 | 11 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈ ℝ) |
13 | | 3re 11799 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 3 ∈ ℝ) |
15 | | 3pos 11824 |
. . . . . . . . . . 11
⊢ 0 <
3 |
16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 3) |
17 | | aks4d1p1p6.3 |
. . . . . . . . . . 11
⊢ (𝜑 → 3 ≤ 𝐴) |
18 | 17 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 3 ≤ 𝐴) |
19 | 10, 14, 12, 16, 18 | ltletrd 10881 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 𝐴) |
20 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ (𝐴(,)𝐵)) |
21 | 11 | rexrd 10772 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
22 | 21 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 ∈
ℝ*) |
23 | | aks4d1p1p6.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ ℝ) |
24 | 23 | rexrd 10772 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
25 | 24 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐵 ∈
ℝ*) |
26 | 9 | rexrd 10772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ*) |
27 | | elioo5 12881 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ ℝ*) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
28 | 22, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 ∈ (𝐴(,)𝐵) ↔ (𝐴 < 𝑥 ∧ 𝑥 < 𝐵))) |
29 | 20, 28 | mpbid 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝐴 < 𝑥 ∧ 𝑥 < 𝐵)) |
30 | 29 | simpld 498 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝐴 < 𝑥) |
31 | 10, 12, 9, 19, 30 | lttrd 10882 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < 𝑥) |
32 | | 1red 10723 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈ ℝ) |
33 | | 1lt2 11890 |
. . . . . . . . . . 11
⊢ 1 <
2 |
34 | 33 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 2) |
35 | 32, 34 | ltned 10857 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ≠ 2) |
36 | 35 | necomd 2990 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 1) |
37 | 5, 7, 9, 31, 36 | relogbcld 39623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb 𝑥) ∈
ℝ) |
38 | | 5nn0 11999 |
. . . . . . . 8
⊢ 5 ∈
ℕ0 |
39 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈
ℕ0) |
40 | 37, 39 | reexpcld 13622 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑5) ∈
ℝ) |
41 | 40, 32 | readdcld 10751 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ∈
ℝ) |
42 | 10, 32 | readdcld 10751 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (0 + 1) ∈
ℝ) |
43 | 10 | ltp1d 11651 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (0 + 1)) |
44 | 39 | nn0zd 12169 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈ ℤ) |
45 | | 2cnd 11797 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ∈ ℂ) |
46 | | 0red 10725 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 0 ∈ ℝ) |
47 | 6 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 0 < 2) |
48 | 46, 47 | ltned 10857 |
. . . . . . . . . . . 12
⊢ (⊤
→ 0 ≠ 2) |
49 | 48 | necomd 2990 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ≠ 0) |
50 | | 1red 10723 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1 ∈ ℝ) |
51 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1 < 2) |
52 | 50, 51 | ltned 10857 |
. . . . . . . . . . . 12
⊢ (⊤
→ 1 ≠ 2) |
53 | 52 | necomd 2990 |
. . . . . . . . . . 11
⊢ (⊤
→ 2 ≠ 1) |
54 | | logb1 25510 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 2 ≠ 1) → (2 logb 1) =
0) |
55 | 45, 49, 53, 54 | syl3anc 1372 |
. . . . . . . . . 10
⊢ (⊤
→ (2 logb 1) = 0) |
56 | 55 | mptru 1549 |
. . . . . . . . 9
⊢ (2
logb 1) = 0 |
57 | | 2lt3 11891 |
. . . . . . . . . . . . . 14
⊢ 2 <
3 |
58 | 57 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 < 3) |
59 | 32, 5, 14, 34, 58 | lttrd 10882 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 3) |
60 | 32, 14, 12, 59, 18 | ltletrd 10881 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 𝐴) |
61 | 32, 12, 9, 60, 30 | lttrd 10882 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 < 𝑥) |
62 | | 2z 12098 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℤ |
63 | 62 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈ ℤ) |
64 | 63 | uzidd 12343 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈
(ℤ≥‘2)) |
65 | | 1rp 12479 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
66 | 65 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈
ℝ+) |
67 | 9, 31 | elrpd 12514 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℝ+) |
68 | | logblt 25525 |
. . . . . . . . . . 11
⊢ ((2
∈ (ℤ≥‘2) ∧ 1 ∈ ℝ+
∧ 𝑥 ∈
ℝ+) → (1 < 𝑥 ↔ (2 logb 1) < (2
logb 𝑥))) |
69 | 64, 66, 67, 68 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 < 𝑥 ↔ (2 logb 1) < (2
logb 𝑥))) |
70 | 61, 69 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb 1) < (2
logb 𝑥)) |
71 | 56, 70 | eqbrtrrid 5067 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (2 logb 𝑥)) |
72 | | expgt0 13557 |
. . . . . . . 8
⊢ (((2
logb 𝑥) ∈
ℝ ∧ 5 ∈ ℤ ∧ 0 < (2 logb 𝑥)) → 0 < ((2
logb 𝑥)↑5)) |
73 | 37, 44, 71, 72 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < ((2 logb 𝑥)↑5)) |
74 | 10, 40, 32, 73 | ltadd1dd 11332 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (0 + 1) < (((2 logb
𝑥)↑5) +
1)) |
75 | 10, 42, 41, 43, 74 | lttrd 10882 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 0 < (((2 logb 𝑥)↑5) + 1)) |
76 | 5, 7, 41, 75, 36 | relogbcld 39623 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb (((2
logb 𝑥)↑5)
+ 1)) ∈ ℝ) |
77 | | recn 10708 |
. . . 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 10742 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 · (2 logb
(((2 logb 𝑥)↑5) + 1))) ∈
ℂ) |
80 | | 2rp 12480 |
. . . . . . . 8
⊢ 2 ∈
ℝ+ |
81 | 80 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ∈
ℝ+) |
82 | 81 | relogcld 25369 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈
ℝ) |
83 | 41, 82 | remulcld 10752 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((2 logb 𝑥)↑5) + 1) ·
(log‘2)) ∈ ℝ) |
84 | 40 | recnd 10750 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑5) ∈
ℂ) |
85 | | 1cnd 10717 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 1 ∈ ℂ) |
86 | 84, 85 | addcld 10741 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ∈
ℂ) |
87 | 7 | gt0ne0d 11285 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) |
88 | 3, 87 | logcld 25317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈
ℂ) |
89 | 75 | gt0ne0d 11285 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ≠
0) |
90 | | 0red 10725 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) |
91 | | loggt0b 25378 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ+ → (0 < (log‘2) ↔ 1 <
2)) |
92 | 80, 91 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (0 <
(log‘2) ↔ 1 < 2) |
93 | 33, 92 | mpbir 234 |
. . . . . . . . . 10
⊢ 0 <
(log‘2) |
94 | 93 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 <
(log‘2)) |
95 | 90, 94 | ltned 10857 |
. . . . . . . 8
⊢ (𝜑 → 0 ≠
(log‘2)) |
96 | 95 | necomd 2990 |
. . . . . . 7
⊢ (𝜑 → (log‘2) ≠
0) |
97 | 96 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ≠
0) |
98 | 86, 88, 89, 97 | mulne0d 11373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((((2 logb 𝑥)↑5) + 1) ·
(log‘2)) ≠ 0) |
99 | 32, 83, 98 | redivcld 11549 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / ((((2 logb 𝑥)↑5) + 1) ·
(log‘2))) ∈ ℝ) |
100 | | 5re 11806 |
. . . . . . . 8
⊢ 5 ∈
ℝ |
101 | 100 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 5 ∈ ℝ) |
102 | | 4nn0 11998 |
. . . . . . . . 9
⊢ 4 ∈
ℕ0 |
103 | 102 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 4 ∈
ℕ0) |
104 | 37, 103 | reexpcld 13622 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑4) ∈
ℝ) |
105 | 101, 104 | remulcld 10752 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (5 · ((2 logb
𝑥)↑4)) ∈
ℝ) |
106 | 9, 82 | remulcld 10752 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 · (log‘2)) ∈
ℝ) |
107 | 9 | recnd 10750 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ∈ ℂ) |
108 | 10, 31 | gtned 10856 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 0) |
109 | 107, 88, 108, 97 | mulne0d 11373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (𝑥 · (log‘2)) ≠
0) |
110 | 32, 106, 109 | redivcld 11549 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (1 / (𝑥 · (log‘2))) ∈
ℝ) |
111 | 105, 110 | remulcld 10752 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))) ∈ ℝ) |
112 | 111, 10 | readdcld 10751 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))) + 0) ∈ ℝ) |
113 | 99, 112 | remulcld 10752 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((1 / ((((2 logb 𝑥)↑5) + 1) ·
(log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) + 0)) ∈
ℝ) |
114 | 5, 113 | remulcld 10752 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 · ((1 / ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝑥)↑4)) · (1 / (𝑥 · (log‘2)))) +
0))) ∈ ℝ) |
115 | 41, 75 | elrpd 12514 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((2 logb 𝑥)↑5) + 1) ∈
ℝ+) |
116 | 4 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ∈
ℝ) |
117 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 <
2) |
118 | | rpre 12483 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℝ) |
119 | 118 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℝ) |
120 | | rpgt0 12487 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 0 < 𝑦) |
121 | 120 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 <
𝑦) |
122 | | 1red 10723 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 1 ∈
ℝ) |
123 | 33 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 1 <
2) |
124 | 122, 123 | ltned 10857 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 1 ≠
2) |
125 | 124 | necomd 2990 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ≠
1) |
126 | 116, 117,
119, 121, 125 | relogbcld 39623 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (2
logb 𝑦) ∈
ℝ) |
127 | 126 | recnd 10750 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (2
logb 𝑦) ∈
ℂ) |
128 | 80 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ∈
ℝ+) |
129 | 128 | relogcld 25369 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(log‘2) ∈ ℝ) |
130 | 119, 129 | remulcld 10752 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 · (log‘2)) ∈
ℝ) |
131 | 119 | recnd 10750 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ∈
ℂ) |
132 | | 2cnd 11797 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ∈
ℂ) |
133 | 128 | rpne0d 12522 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 2 ≠
0) |
134 | 132, 133 | logcld 25317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(log‘2) ∈ ℂ) |
135 | | rpne0 12491 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
136 | 135 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 𝑦 ≠ 0) |
137 | 96 | necomd 2990 |
. . . . . . . 8
⊢ (𝜑 → 0 ≠
(log‘2)) |
138 | 137 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → 0 ≠
(log‘2)) |
139 | 138 | necomd 2990 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) →
(log‘2) ≠ 0) |
140 | 131, 134,
136, 139 | mulne0d 11373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (𝑦 · (log‘2)) ≠
0) |
141 | 122, 130,
140 | redivcld 11549 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ+) → (1 /
(𝑦 · (log‘2)))
∈ ℝ) |
142 | | cnelprrecn 10711 |
. . . . . . 7
⊢ ℂ
∈ {ℝ, ℂ} |
143 | 142 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂ ∈ {ℝ,
ℂ}) |
144 | 37 | recnd 10750 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 logb 𝑥) ∈
ℂ) |
145 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑧 ∈ ℂ) |
146 | 38 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 5 ∈
ℕ0) |
147 | 145, 146 | expcld 13605 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑5) ∈ ℂ) |
148 | | 5cn 11807 |
. . . . . . . 8
⊢ 5 ∈
ℂ |
149 | 148 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 5 ∈
ℂ) |
150 | 102 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 4 ∈
ℕ0) |
151 | 145, 150 | expcld 13605 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑4) ∈ ℂ) |
152 | 149, 151 | mulcld 10742 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 · (𝑧↑4)) ∈
ℂ) |
153 | 13 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 3 ∈
ℝ) |
154 | 15 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 3) |
155 | 90, 153, 11, 154, 17 | ltletrd 10881 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝐴) |
156 | 90, 11, 155 | ltled 10869 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐴) |
157 | | aks4d1p1p6.4 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
158 | | eqid 2739 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥)) |
159 | | eqid 2739 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2)))) |
160 | 21, 24, 156, 157, 158, 159 | dvrelog2b 39716 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (2 logb 𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (1 / (𝑥 · (log‘2))))) |
161 | | 5nn 11805 |
. . . . . . . 8
⊢ 5 ∈
ℕ |
162 | | dvexp 24708 |
. . . . . . . 8
⊢ (5 ∈
ℕ → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑(5 −
1))))) |
163 | 161, 162 | ax-mp 5 |
. . . . . . 7
⊢ (ℂ
D (𝑧 ∈ ℂ ↦
(𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5
· (𝑧↑(5 −
1)))) |
164 | | 5m1e4 11849 |
. . . . . . . . . . 11
⊢ (5
− 1) = 4 |
165 | 164 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 − 1) =
4) |
166 | 165 | oveq2d 7189 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑧↑(5 − 1)) = (𝑧↑4)) |
167 | 166 | oveq2d 7189 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (5 · (𝑧↑(5 − 1))) = (5
· (𝑧↑4))) |
168 | 167 | mpteq2dva 5126 |
. . . . . . 7
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ (5 · (𝑧↑(5 − 1)))) = (𝑧 ∈ ℂ ↦ (5
· (𝑧↑4)))) |
169 | 163, 168 | syl5eq 2786 |
. . . . . 6
⊢ (𝜑 → (ℂ D (𝑧 ∈ ℂ ↦ (𝑧↑5))) = (𝑧 ∈ ℂ ↦ (5 · (𝑧↑4)))) |
170 | | oveq1 7180 |
. . . . . 6
⊢ (𝑧 = (2 logb 𝑥) → (𝑧↑5) = ((2 logb 𝑥)↑5)) |
171 | | oveq1 7180 |
. . . . . . 7
⊢ (𝑧 = (2 logb 𝑥) → (𝑧↑4) = ((2 logb 𝑥)↑4)) |
172 | 171 | oveq2d 7189 |
. . . . . 6
⊢ (𝑧 = (2 logb 𝑥) → (5 · (𝑧↑4)) = (5 · ((2
logb 𝑥)↑4))) |
173 | 2, 143, 144, 110, 147, 152, 160, 169, 170, 172 | dvmptco 24727 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑5))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))))) |
174 | | 1cnd 10717 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
175 | 174 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 1 ∈
ℂ) |
176 | | 0red 10725 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → 0 ∈
ℝ) |
177 | 2, 174 | dvmptc 24713 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑥 ∈ ℝ ↦ 1)) =
(𝑥 ∈ ℝ ↦
0)) |
178 | | ioossre 12885 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ⊆ ℝ |
179 | 178 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ ℝ) |
180 | | eqid 2739 |
. . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
181 | 180 | tgioo2 23558 |
. . . . . 6
⊢
(topGen‘ran (,)) = ((TopOpen‘ℂfld)
↾t ℝ) |
182 | | iooretop 23521 |
. . . . . . 7
⊢ (𝐴(,)𝐵) ∈ (topGen‘ran
(,)) |
183 | 182 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴(,)𝐵) ∈ (topGen‘ran
(,))) |
184 | 2, 175, 176, 177, 179, 181, 180, 183 | dvmptres 24718 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ 1)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ 0)) |
185 | 2, 84, 111, 173, 85, 10, 184 | dvmptadd 24715 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ (((2 logb 𝑥)↑5) + 1))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ (((5 · ((2 logb
𝑥)↑4)) · (1 /
(𝑥 ·
(log‘2)))) + 0))) |
186 | | dfrp2 12873 |
. . . . . . . 8
⊢
ℝ+ = (0(,)+∞) |
187 | 186 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℝ+ =
(0(,)+∞)) |
188 | 187 | mpteq1d 5120 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ+ ↦ (2
logb 𝑦)) =
(𝑦 ∈ (0(,)+∞)
↦ (2 logb 𝑦))) |
189 | 188 | oveq2d 7189 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ+
↦ (2 logb 𝑦))) = (ℝ D (𝑦 ∈ (0(,)+∞) ↦ (2
logb 𝑦)))) |
190 | 90 | rexrd 10772 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℝ*) |
191 | | pnfxr 10776 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
192 | 191 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → +∞ ∈
ℝ*) |
193 | 90 | leidd 11287 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 0) |
194 | | 0lepnf 12613 |
. . . . . . . 8
⊢ 0 ≤
+∞ |
195 | 194 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ≤
+∞) |
196 | | eqid 2739 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)+∞) ↦
(2 logb 𝑦)) =
(𝑦 ∈ (0(,)+∞)
↦ (2 logb 𝑦)) |
197 | | eqid 2739 |
. . . . . . 7
⊢ (𝑦 ∈ (0(,)+∞) ↦
(1 / (𝑦 ·
(log‘2)))) = (𝑦
∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2)))) |
198 | 190, 192,
193, 195, 196, 197 | dvrelog2b 39716 |
. . . . . 6
⊢ (𝜑 → (ℝ D (𝑦 ∈ (0(,)+∞) ↦
(2 logb 𝑦))) =
(𝑦 ∈ (0(,)+∞)
↦ (1 / (𝑦 ·
(log‘2))))) |
199 | 187 | eqcomd 2745 |
. . . . . . 7
⊢ (𝜑 → (0(,)+∞) =
ℝ+) |
200 | 199 | mpteq1d 5120 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ (0(,)+∞) ↦ (1 / (𝑦 · (log‘2)))) =
(𝑦 ∈
ℝ+ ↦ (1 / (𝑦 · (log‘2))))) |
201 | 198, 200 | eqtrd 2774 |
. . . . 5
⊢ (𝜑 → (ℝ D (𝑦 ∈ (0(,)+∞) ↦
(2 logb 𝑦))) =
(𝑦 ∈
ℝ+ ↦ (1 / (𝑦 · (log‘2))))) |
202 | 189, 201 | eqtrd 2774 |
. . . 4
⊢ (𝜑 → (ℝ D (𝑦 ∈ ℝ+
↦ (2 logb 𝑦))) = (𝑦 ∈ ℝ+ ↦ (1 /
(𝑦 ·
(log‘2))))) |
203 | | oveq2 7181 |
. . . 4
⊢ (𝑦 = (((2 logb 𝑥)↑5) + 1) → (2
logb 𝑦) = (2
logb (((2 logb 𝑥)↑5) + 1))) |
204 | | oveq1 7180 |
. . . . 5
⊢ (𝑦 = (((2 logb 𝑥)↑5) + 1) → (𝑦 · (log‘2)) = ((((2
logb 𝑥)↑5)
+ 1) · (log‘2))) |
205 | 204 | oveq2d 7189 |
. . . 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 24727 |
. . 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 10750 |
. . 3
⊢ (𝜑 → 2 ∈
ℂ) |
209 | 2, 78, 113, 206, 208 | dvmptcmul 24719 |
. 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 13603 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 logb 𝑥)↑2) ∈
ℂ) |
211 | 82 | resqcld 13706 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘2)↑2) ∈
ℝ) |
212 | 81 | rpne0d 12522 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 2 ≠ 0) |
213 | 3, 212 | logcld 25317 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘2) ∈
ℂ) |
214 | 213, 97, 63 | expne0d 13611 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘2)↑2) ≠
0) |
215 | 5, 211, 214 | redivcld 11549 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 / ((log‘2)↑2))
∈ ℝ) |
216 | 67 | relogcld 25369 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (log‘𝑥) ∈ ℝ) |
217 | | 2m1e1 11845 |
. . . . . . 7
⊢ (2
− 1) = 1 |
218 | | 1nn0 11995 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
219 | 217, 218 | eqeltri 2830 |
. . . . . 6
⊢ (2
− 1) ∈ ℕ0 |
220 | 219 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (2 − 1) ∈
ℕ0) |
221 | 216, 220 | reexpcld 13622 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((log‘𝑥)↑(2 − 1)) ∈
ℝ) |
222 | 67 | rpne0d 12522 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → 𝑥 ≠ 0) |
223 | 221, 9, 222 | redivcld 11549 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → (((log‘𝑥)↑(2 − 1)) / 𝑥) ∈ ℝ) |
224 | 215, 223 | remulcld 10752 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴(,)𝐵)) → ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥)) ∈ ℝ) |
225 | | eqid 2739 |
. . 3
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑2)) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑2)) |
226 | | eqid 2739 |
. . 3
⊢ (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥))) |
227 | | eqid 2739 |
. . 3
⊢ (2 /
((log‘2)↑2)) = (2 / ((log‘2)↑2)) |
228 | | 2nn 11792 |
. . . 4
⊢ 2 ∈
ℕ |
229 | 228 | a1i 11 |
. . 3
⊢ (𝜑 → 2 ∈
ℕ) |
230 | 11, 23, 155, 157, 225, 226, 227, 229 | dvrelogpow2b 39718 |
. 2
⊢ (𝜑 → (ℝ D (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 logb 𝑥)↑2))) = (𝑥 ∈ (𝐴(,)𝐵) ↦ ((2 / ((log‘2)↑2))
· (((log‘𝑥)↑(2 − 1)) / 𝑥)))) |
231 | 2, 79, 114, 209, 210, 224, 230 | dvmptadd 24715 |
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)) / 𝑥))))) |