Proof of Theorem aks4d1p1p7
Step | Hyp | Ref
| Expression |
1 | | aks4d1p1p7.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | recnd 10747 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | 0red 10722 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
4 | | 4re 11800 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℝ |
5 | 4 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 4 ∈
ℝ) |
6 | | 4pos 11823 |
. . . . . . . . . . . . . . 15
⊢ 0 <
4 |
7 | 6 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 < 4) |
8 | | aks4d1p1p7.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 4 ≤ 𝐴) |
9 | 3, 5, 1, 7, 8 | ltletrd 10878 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝐴) |
10 | 3, 9 | ltned 10854 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≠ 𝐴) |
11 | 10 | necomd 2989 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≠ 0) |
12 | 2, 11 | logcld 25314 |
. . . . . . . . . 10
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) |
13 | | 2cnd 11794 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
14 | | 2pos 11819 |
. . . . . . . . . . . . . 14
⊢ 0 <
2 |
15 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 2) |
16 | 3, 15 | ltned 10854 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≠ 2) |
17 | 16 | necomd 2989 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ≠ 0) |
18 | 13, 17 | logcld 25314 |
. . . . . . . . . 10
⊢ (𝜑 → (log‘2) ∈
ℂ) |
19 | | 1lt2 11887 |
. . . . . . . . . . . . . 14
⊢ 1 <
2 |
20 | | 2rp 12477 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ+ |
21 | | loggt0b 25375 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℝ+ → (0 < (log‘2) ↔ 1 <
2)) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (0 <
(log‘2) ↔ 1 < 2) |
23 | 19, 22 | mpbir 234 |
. . . . . . . . . . . . 13
⊢ 0 <
(log‘2) |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 <
(log‘2)) |
25 | 3, 24 | ltned 10854 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≠
(log‘2)) |
26 | 25 | necomd 2989 |
. . . . . . . . . 10
⊢ (𝜑 → (log‘2) ≠
0) |
27 | | 5nn0 11996 |
. . . . . . . . . . 11
⊢ 5 ∈
ℕ0 |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 5 ∈
ℕ0) |
29 | 12, 18, 26, 28 | expdivd 13616 |
. . . . . . . . 9
⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) =
(((log‘𝐴)↑5) /
((log‘2)↑5))) |
30 | 29 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1)
= ((((log‘𝐴)↑5)
/ ((log‘2)↑5)) + 1)) |
31 | 30 | oveq1d 7185 |
. . . . . . 7
⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1)
· (log‘2)) = (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1)
· (log‘2))) |
32 | 31 | oveq2d 7186 |
. . . . . 6
⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1)
· (log‘2))) = (1 / (((((log‘𝐴)↑5) / ((log‘2)↑5)) + 1)
· (log‘2)))) |
33 | 32 | oveq1d 7185 |
. . . . 5
⊢ (𝜑 → ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1)
· (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) = ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) |
34 | 33 | oveq2d 7186 |
. . . 4
⊢ (𝜑 → (2 · ((1 /
(((((log‘𝐴) /
(log‘2))↑5) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) = (2 · ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))))) |
35 | 34 | oveq1d 7185 |
. . 3
⊢ (𝜑 → ((2 · ((1 /
(((((log‘𝐴) /
(log‘2))↑5) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) = ((2 · ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴)))) |
36 | | 2re 11790 |
. . . . . . 7
⊢ 2 ∈
ℝ |
37 | 36 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℝ) |
38 | | 1red 10720 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
39 | 1, 9 | elrpd 12511 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
40 | 39 | relogcld 25366 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘𝐴) ∈
ℝ) |
41 | 40, 28 | reexpcld 13619 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝐴)↑5) ∈
ℝ) |
42 | 20 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 2 ∈
ℝ+) |
43 | 42 | relogcld 25366 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘2) ∈
ℝ) |
44 | 43, 28 | reexpcld 13619 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘2)↑5)
∈ ℝ) |
45 | 28 | nn0zd 12166 |
. . . . . . . . . . . 12
⊢ (𝜑 → 5 ∈
ℤ) |
46 | 18, 26, 45 | expne0d 13608 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘2)↑5)
≠ 0) |
47 | 41, 44, 46 | redivcld 11546 |
. . . . . . . . . 10
⊢ (𝜑 → (((log‘𝐴)↑5) /
((log‘2)↑5)) ∈ ℝ) |
48 | 47, 38 | readdcld 10748 |
. . . . . . . . 9
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) ∈ ℝ) |
49 | 48, 43 | remulcld 10749 |
. . . . . . . 8
⊢ (𝜑 → (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2)) ∈
ℝ) |
50 | 12, 28 | expcld 13602 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝐴)↑5) ∈
ℂ) |
51 | 18, 28 | expcld 13602 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘2)↑5)
∈ ℂ) |
52 | 50, 51, 46 | divcld 11494 |
. . . . . . . . . 10
⊢ (𝜑 → (((log‘𝐴)↑5) /
((log‘2)↑5)) ∈ ℂ) |
53 | | 1cnd 10714 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) |
54 | 52, 53 | addcld 10738 |
. . . . . . . . 9
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) ∈ ℂ) |
55 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < 2) |
56 | 37, 55 | rplogcld 25372 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (log‘2) ∈
ℝ+) |
57 | 56, 45 | rpexpcld 13700 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((log‘2)↑5)
∈ ℝ+) |
58 | | 1re 10719 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
59 | | 3nn0 11994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 ∈
ℕ0 |
60 | 58, 59 | nn0addge2i 12025 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ≤ (3
+ 1) |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ≤ (3 +
1)) |
62 | | df-4 11781 |
. . . . . . . . . . . . . . . . 17
⊢ 4 = (3 +
1) |
63 | 61, 62 | breqtrrdi 5072 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ≤ 4) |
64 | 38, 5, 1, 63, 8 | letrd 10875 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ≤ 𝐴) |
65 | 1, 64 | logge0d 25373 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ≤ (log‘𝐴)) |
66 | 40, 28, 65 | expge0d 13620 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑5)) |
67 | 41, 57, 66 | divge0d 12554 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) /
((log‘2)↑5))) |
68 | 47 | ltp1d 11648 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((log‘𝐴)↑5) /
((log‘2)↑5)) < ((((log‘𝐴)↑5) / ((log‘2)↑5)) +
1)) |
69 | 3, 47, 48, 67, 68 | lelttrd 10876 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < ((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1)) |
70 | 3, 69 | ltned 10854 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≠ ((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1)) |
71 | 70 | necomd 2989 |
. . . . . . . . 9
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) ≠ 0) |
72 | 54, 18, 71, 26 | mulne0d 11370 |
. . . . . . . 8
⊢ (𝜑 → (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2)) ≠ 0) |
73 | 38, 49, 72 | redivcld 11546 |
. . . . . . 7
⊢ (𝜑 → (1 / (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) ∈
ℝ) |
74 | | 5re 11803 |
. . . . . . . . . 10
⊢ 5 ∈
ℝ |
75 | 74 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 5 ∈
ℝ) |
76 | | 4nn0 11995 |
. . . . . . . . . . 11
⊢ 4 ∈
ℕ0 |
77 | 76 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 4 ∈
ℕ0) |
78 | 40, 77 | reexpcld 13619 |
. . . . . . . . 9
⊢ (𝜑 → ((log‘𝐴)↑4) ∈
ℝ) |
79 | 75, 78 | remulcld 10749 |
. . . . . . . 8
⊢ (𝜑 → (5 ·
((log‘𝐴)↑4))
∈ ℝ) |
80 | 44, 1 | remulcld 10749 |
. . . . . . . 8
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) ∈
ℝ) |
81 | 51, 2, 46, 11 | mulne0d 11370 |
. . . . . . . 8
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) ≠
0) |
82 | 79, 80, 81 | redivcld 11546 |
. . . . . . 7
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) ∈ ℝ) |
83 | 73, 82 | remulcld 10749 |
. . . . . 6
⊢ (𝜑 → ((1 / (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))) ∈ ℝ) |
84 | 37, 83 | remulcld 10749 |
. . . . 5
⊢ (𝜑 → (2 · ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) ∈ ℝ) |
85 | 43 | resqcld 13703 |
. . . . . . 7
⊢ (𝜑 → ((log‘2)↑2)
∈ ℝ) |
86 | | 2z 12095 |
. . . . . . . . 9
⊢ 2 ∈
ℤ |
87 | 86 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℤ) |
88 | 18, 26, 87 | expne0d 13608 |
. . . . . . 7
⊢ (𝜑 → ((log‘2)↑2)
≠ 0) |
89 | 37, 85, 88 | redivcld 11546 |
. . . . . 6
⊢ (𝜑 → (2 /
((log‘2)↑2)) ∈ ℝ) |
90 | | 1nn0 11992 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
91 | 90 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℕ0) |
92 | 40, 91 | reexpcld 13619 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝐴)↑1) ∈
ℝ) |
93 | 92, 1, 11 | redivcld 11546 |
. . . . . 6
⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) ∈ ℝ) |
94 | 89, 93 | remulcld 10749 |
. . . . 5
⊢ (𝜑 → ((2 /
((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) ∈ ℝ) |
95 | 84, 94 | readdcld 10748 |
. . . 4
⊢ (𝜑 → ((2 · ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) ∈ ℝ) |
96 | 47, 43 | remulcld 10749 |
. . . . . . . 8
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2)) ∈
ℝ) |
97 | | 1lt4 11892 |
. . . . . . . . . . . . . . . 16
⊢ 1 <
4 |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 < 4) |
99 | 38, 5, 1, 98, 8 | ltletrd 10878 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 < 𝐴) |
100 | | loggt0b 25375 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ+
→ (0 < (log‘𝐴) ↔ 1 < 𝐴)) |
101 | 39, 100 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 < (log‘𝐴) ↔ 1 < 𝐴)) |
102 | 99, 101 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < (log‘𝐴)) |
103 | 3, 102 | ltned 10854 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≠ (log‘𝐴)) |
104 | 103 | necomd 2989 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝐴) ≠ 0) |
105 | 12, 104, 45 | expne0d 13608 |
. . . . . . . . . 10
⊢ (𝜑 → ((log‘𝐴)↑5) ≠
0) |
106 | 50, 51, 105, 46 | divne0d 11510 |
. . . . . . . . 9
⊢ (𝜑 → (((log‘𝐴)↑5) /
((log‘2)↑5)) ≠ 0) |
107 | 52, 18, 106, 26 | mulne0d 11370 |
. . . . . . . 8
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2)) ≠ 0) |
108 | 38, 96, 107 | redivcld 11546 |
. . . . . . 7
⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) ∈
ℝ) |
109 | 108, 82 | remulcld 10749 |
. . . . . 6
⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))) ∈ ℝ) |
110 | 37, 109 | remulcld 10749 |
. . . . 5
⊢ (𝜑 → (2 · ((1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) ∈ ℝ) |
111 | 110, 94 | readdcld 10748 |
. . . 4
⊢ (𝜑 → ((2 · ((1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) ∈ ℝ) |
112 | 59 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 3 ∈
ℕ0) |
113 | 40, 112 | reexpcld 13619 |
. . . . . 6
⊢ (𝜑 → ((log‘𝐴)↑3) ∈
ℝ) |
114 | 5, 113 | remulcld 10749 |
. . . . 5
⊢ (𝜑 → (4 ·
((log‘𝐴)↑3))
∈ ℝ) |
115 | 43, 77 | reexpcld 13619 |
. . . . . 6
⊢ (𝜑 → ((log‘2)↑4)
∈ ℝ) |
116 | 115, 1 | remulcld 10749 |
. . . . 5
⊢ (𝜑 → (((log‘2)↑4)
· 𝐴) ∈
ℝ) |
117 | 18, 77 | expcld 13602 |
. . . . . 6
⊢ (𝜑 → ((log‘2)↑4)
∈ ℂ) |
118 | | 4z 12097 |
. . . . . . . 8
⊢ 4 ∈
ℤ |
119 | 118 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 4 ∈
ℤ) |
120 | 18, 26, 119 | expne0d 13608 |
. . . . . 6
⊢ (𝜑 → ((log‘2)↑4)
≠ 0) |
121 | 117, 2, 120, 11 | mulne0d 11370 |
. . . . 5
⊢ (𝜑 → (((log‘2)↑4)
· 𝐴) ≠
0) |
122 | 114, 116,
121 | redivcld 11546 |
. . . 4
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴)) ∈ ℝ) |
123 | | 0le2 11818 |
. . . . . . 7
⊢ 0 ≤
2 |
124 | 123 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 0 ≤ 2) |
125 | 57, 39 | rpmulcld 12530 |
. . . . . . . 8
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) ∈
ℝ+) |
126 | 28 | nn0ge0d 12039 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 5) |
127 | 40, 77, 65 | expge0d 13620 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ ((log‘𝐴)↑4)) |
128 | 75, 78, 126, 127 | mulge0d 11295 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (5 ·
((log‘𝐴)↑4))) |
129 | 79, 125, 128 | divge0d 12554 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))) |
130 | 1, 99 | rplogcld 25372 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘𝐴) ∈
ℝ+) |
131 | 130, 45 | rpexpcld 13700 |
. . . . . . . . . 10
⊢ (𝜑 → ((log‘𝐴)↑5) ∈
ℝ+) |
132 | 131, 57 | rpdivcld 12531 |
. . . . . . . . 9
⊢ (𝜑 → (((log‘𝐴)↑5) /
((log‘2)↑5)) ∈ ℝ+) |
133 | 132, 56 | rpmulcld 12530 |
. . . . . . . 8
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2)) ∈
ℝ+) |
134 | 24, 22 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 < 2) |
135 | 37, 134 | rplogcld 25372 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘2) ∈
ℝ+) |
136 | 135, 45 | rpexpcld 13700 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘2)↑5)
∈ ℝ+) |
137 | 41, 136, 66 | divge0d 12554 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (((log‘𝐴)↑5) /
((log‘2)↑5))) |
138 | 47, 137 | ge0p1rpd 12544 |
. . . . . . . . 9
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) ∈ ℝ+) |
139 | 138, 135 | rpmulcld 12530 |
. . . . . . . 8
⊢ (𝜑 → (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2)) ∈
ℝ+) |
140 | | 0le1 11241 |
. . . . . . . . 9
⊢ 0 ≤
1 |
141 | 140 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ 1) |
142 | 135 | rpred 12514 |
. . . . . . . . 9
⊢ (𝜑 → (log‘2) ∈
ℝ) |
143 | 135 | rpge0d 12518 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤
(log‘2)) |
144 | 47 | lep1d 11649 |
. . . . . . . . 9
⊢ (𝜑 → (((log‘𝐴)↑5) /
((log‘2)↑5)) ≤ ((((log‘𝐴)↑5) / ((log‘2)↑5)) +
1)) |
145 | 47, 48, 142, 143, 144 | lemul1ad 11657 |
. . . . . . . 8
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2)) ≤ (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) |
146 | 133, 139,
38, 141, 145 | lediv2ad 12536 |
. . . . . . 7
⊢ (𝜑 → (1 / (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) ≤ (1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2)))) |
147 | 73, 108, 82, 129, 146 | lemul1ad 11657 |
. . . . . 6
⊢ (𝜑 → ((1 / (((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))) ≤ ((1 / ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) |
148 | 83, 109, 37, 124, 147 | lemul2ad 11658 |
. . . . 5
⊢ (𝜑 → (2 · ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) ≤ (2 · ((1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))))) |
149 | 84, 110, 94, 148 | leadd1dd 11332 |
. . . 4
⊢ (𝜑 → ((2 · ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) ≤ ((2 · ((1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴)))) |
150 | 50, 18, 51, 46 | div23d 11531 |
. . . . . . . . . 10
⊢ (𝜑 → ((((log‘𝐴)↑5) ·
(log‘2)) / ((log‘2)↑5)) = ((((log‘𝐴)↑5) / ((log‘2)↑5)) ·
(log‘2))) |
151 | 150 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2)) = ((((log‘𝐴)↑5) ·
(log‘2)) / ((log‘2)↑5))) |
152 | 151 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) = (1 / ((((log‘𝐴)↑5) ·
(log‘2)) / ((log‘2)↑5)))) |
153 | 152 | oveq1d 7185 |
. . . . . . 7
⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))) = ((1 / ((((log‘𝐴)↑5) · (log‘2)) /
((log‘2)↑5))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) |
154 | 153 | oveq2d 7186 |
. . . . . 6
⊢ (𝜑 → (2 · ((1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) = (2 · ((1 / ((((log‘𝐴)↑5) ·
(log‘2)) / ((log‘2)↑5))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))))) |
155 | 18 | sqcld 13600 |
. . . . . . 7
⊢ (𝜑 → ((log‘2)↑2)
∈ ℂ) |
156 | 12, 91 | expcld 13602 |
. . . . . . 7
⊢ (𝜑 → ((log‘𝐴)↑1) ∈
ℂ) |
157 | 13, 155, 156, 2, 88, 11 | divmuldivd 11535 |
. . . . . 6
⊢ (𝜑 → ((2 /
((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) |
158 | 154, 157 | oveq12d 7188 |
. . . . 5
⊢ (𝜑 → ((2 · ((1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) = ((2 · ((1 / ((((log‘𝐴)↑5) ·
(log‘2)) / ((log‘2)↑5))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
159 | 50, 18 | mulcld 10739 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘𝐴)↑5) ·
(log‘2)) ∈ ℂ) |
160 | 50, 18, 105, 26 | mulne0d 11370 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘𝐴)↑5) ·
(log‘2)) ≠ 0) |
161 | 53, 159, 51, 160, 46 | divdiv2d 11526 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / ((((log‘𝐴)↑5) ·
(log‘2)) / ((log‘2)↑5))) = ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) ·
(log‘2)))) |
162 | 161 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝜑 → ((1 / ((((log‘𝐴)↑5) ·
(log‘2)) / ((log‘2)↑5))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴))) = (((1 · ((log‘2)↑5))
/ (((log‘𝐴)↑5)
· (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) |
163 | 162 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝜑 → (2 · ((1 /
((((log‘𝐴)↑5)
· (log‘2)) / ((log‘2)↑5))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) = (2 · (((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))))) |
164 | 53, 51 | mulcld 10739 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 ·
((log‘2)↑5)) ∈ ℂ) |
165 | 164, 159,
160 | divcld 11494 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ∈
ℂ) |
166 | 82 | recnd 10747 |
. . . . . . . . . 10
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) ∈ ℂ) |
167 | 13, 165, 166 | mulassd 10742 |
. . . . . . . . 9
⊢ (𝜑 → ((2 · ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) = (2 ·
(((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))))) |
168 | 167 | eqcomd 2744 |
. . . . . . . 8
⊢ (𝜑 → (2 · (((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) = ((2
· ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) |
169 | 163, 168 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → (2 · ((1 /
((((log‘𝐴)↑5)
· (log‘2)) / ((log‘2)↑5))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) = ((2 · ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) |
170 | 169 | oveq1d 7185 |
. . . . . 6
⊢ (𝜑 → ((2 · ((1 /
((((log‘𝐴)↑5)
· (log‘2)) / ((log‘2)↑5))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = (((2 · ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴)))) |
171 | 13, 164, 159, 160 | divassd 11529 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · (1 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (2
· ((1 · ((log‘2)↑5)) / (((log‘𝐴)↑5) ·
(log‘2))))) |
172 | 171 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → (2 · ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) = ((2
· (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) ·
(log‘2)))) |
173 | 172 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝜑 → ((2 · ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) = (((2
· (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) |
174 | 173 | oveq1d 7185 |
. . . . . . 7
⊢ (𝜑 → (((2 · ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) = ((((2
· (1 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴)))) |
175 | 13, 53, 51 | mulassd 10742 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 1) ·
((log‘2)↑5)) = (2 · (1 ·
((log‘2)↑5)))) |
176 | 175 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · (1 ·
((log‘2)↑5))) = ((2 · 1) ·
((log‘2)↑5))) |
177 | 176 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · (1 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) = (((2
· 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) ·
(log‘2)))) |
178 | 177 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝜑 → (((2 · (1 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) = ((((2
· 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) |
179 | 178 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝜑 → ((((2 · (1 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) = (((((2
· 1) · ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴)))) |
180 | 13 | mulid1d 10736 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 1) =
2) |
181 | 180 | oveq1d 7185 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 1) ·
((log‘2)↑5)) = (2 · ((log‘2)↑5))) |
182 | 181 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 · 1) ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) = ((2
· ((log‘2)↑5)) / (((log‘𝐴)↑5) ·
(log‘2)))) |
183 | 182 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (𝜑 → ((((2 · 1) ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) = (((2
· ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴)))) |
184 | 183 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝜑 → (((((2 · 1)
· ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) = ((((2
· ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴)))) |
185 | 13, 51 | mulcld 10739 |
. . . . . . . . . . . 12
⊢ (𝜑 → (2 ·
((log‘2)↑5)) ∈ ℂ) |
186 | 79 | recnd 10747 |
. . . . . . . . . . . 12
⊢ (𝜑 → (5 ·
((log‘𝐴)↑4))
∈ ℂ) |
187 | 51, 2 | mulcld 10739 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) ∈
ℂ) |
188 | 185, 159,
186, 187, 160, 81 | divmuldivd 11535 |
. . . . . . . . . . 11
⊢ (𝜑 → (((2 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) = (((2
· ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) /
((((log‘𝐴)↑5)
· (log‘2)) · (((log‘2)↑5) · 𝐴)))) |
189 | 188 | oveq1d 7185 |
. . . . . . . . . 10
⊢ (𝜑 → ((((2 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) = ((((2
· ((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) /
((((log‘𝐴)↑5)
· (log‘2)) · (((log‘2)↑5) · 𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
190 | 50, 18, 187 | mulassd 10742 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((log‘𝐴)↑5) ·
(log‘2)) · (((log‘2)↑5) · 𝐴)) = (((log‘𝐴)↑5) · ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) |
191 | 190 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 ·
((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) ·
(log‘2)) · (((log‘2)↑5) · 𝐴))) = (((2 · ((log‘2)↑5))
· (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) ·
(((log‘2)↑5) · 𝐴))))) |
192 | 191 | oveq1d 7185 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2 ·
((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) ·
(log‘2)) · (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = ((((2 · ((log‘2)↑5))
· (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
193 | 185, 186 | mulcomd 10740 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 ·
((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) = ((5 · ((log‘𝐴)↑4)) · (2 ·
((log‘2)↑5)))) |
194 | 18, 51, 2 | mulassd 10742 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((log‘2) ·
((log‘2)↑5)) · 𝐴) = ((log‘2) ·
(((log‘2)↑5) · 𝐴))) |
195 | 194 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((log‘2) ·
(((log‘2)↑5) · 𝐴)) = (((log‘2) ·
((log‘2)↑5)) · 𝐴)) |
196 | 195 | oveq2d 7186 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((log‘𝐴)↑5) ·
((log‘2) · (((log‘2)↑5) · 𝐴))) = (((log‘𝐴)↑5) · (((log‘2) ·
((log‘2)↑5)) · 𝐴))) |
197 | 193, 196 | oveq12d 7188 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((2 ·
((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) = (((5 · ((log‘𝐴)↑4)) · (2 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) ·
((log‘2)↑5)) · 𝐴)))) |
198 | 197 | oveq1d 7185 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((2 ·
((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = ((((5 · ((log‘𝐴)↑4)) · (2 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) ·
((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
199 | 18, 51 | mulcld 10739 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((log‘2) ·
((log‘2)↑5)) ∈ ℂ) |
200 | 199, 2 | mulcld 10739 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((log‘2) ·
((log‘2)↑5)) · 𝐴) ∈ ℂ) |
201 | 18, 51, 26, 46 | mulne0d 11370 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((log‘2) ·
((log‘2)↑5)) ≠ 0) |
202 | 199, 2, 201, 11 | mulne0d 11370 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((log‘2) ·
((log‘2)↑5)) · 𝐴) ≠ 0) |
203 | 186, 50, 185, 200, 105, 202 | divmuldivd 11535 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑4)) /
((log‘𝐴)↑5))
· ((2 · ((log‘2)↑5)) / (((log‘2) ·
((log‘2)↑5)) · 𝐴))) = (((5 · ((log‘𝐴)↑4)) · (2 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) ·
((log‘2)↑5)) · 𝐴)))) |
204 | 203 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑4))
· (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) ·
((log‘2)↑5)) · 𝐴))) = (((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 ·
((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5))
· 𝐴)))) |
205 | 204 | oveq1d 7185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((5 ·
((log‘𝐴)↑4))
· (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) ·
((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = ((((5 · ((log‘𝐴)↑4)) / ((log‘𝐴)↑5)) · ((2 ·
((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5))
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴)))) |
206 | 75 | recnd 10747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 5 ∈
ℂ) |
207 | 78 | recnd 10747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((log‘𝐴)↑4) ∈
ℂ) |
208 | 206, 207,
50, 105 | divassd 11529 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
((log‘𝐴)↑5)) =
(5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5)))) |
209 | 194 | oveq2d 7186 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((2 ·
((log‘2)↑5)) / (((log‘2) · ((log‘2)↑5))
· 𝐴)) = ((2 ·
((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5)
· 𝐴)))) |
210 | 208, 209 | oveq12d 7188 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑4)) /
((log‘𝐴)↑5))
· ((2 · ((log‘2)↑5)) / (((log‘2) ·
((log‘2)↑5)) · 𝐴))) = ((5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) · ((2
· ((log‘2)↑5)) / ((log‘2) ·
(((log‘2)↑5) · 𝐴))))) |
211 | 210 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((5 ·
((log‘𝐴)↑4)) /
((log‘𝐴)↑5))
· ((2 · ((log‘2)↑5)) / (((log‘2) ·
((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = (((5 · (((log‘𝐴)↑4) / ((log‘𝐴)↑5))) · ((2
· ((log‘2)↑5)) / ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
212 | 77 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 4 ∈
ℤ) |
213 | 12, 104, 45, 212 | expsubd 13613 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) =
(((log‘𝐴)↑4) /
((log‘𝐴)↑5))) |
214 | 213 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑(4 −
5))) |
215 | | 4p1e5 11862 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (4 + 1) =
5 |
216 | 74 | recni 10733 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 5 ∈
ℂ |
217 | 4 | recni 10733 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 4 ∈
ℂ |
218 | | ax-1cn 10673 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℂ |
219 | 216, 217,
218 | subaddi 11051 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((5
− 4) = 1 ↔ (4 + 1) = 5) |
220 | 215, 219 | mpbir 234 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (5
− 4) = 1 |
221 | 220 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (5 − 4) =
1) |
222 | 53 | subid1d 11064 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 − 0) =
1) |
223 | 221, 222 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (5 − 4) = (1 −
0)) |
224 | 206, 217 | jctir 524 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (5 ∈ ℂ ∧ 4
∈ ℂ)) |
225 | | 0cnd 10712 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 0 ∈
ℂ) |
226 | 53, 225 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (1 ∈ ℂ ∧ 0
∈ ℂ)) |
227 | | subeqrev 11140 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((5
∈ ℂ ∧ 4 ∈ ℂ) ∧ (1 ∈ ℂ ∧ 0 ∈
ℂ)) → ((5 − 4) = (1 − 0) ↔ (4 − 5) = (0
− 1))) |
228 | 224, 226,
227 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((5 − 4) = (1
− 0) ↔ (4 − 5) = (0 − 1))) |
229 | 223, 228 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (4 − 5) = (0 −
1)) |
230 | | df-neg 10951 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ -1 = (0
− 1) |
231 | 229, 230 | eqtr4di 2791 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (4 − 5) =
-1) |
232 | 231 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((log‘𝐴)↑(4 − 5)) =
((log‘𝐴)↑-1)) |
233 | 214, 232 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((log‘𝐴)↑4) / ((log‘𝐴)↑5)) = ((log‘𝐴)↑-1)) |
234 | 233 | oveq2d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (5 ·
(((log‘𝐴)↑4) /
((log‘𝐴)↑5))) =
(5 · ((log‘𝐴)↑-1))) |
235 | 13, 18, 51, 187, 26, 81 | divmuldivd 11535 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 / (log‘2))
· (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 ·
((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5)
· 𝐴)))) |
236 | 235 | eqcomd 2744 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((2 ·
((log‘2)↑5)) / ((log‘2) · (((log‘2)↑5)
· 𝐴))) = ((2 /
(log‘2)) · (((log‘2)↑5) / (((log‘2)↑5)
· 𝐴)))) |
237 | 234, 236 | oveq12d 7188 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((5 ·
(((log‘𝐴)↑4) /
((log‘𝐴)↑5)))
· ((2 · ((log‘2)↑5)) / ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) = ((5 · ((log‘𝐴)↑-1)) · ((2 /
(log‘2)) · (((log‘2)↑5) / (((log‘2)↑5)
· 𝐴))))) |
238 | 237 | oveq1d 7185 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((5 ·
(((log‘𝐴)↑4) /
((log‘𝐴)↑5)))
· ((2 · ((log‘2)↑5)) / ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = (((5 · ((log‘𝐴)↑-1)) · ((2 /
(log‘2)) · (((log‘2)↑5) / (((log‘2)↑5)
· 𝐴)))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴)))) |
239 | | 1zzd 12094 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 1 ∈
ℤ) |
240 | 12, 104, 239 | expnegd 13609 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((log‘𝐴)↑-1) = (1 /
((log‘𝐴)↑1))) |
241 | 240 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (5 ·
((log‘𝐴)↑-1)) =
(5 · (1 / ((log‘𝐴)↑1)))) |
242 | 51, 51, 2, 46, 11 | divdiv1d 11525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((((log‘2)↑5) /
((log‘2)↑5)) / 𝐴) = (((log‘2)↑5) /
(((log‘2)↑5) · 𝐴))) |
243 | 242 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((log‘2)↑5) /
(((log‘2)↑5) · 𝐴)) = ((((log‘2)↑5) /
((log‘2)↑5)) / 𝐴)) |
244 | 243 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((2 / (log‘2))
· (((log‘2)↑5) / (((log‘2)↑5) · 𝐴))) = ((2 / (log‘2))
· ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴))) |
245 | 241, 244 | oveq12d 7188 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑-1))
· ((2 / (log‘2)) · (((log‘2)↑5) /
(((log‘2)↑5) · 𝐴)))) = ((5 · (1 / ((log‘𝐴)↑1))) · ((2 /
(log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) /
𝐴)))) |
246 | 245 | oveq1d 7185 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑-1))
· ((2 / (log‘2)) · (((log‘2)↑5) /
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = (((5 · (1 / ((log‘𝐴)↑1))) · ((2 /
(log‘2)) · ((((log‘2)↑5) / ((log‘2)↑5)) /
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
247 | 12, 104, 239 | expne0d 13608 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((log‘𝐴)↑1) ≠
0) |
248 | 206, 53, 156, 247 | divassd 11529 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((5 · 1) /
((log‘𝐴)↑1)) =
(5 · (1 / ((log‘𝐴)↑1)))) |
249 | 248 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (5 · (1 /
((log‘𝐴)↑1))) =
((5 · 1) / ((log‘𝐴)↑1))) |
250 | 51, 46 | dividd 11492 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((log‘2)↑5) /
((log‘2)↑5)) = 1) |
251 | 250 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((((log‘2)↑5) /
((log‘2)↑5)) / 𝐴) = (1 / 𝐴)) |
252 | 251 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((2 / (log‘2))
· ((((log‘2)↑5) / ((log‘2)↑5)) / 𝐴)) = ((2 / (log‘2)) · (1 /
𝐴))) |
253 | 249, 252 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((5 · (1 /
((log‘𝐴)↑1)))
· ((2 / (log‘2)) · ((((log‘2)↑5) /
((log‘2)↑5)) / 𝐴))) = (((5 · 1) / ((log‘𝐴)↑1)) · ((2 /
(log‘2)) · (1 / 𝐴)))) |
254 | 253 | oveq1d 7185 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((5 · (1 /
((log‘𝐴)↑1)))
· ((2 / (log‘2)) · ((((log‘2)↑5) /
((log‘2)↑5)) / 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = ((((5 · 1) / ((log‘𝐴)↑1)) · ((2 /
(log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
255 | 206 | mulid1d 10736 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (5 · 1) =
5) |
256 | 255 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((5 · 1) /
((log‘𝐴)↑1)) =
(5 / ((log‘𝐴)↑1))) |
257 | 13, 18, 53, 2, 26, 11 | divmuldivd 11535 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((2 / (log‘2))
· (1 / 𝐴)) = ((2
· 1) / ((log‘2) · 𝐴))) |
258 | 256, 257 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((5 · 1) /
((log‘𝐴)↑1))
· ((2 / (log‘2)) · (1 / 𝐴))) = ((5 / ((log‘𝐴)↑1)) · ((2 · 1) /
((log‘2) · 𝐴)))) |
259 | 258 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((5 · 1) /
((log‘𝐴)↑1))
· ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = (((5 / ((log‘𝐴)↑1)) · ((2 · 1) /
((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
260 | 180, 13 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (2 · 1) ∈
ℂ) |
261 | 18, 2 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((log‘2) ·
𝐴) ∈
ℂ) |
262 | 18, 2, 26, 11 | mulne0d 11370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((log‘2) ·
𝐴) ≠ 0) |
263 | 206, 156,
260, 261, 247, 262 | divmuldivd 11535 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 ·
1) / ((log‘2) · 𝐴))) = ((5 · (2 · 1)) /
(((log‘𝐴)↑1)
· ((log‘2) · 𝐴)))) |
264 | 180 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (5 · (2 ·
1)) = (5 · 2)) |
265 | 264 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((5 · (2 ·
1)) / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) = ((5 · 2) /
(((log‘𝐴)↑1)
· ((log‘2) · 𝐴)))) |
266 | 263, 265 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((5 / ((log‘𝐴)↑1)) · ((2 ·
1) / ((log‘2) · 𝐴))) = ((5 · 2) / (((log‘𝐴)↑1) ·
((log‘2) · 𝐴)))) |
267 | 266 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 ·
1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = (((5 · 2) / (((log‘𝐴)↑1) ·
((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
268 | | 5t2e10 12279 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (5
· 2) = ;10 |
269 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (5 · 2) = ;10) |
270 | 269 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((5 · 2) /
(((log‘𝐴)↑1)
· ((log‘2) · 𝐴))) = (;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴)))) |
271 | 270 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((5 · 2) /
(((log‘𝐴)↑1)
· ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) = ((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)))) |
272 | | 10nn0 12197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ;10 ∈
ℕ0 |
273 | 272 | nn0cni 11988 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ;10 ∈ ℂ |
274 | 273 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ;10 ∈ ℂ) |
275 | 274 | mulid1d 10736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (;10 · 1) = ;10) |
276 | 275 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 / (((log‘𝐴)↑1) ·
(log‘2)))) |
277 | 13, 156 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (2 ·
((log‘𝐴)↑1))
∈ ℂ) |
278 | 277, 155,
88 | divcld 11494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑2)) ∈ ℂ) |
279 | 278 | mulid2d 10737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (1 · ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) /
((log‘2)↑2))) |
280 | 276, 279 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1
· ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) =
((;10 / (((log‘𝐴)↑1) ·
(log‘2))) + ((2 · ((log‘𝐴)↑1)) /
((log‘2)↑2)))) |
281 | 18, 91 | expcld 13602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ((log‘2)↑1)
∈ ℂ) |
282 | 18, 26, 239 | expne0d 13608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ((log‘2)↑1)
≠ 0) |
283 | 277, 281,
282 | divcld 11494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)) ∈ ℂ) |
284 | 283 | mulid1d 10736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)) · 1) = ((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1))) |
285 | 284 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1)) · 1)) = ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1)))) |
286 | | 10re 12198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ;10 ∈ ℝ |
287 | 286 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ;10 ∈ ℝ) |
288 | 287, 40, 104 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (;10 / (log‘𝐴)) ∈ ℝ) |
289 | 40, 43, 26 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → ((log‘𝐴) / (log‘2)) ∈
ℝ) |
290 | 289, 91 | reexpcld 13619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1)
∈ ℝ) |
291 | 37, 290 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (2 ·
(((log‘𝐴) /
(log‘2))↑1)) ∈ ℝ) |
292 | 288, 291 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1)))
∈ ℝ) |
293 | 287, 291 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ∈
ℝ) |
294 | 43, 112 | reexpcld 13619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((log‘2)↑3)
∈ ℝ) |
295 | | 3z 12096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ 3 ∈
ℤ |
296 | 295 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → 3 ∈
ℤ) |
297 | 18, 26, 296 | expne0d 13608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((log‘2)↑3)
≠ 0) |
298 | 113, 294,
297 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (((log‘𝐴)↑3) /
((log‘2)↑3)) ∈ ℝ) |
299 | 5, 298 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (4 ·
(((log‘𝐴)↑3) /
((log‘2)↑3))) ∈ ℝ) |
300 | | ere 15534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ e ∈
ℝ |
301 | 300 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → e ∈
ℝ) |
302 | 112 | nn0red 12037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → 3 ∈
ℝ) |
303 | | egt2lt3 15651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (2 < e
∧ e < 3) |
304 | 303 | simpri 489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ e <
3 |
305 | 304 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → e < 3) |
306 | | 3lt4 11890 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 3 <
4 |
307 | 306 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → 3 < 4) |
308 | 302, 5, 1, 307, 8 | ltletrd 10878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → 3 < 𝐴) |
309 | 301, 302,
1, 305, 308 | lttrd 10879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → e < 𝐴) |
310 | 301, 1, 309 | ltled 10866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → e ≤ 𝐴) |
311 | 301, 1 | lenltd 10864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → (e ≤ 𝐴 ↔ ¬ 𝐴 < e)) |
312 | 310, 311 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → ¬ 𝐴 < e) |
313 | | loglt1b 25377 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐴 ∈ ℝ+
→ ((log‘𝐴) <
1 ↔ 𝐴 <
e)) |
314 | 39, 313 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → ((log‘𝐴) < 1 ↔ 𝐴 < e)) |
315 | 312, 314 | mtbird 328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → ¬ (log‘𝐴) < 1) |
316 | 38, 40 | lenltd 10864 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ ¬ (log‘𝐴) < 1)) |
317 | 315, 316 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → 1 ≤ (log‘𝐴)) |
318 | | 10nn 12195 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ;10 ∈ ℕ |
319 | 318 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → ;10 ∈ ℕ) |
320 | | nnledivrp 12584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((;10 ∈ ℕ ∧
(log‘𝐴) ∈
ℝ+) → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10)) |
321 | 319, 130,
320 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (1 ≤ (log‘𝐴) ↔ (;10 / (log‘𝐴)) ≤ ;10)) |
322 | 317, 321 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (;10 / (log‘𝐴)) ≤ ;10) |
323 | 288, 287,
291, 322 | leadd1dd 11332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1)))
≤ (;10 + (2 ·
(((log‘𝐴) /
(log‘2))↑1)))) |
324 | 38, 55 | gtned 10853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → 2 ≠ 1) |
325 | 37, 15, 1, 9, 324 | relogbcld 39620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (2 logb 𝐴) ∈
ℝ) |
326 | 325, 91 | reexpcld 13619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈
ℝ) |
327 | 42, 55 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝜑 → (2 ∈
ℝ+ ∧ 1 < 2)) |
328 | | logbgt0b 25531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝐴 ∈ ℝ+
∧ (2 ∈ ℝ+ ∧ 1 < 2)) → (0 < (2
logb 𝐴) ↔ 1
< 𝐴)) |
329 | 39, 327, 328 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝜑 → (0 < (2 logb
𝐴) ↔ 1 < 𝐴)) |
330 | 99, 329 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → 0 < (2 logb
𝐴)) |
331 | 325, 330 | elrpd 12511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → (2 logb 𝐴) ∈
ℝ+) |
332 | 331, 239 | rpexpcld 13700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈
ℝ+) |
333 | 332 | rpne0d 12519 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((2 logb 𝐴)↑1) ≠
0) |
334 | 287, 326,
333 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) ∈ ℝ) |
335 | 334, 37 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ∈
ℝ) |
336 | | sq2 13652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(2↑2) = 4 |
337 | 336 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → (2↑2) =
4) |
338 | 337, 5 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → (2↑2) ∈
ℝ) |
339 | 5, 338 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (4 · (2↑2))
∈ ℝ) |
340 | 325 | resqcld 13703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → ((2 logb 𝐴)↑2) ∈
ℝ) |
341 | 5, 340 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (4 · ((2
logb 𝐴)↑2))
∈ ℝ) |
342 | 325 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → (2 logb 𝐴) ∈
ℂ) |
343 | 342 | exp1d 13597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → ((2 logb 𝐴)↑1) = (2 logb
𝐴)) |
344 | 343 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → (;10 / ((2 logb 𝐴)↑1)) = (;10 / (2 logb 𝐴))) |
345 | 344 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 / (2 logb 𝐴)) + 2)) |
346 | 345, 335 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ∈ ℝ) |
347 | 287 | rehalfcld 11963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (;10 / 2) ∈ ℝ) |
348 | 347, 37 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((;10 / 2) + 2) ∈ ℝ) |
349 | 344, 334 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (;10 / (2 logb 𝐴)) ∈ ℝ) |
350 | 287, 37, 17 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (;10 / 2) ∈ ℝ) |
351 | 272 | nn0ge0i 12003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 0 ≤
;10 |
352 | 351 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → 0 ≤ ;10) |
353 | 42, 324, 87 | relogbexpd 39621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝜑 → (2 logb
(2↑2)) = 2) |
354 | 353 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝜑 → 2 = (2 logb
(2↑2))) |
355 | 337 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝜑 → (2 logb
(2↑2)) = (2 logb 4)) |
356 | 354, 355 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → 2 = (2 logb
4)) |
357 | 37 | leidd 11284 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝜑 → 2 ≤ 2) |
358 | 87, 357, 5, 7, 1, 9, 8 | logblebd 39623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → (2 logb 4) ≤
(2 logb 𝐴)) |
359 | 356, 358 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → 2 ≤ (2 logb
𝐴)) |
360 | 42, 331, 287, 352, 359 | lediv2ad 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (;10 / (2 logb 𝐴)) ≤ (;10 / 2)) |
361 | 349, 350,
37, 360 | leadd1dd 11332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ ((;10 / 2) + 2)) |
362 | | 1nn 11727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 1 ∈
ℕ |
363 | | 6nn0 11997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ 6 ∈
ℕ0 |
364 | | 2nn0 11993 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ 2 ∈
ℕ0 |
365 | 27, 364 | nn0addcli 12013 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (5 + 2)
∈ ℕ0 |
366 | | 5p2e7 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (5 + 2) =
7 |
367 | | 7re 11809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ 7 ∈
ℝ |
368 | 367, 364 | nn0addge1i 12024 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ 7 ≤ (7
+ 2) |
369 | | 7p2e9 11877 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (7 + 2) =
9 |
370 | 368, 369 | breqtri 5055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ 7 ≤
9 |
371 | 366, 370 | eqbrtri 5051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (5 + 2)
≤ 9 |
372 | 362, 363,
365, 371 | declei 12215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (5 + 2)
≤ ;16 |
373 | 372 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (5 + 2) ≤ ;16) |
374 | 206, 13, 274, 17 | ldiv 11552 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → ((5 · 2) = ;10 ↔ 5 = (;10 / 2))) |
375 | 269, 374 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → 5 = (;10 / 2)) |
376 | 375 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (5 + 2) = ((;10 / 2) + 2)) |
377 | | 4t4e16 12278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (4
· 4) = ;16 |
378 | 377 | eqcomi 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ;16 = (4 · 4) |
379 | 378 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → ;16 = (4 · 4)) |
380 | 337 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → 4 =
(2↑2)) |
381 | 380 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → (4 · 4) = (4
· (2↑2))) |
382 | 379, 381 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → ;16 = (4 · (2↑2))) |
383 | 373, 376,
382 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((;10 / 2) + 2) ≤ (4 ·
(2↑2))) |
384 | 346, 348,
339, 361, 383 | letrd 10875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → ((;10 / (2 logb 𝐴)) + 2) ≤ (4 ·
(2↑2))) |
385 | 345, 384 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 ·
(2↑2))) |
386 | 3, 5, 7 | ltled 10866 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → 0 ≤ 4) |
387 | 364 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → 2 ∈
ℕ0) |
388 | 37, 325, 387, 124, 359 | leexp1ad 39619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → (2↑2) ≤ ((2
logb 𝐴)↑2)) |
389 | 338, 340,
5, 386, 388 | lemul2ad 11658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (4 · (2↑2))
≤ (4 · ((2 logb 𝐴)↑2))) |
390 | 335, 339,
341, 385, 389 | letrd 10875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) ≤ (4 · ((2
logb 𝐴)↑2))) |
391 | 37, 326 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (2 · ((2
logb 𝐴)↑1))
∈ ℝ) |
392 | 391 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → (2 · ((2
logb 𝐴)↑1))
∈ ℂ) |
393 | 326 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((2 logb 𝐴)↑1) ∈
ℂ) |
394 | 274, 392,
393, 333 | divdird 11532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2
logb 𝐴)↑1))
= ((;10 / ((2 logb
𝐴)↑1)) + ((2 ·
((2 logb 𝐴)↑1)) / ((2 logb 𝐴)↑1)))) |
395 | 13, 393, 393, 333 | divassd 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → ((2 · ((2
logb 𝐴)↑1))
/ ((2 logb 𝐴)↑1)) = (2 · (((2
logb 𝐴)↑1)
/ ((2 logb 𝐴)↑1)))) |
396 | 395 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + ((2 · ((2
logb 𝐴)↑1))
/ ((2 logb 𝐴)↑1))) = ((;10 / ((2 logb 𝐴)↑1)) + (2 · (((2
logb 𝐴)↑1)
/ ((2 logb 𝐴)↑1))))) |
397 | 393, 333 | dividd 11492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → (((2 logb 𝐴)↑1) / ((2 logb
𝐴)↑1)) =
1) |
398 | 397 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → (2 · (((2
logb 𝐴)↑1)
/ ((2 logb 𝐴)↑1))) = (2 ·
1)) |
399 | 398, 180 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (2 · (((2
logb 𝐴)↑1)
/ ((2 logb 𝐴)↑1))) = 2) |
400 | 399 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + (2 · (((2
logb 𝐴)↑1)
/ ((2 logb 𝐴)↑1)))) = ((;10 / ((2 logb 𝐴)↑1)) + 2)) |
401 | 396, 400 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + ((2 · ((2
logb 𝐴)↑1))
/ ((2 logb 𝐴)↑1))) = ((;10 / ((2 logb 𝐴)↑1)) + 2)) |
402 | 394, 401 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2
logb 𝐴)↑1))
= ((;10 / ((2 logb
𝐴)↑1)) +
2)) |
403 | 402 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → ((;10 / ((2 logb 𝐴)↑1)) + 2) = ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2
logb 𝐴)↑1))) |
404 | | 2p1e3 11858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (2 + 1) =
3 |
405 | 404 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → (2 + 1) =
3) |
406 | 302 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝜑 → 3 ∈
ℂ) |
407 | 406, 53, 13 | subadd2d 11094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝜑 → ((3 − 1) = 2 ↔
(2 + 1) = 3)) |
408 | 405, 407 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝜑 → (3 − 1) =
2) |
409 | 408 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → 2 = (3 −
1)) |
410 | 409 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((2 logb 𝐴)↑2) = ((2 logb
𝐴)↑(3 −
1))) |
411 | 410 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → (4 · ((2
logb 𝐴)↑2))
= (4 · ((2 logb 𝐴)↑(3 − 1)))) |
412 | 3, 330 | gtned 10853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → (2 logb 𝐴) ≠ 0) |
413 | 342, 412,
239, 296 | expsubd 13613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((2 logb 𝐴)↑(3 − 1)) = (((2
logb 𝐴)↑3)
/ ((2 logb 𝐴)↑1))) |
414 | 413 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → (4 · ((2
logb 𝐴)↑(3
− 1))) = (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))) |
415 | 411, 414 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (4 · ((2
logb 𝐴)↑2))
= (4 · (((2 logb 𝐴)↑3) / ((2 logb 𝐴)↑1)))) |
416 | 217 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → 4 ∈
ℂ) |
417 | 325, 112 | reexpcld 13619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈
ℝ) |
418 | 417 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → ((2 logb 𝐴)↑3) ∈
ℂ) |
419 | 416, 418,
393, 333 | divassd 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → ((4 · ((2
logb 𝐴)↑3))
/ ((2 logb 𝐴)↑1)) = (4 · (((2
logb 𝐴)↑3)
/ ((2 logb 𝐴)↑1)))) |
420 | 419 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (4 · (((2
logb 𝐴)↑3)
/ ((2 logb 𝐴)↑1))) = ((4 · ((2
logb 𝐴)↑3))
/ ((2 logb 𝐴)↑1))) |
421 | 415, 420 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → (4 · ((2
logb 𝐴)↑2))
= ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1))) |
422 | 390, 403,
421 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) / ((2
logb 𝐴)↑1))
≤ ((4 · ((2 logb 𝐴)↑3)) / ((2 logb 𝐴)↑1))) |
423 | 287, 391 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ∈
ℝ) |
424 | 5, 417 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → (4 · ((2
logb 𝐴)↑3))
∈ ℝ) |
425 | 423, 424,
332 | lediv1d 12560 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2
logb 𝐴)↑3))
↔ ((;10 + (2 · ((2
logb 𝐴)↑1))) / ((2 logb 𝐴)↑1)) ≤ ((4 · ((2
logb 𝐴)↑3))
/ ((2 logb 𝐴)↑1)))) |
426 | 422, 425 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) ≤ (4 · ((2
logb 𝐴)↑3))) |
427 | 87 | uzidd 12340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝜑 → 2 ∈
(ℤ≥‘2)) |
428 | 427, 39 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝜑 → (2 ∈
(ℤ≥‘2) ∧ 𝐴 ∈
ℝ+)) |
429 | | relogbval 25510 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((2
∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℝ+) → (2
logb 𝐴) =
((log‘𝐴) /
(log‘2))) |
430 | 428, 429 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) /
(log‘2))) |
431 | 430 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → ((2 logb 𝐴)↑1) = (((log‘𝐴) /
(log‘2))↑1)) |
432 | 431 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (2 · ((2
logb 𝐴)↑1))
= (2 · (((log‘𝐴) /
(log‘2))↑1))) |
433 | 432 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (;10 + (2 · ((2 logb 𝐴)↑1))) = (;10 + (2 · (((log‘𝐴) /
(log‘2))↑1)))) |
434 | 430 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴) /
(log‘2))↑3)) |
435 | 12, 18, 26, 112 | expdivd 13616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑3) =
(((log‘𝐴)↑3) /
((log‘2)↑3))) |
436 | 434, 435 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((2 logb 𝐴)↑3) = (((log‘𝐴)↑3) /
((log‘2)↑3))) |
437 | 436 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (4 · ((2
logb 𝐴)↑3))
= (4 · (((log‘𝐴)↑3) /
((log‘2)↑3)))) |
438 | 426, 433,
437 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (;10 + (2 · (((log‘𝐴) / (log‘2))↑1))) ≤ (4
· (((log‘𝐴)↑3) /
((log‘2)↑3)))) |
439 | 292, 293,
299, 323, 438 | letrd 10875 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1)))
≤ (4 · (((log‘𝐴)↑3) /
((log‘2)↑3)))) |
440 | 12 | exp1d 13597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((log‘𝐴)↑1) = (log‘𝐴)) |
441 | 440 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (log‘𝐴) = ((log‘𝐴)↑1)) |
442 | 441 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (;10 / (log‘𝐴)) = (;10 / ((log‘𝐴)↑1))) |
443 | 13, 156, 281, 282 | divassd 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)) = (2 · (((log‘𝐴)↑1) /
((log‘2)↑1)))) |
444 | 12, 18, 26, 91 | expdivd 13616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑1) =
(((log‘𝐴)↑1) /
((log‘2)↑1))) |
445 | 444 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝜑 → (((log‘𝐴)↑1) /
((log‘2)↑1)) = (((log‘𝐴) / (log‘2))↑1)) |
446 | 445 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝜑 → (2 ·
(((log‘𝐴)↑1) /
((log‘2)↑1))) = (2 · (((log‘𝐴) /
(log‘2))↑1))) |
447 | 443, 446 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)) = (2 · (((log‘𝐴) /
(log‘2))↑1))) |
448 | 447 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (2 ·
(((log‘𝐴) /
(log‘2))↑1)) = ((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1))) |
449 | 442, 448 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((;10 / (log‘𝐴)) + (2 · (((log‘𝐴) / (log‘2))↑1))) =
((;10 / ((log‘𝐴)↑1)) + ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)))) |
450 | 113 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ((log‘𝐴)↑3) ∈
ℂ) |
451 | 18, 112 | expcld 13602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ((log‘2)↑3)
∈ ℂ) |
452 | 416, 450,
451, 297 | divassd 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑3)) = (4 · (((log‘𝐴)↑3) /
((log‘2)↑3)))) |
453 | 452 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (4 ·
(((log‘𝐴)↑3) /
((log‘2)↑3))) = ((4 · ((log‘𝐴)↑3)) /
((log‘2)↑3))) |
454 | 439, 449,
453 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + ((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1))) ≤ ((4 · ((log‘𝐴)↑3)) /
((log‘2)↑3))) |
455 | 285, 454 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1)) · 1)) ≤ ((4 · ((log‘𝐴)↑3)) /
((log‘2)↑3))) |
456 | 281, 282 | dividd 11492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (((log‘2)↑1) /
((log‘2)↑1)) = 1) |
457 | 456 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 1 =
(((log‘2)↑1) / ((log‘2)↑1))) |
458 | 457 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1)) · (((log‘2)↑1) /
((log‘2)↑1)))) |
459 | 277, 281,
281, 281, 282, 282 | divmuldivd 11535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)) · (((log‘2)↑1) /
((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · ((log‘2)↑1))
/ (((log‘2)↑1) · ((log‘2)↑1)))) |
460 | 458, 459 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑1)) · 1) = (((2 · ((log‘𝐴)↑1)) ·
((log‘2)↑1)) / (((log‘2)↑1) ·
((log‘2)↑1)))) |
461 | 460 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) /
((log‘2)↑1)) · 1)) = ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) ·
((log‘2)↑1)) / (((log‘2)↑1) ·
((log‘2)↑1))))) |
462 | 416, 450 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (4 ·
((log‘𝐴)↑3))
∈ ℂ) |
463 | 462, 451,
297 | divcld 11494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑3)) ∈ ℂ) |
464 | 463 | mulid1d 10736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑3)) · 1) = ((4 · ((log‘𝐴)↑3)) /
((log‘2)↑3))) |
465 | 464 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑3)) = (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3))
· 1)) |
466 | 455, 461,
465 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) ·
((log‘2)↑1)) / (((log‘2)↑1) ·
((log‘2)↑1)))) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑3))
· 1)) |
467 | 274, 156,
247 | divcld 11494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) ∈ ℂ) |
468 | 467 | mulid1d 10736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = (;10 / ((log‘𝐴)↑1))) |
469 | 468 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · 1)) |
470 | 18, 26 | dividd 11492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → ((log‘2) /
(log‘2)) = 1) |
471 | 470 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → 1 = ((log‘2) /
(log‘2))) |
472 | 471 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · 1) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) /
(log‘2)))) |
473 | 469, 472 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 / ((log‘𝐴)↑1)) · ((log‘2) /
(log‘2)))) |
474 | 274, 156,
18, 18, 247, 26 | divmuldivd 11535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) · ((log‘2) /
(log‘2))) = ((;10 ·
(log‘2)) / (((log‘𝐴)↑1) ·
(log‘2)))) |
475 | 473, 474 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (;10 / ((log‘𝐴)↑1)) = ((;10 · (log‘2)) / (((log‘𝐴)↑1) ·
(log‘2)))) |
476 | 18 | exp1d 13597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((log‘2)↑1) =
(log‘2)) |
477 | 476 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1))
· ((log‘2)↑1)) = ((2 · ((log‘𝐴)↑1)) ·
(log‘2))) |
478 | | df-2 11779 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ 2 = (1 +
1) |
479 | 478 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝜑 → 2 = (1 +
1)) |
480 | 479 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((log‘2)↑2) =
((log‘2)↑(1 + 1))) |
481 | 18, 91, 91 | expaddd 13604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → ((log‘2)↑(1 +
1)) = (((log‘2)↑1) ·
((log‘2)↑1))) |
482 | 480, 481 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((log‘2)↑2) =
(((log‘2)↑1) · ((log‘2)↑1))) |
483 | 482 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (((log‘2)↑1)
· ((log‘2)↑1)) = ((log‘2)↑2)) |
484 | 477, 483 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (((2 ·
((log‘𝐴)↑1))
· ((log‘2)↑1)) / (((log‘2)↑1) ·
((log‘2)↑1))) = (((2 · ((log‘𝐴)↑1)) · (log‘2)) /
((log‘2)↑2))) |
485 | 475, 484 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ((;10 / ((log‘𝐴)↑1)) + (((2 · ((log‘𝐴)↑1)) ·
((log‘2)↑1)) / (((log‘2)↑1) ·
((log‘2)↑1)))) = (((;10
· (log‘2)) / (((log‘𝐴)↑1) · (log‘2))) + (((2
· ((log‘𝐴)↑1)) · (log‘2)) /
((log‘2)↑2)))) |
486 | 476 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝜑 → (log‘2) =
((log‘2)↑1)) |
487 | 486 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → ((log‘2) /
(log‘2)) = ((log‘2) / ((log‘2)↑1))) |
488 | 471, 487 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → 1 = ((log‘2) /
((log‘2)↑1))) |
489 | 488 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) /
((log‘2)↑3)) · ((log‘2) /
((log‘2)↑1)))) |
490 | 476, 18 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((log‘2)↑1)
∈ ℂ) |
491 | 476, 26 | eqnetrd 3001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((log‘2)↑1)
≠ 0) |
492 | 462, 451,
18, 490, 297, 491 | divmuldivd 11535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑3)) · ((log‘2) / ((log‘2)↑1))) =
(((4 · ((log‘𝐴)↑3)) · (log‘2)) /
(((log‘2)↑3) · ((log‘2)↑1)))) |
493 | 489, 492 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑3)) · 1) = (((4 · ((log‘𝐴)↑3)) ·
(log‘2)) / (((log‘2)↑3) ·
((log‘2)↑1)))) |
494 | 466, 485,
493 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (((;10 · (log‘2)) / (((log‘𝐴)↑1) ·
(log‘2))) + (((2 · ((log‘𝐴)↑1)) · (log‘2)) /
((log‘2)↑2))) ≤ (((4 · ((log‘𝐴)↑3)) · (log‘2)) /
(((log‘2)↑3) · ((log‘2)↑1)))) |
495 | 156, 18 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (((log‘𝐴)↑1) ·
(log‘2)) ∈ ℂ) |
496 | 156, 18, 247, 26 | mulne0d 11370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (((log‘𝐴)↑1) ·
(log‘2)) ≠ 0) |
497 | 274, 18, 495, 496 | div23d 11531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ((;10 · (log‘2)) / (((log‘𝐴)↑1) ·
(log‘2))) = ((;10 /
(((log‘𝐴)↑1)
· (log‘2))) · (log‘2))) |
498 | 277, 18, 155, 88 | div23d 11531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (((2 ·
((log‘𝐴)↑1))
· (log‘2)) / ((log‘2)↑2)) = (((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑2)) · (log‘2))) |
499 | 497, 498 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (((;10 · (log‘2)) / (((log‘𝐴)↑1) ·
(log‘2))) + (((2 · ((log‘𝐴)↑1)) · (log‘2)) /
((log‘2)↑2))) = (((;10
/ (((log‘𝐴)↑1)
· (log‘2))) · (log‘2)) + (((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑2)) · (log‘2)))) |
500 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝜑 → 4 = (3 +
1)) |
501 | 500 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((log‘2)↑4) =
((log‘2)↑(3 + 1))) |
502 | 18, 91, 112 | expaddd 13604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → ((log‘2)↑(3 +
1)) = (((log‘2)↑3) ·
((log‘2)↑1))) |
503 | 501, 502 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → ((log‘2)↑4) =
(((log‘2)↑3) · ((log‘2)↑1))) |
504 | 503 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (((log‘2)↑3)
· ((log‘2)↑1)) = ((log‘2)↑4)) |
505 | 504 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3))
· (log‘2)) / (((log‘2)↑3) ·
((log‘2)↑1))) = (((4 · ((log‘𝐴)↑3)) · (log‘2)) /
((log‘2)↑4))) |
506 | 494, 499,
505 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) ·
(log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))
· (log‘2))) ≤ (((4 · ((log‘𝐴)↑3)) · (log‘2)) /
((log‘2)↑4))) |
507 | 92, 43 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝜑 → (((log‘𝐴)↑1) ·
(log‘2)) ∈ ℝ) |
508 | 287, 507,
496 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈
ℝ) |
509 | 508 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · (log‘2))) ∈
ℂ) |
510 | 509, 278,
18 | adddird 10744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2
· ((log‘𝐴)↑1)) / ((log‘2)↑2)))
· (log‘2)) = (((;10 /
(((log‘𝐴)↑1)
· (log‘2))) · (log‘2)) + (((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑2)) · (log‘2)))) |
511 | 510 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) ·
(log‘2)) + (((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2))
· (log‘2))) = (((;10
/ (((log‘𝐴)↑1)
· (log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
· (log‘2))) |
512 | 18, 26, 212 | expne0d 13608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ((log‘2)↑4)
≠ 0) |
513 | 462, 18, 117, 512 | div23d 11531 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3))
· (log‘2)) / ((log‘2)↑4)) = (((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑4)) · (log‘2))) |
514 | 506, 511,
513 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2
· ((log‘𝐴)↑1)) / ((log‘2)↑2)))
· (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4))
· (log‘2))) |
515 | 37, 92 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → (2 ·
((log‘𝐴)↑1))
∈ ℝ) |
516 | 515, 85, 88 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑2)) ∈ ℝ) |
517 | 508, 516 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2
· ((log‘𝐴)↑1)) / ((log‘2)↑2))) ∈
ℝ) |
518 | 114, 115,
120 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑4)) ∈ ℝ) |
519 | 517, 518,
135 | lemul1d 12557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2
· ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤
((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4)) ↔
(((;10 / (((log‘𝐴)↑1) ·
(log‘2))) + ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))
· (log‘2)) ≤ (((4 · ((log‘𝐴)↑3)) / ((log‘2)↑4))
· (log‘2)))) |
520 | 514, 519 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · (log‘2))) + ((2
· ((log‘𝐴)↑1)) / ((log‘2)↑2))) ≤
((4 · ((log‘𝐴)↑3)) /
((log‘2)↑4))) |
521 | 280, 520 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1
· ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) ≤
((4 · ((log‘𝐴)↑3)) /
((log‘2)↑4))) |
522 | 274, 53, 495, 496 | divassd 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) = (;10 · (1 / (((log‘𝐴)↑1) ·
(log‘2))))) |
523 | 53, 277, 155, 88 | div12d 11530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (1 · ((2 ·
((log‘𝐴)↑1)) /
((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 /
((log‘2)↑2)))) |
524 | 522, 523 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((;10 · 1) / (((log‘𝐴)↑1) · (log‘2))) + (1
· ((2 · ((log‘𝐴)↑1)) / ((log‘2)↑2)))) =
((;10 · (1 /
(((log‘𝐴)↑1)
· (log‘2)))) + ((2 · ((log‘𝐴)↑1)) · (1 /
((log‘2)↑2))))) |
525 | 462 | mulid1d 10736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3))
· 1) = (4 · ((log‘𝐴)↑3))) |
526 | 525 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (4 ·
((log‘𝐴)↑3)) =
((4 · ((log‘𝐴)↑3)) · 1)) |
527 | 526 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3)) /
((log‘2)↑4)) = (((4 · ((log‘𝐴)↑3)) · 1) /
((log‘2)↑4))) |
528 | 521, 524,
527 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2
· ((log‘𝐴)↑1)) · (1 /
((log‘2)↑2)))) ≤ (((4 · ((log‘𝐴)↑3)) · 1) /
((log‘2)↑4))) |
529 | 2, 11 | dividd 11492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → (𝐴 / 𝐴) = 1) |
530 | 529 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 1 = (𝐴 / 𝐴)) |
531 | 530 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (1 / (((log‘𝐴)↑1) ·
(log‘2))) = ((𝐴 /
𝐴) / (((log‘𝐴)↑1) ·
(log‘2)))) |
532 | 2, 2, 495, 11, 496 | divdiv1d 11525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((𝐴 / 𝐴) / (((log‘𝐴)↑1) · (log‘2))) = (𝐴 / (𝐴 · (((log‘𝐴)↑1) ·
(log‘2))))) |
533 | 531, 532 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (1 / (((log‘𝐴)↑1) ·
(log‘2))) = (𝐴 /
(𝐴 ·
(((log‘𝐴)↑1)
· (log‘2))))) |
534 | 533 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) = (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) ·
(log‘2)))))) |
535 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1))
· (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · (1 /
((log‘2)↑2)))) |
536 | 530 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (1 /
((log‘2)↑2)) = ((𝐴 / 𝐴) /
((log‘2)↑2))) |
537 | 536 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1))
· (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) /
((log‘2)↑2)))) |
538 | 535, 537 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1))
· (1 / ((log‘2)↑2))) = ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) /
((log‘2)↑2)))) |
539 | 534, 538 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((;10 · (1 / (((log‘𝐴)↑1) · (log‘2)))) + ((2
· ((log‘𝐴)↑1)) · (1 /
((log‘2)↑2)))) = ((;10
· (𝐴 / (𝐴 · (((log‘𝐴)↑1) ·
(log‘2))))) + ((2 · ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) /
((log‘2)↑2))))) |
540 | 462, 53, 117, 512 | divassd 11529 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3))
· 1) / ((log‘2)↑4)) = ((4 · ((log‘𝐴)↑3)) · (1 /
((log‘2)↑4)))) |
541 | 528, 539,
540 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2
· ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) ≤ ((4
· ((log‘𝐴)↑3)) · (1 /
((log‘2)↑4)))) |
542 | 2, 495 | mulcomd 10740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) =
((((log‘𝐴)↑1)
· (log‘2)) · 𝐴)) |
543 | 156, 18, 2 | mulassd 10742 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → ((((log‘𝐴)↑1) ·
(log‘2)) · 𝐴)
= (((log‘𝐴)↑1)
· ((log‘2) · 𝐴))) |
544 | 542, 543 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 · (((log‘𝐴)↑1) · (log‘2))) =
(((log‘𝐴)↑1)
· ((log‘2) · 𝐴))) |
545 | 544 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2)))) = (𝐴 / (((log‘𝐴)↑1) ·
((log‘2) · 𝐴)))) |
546 | 545 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) =
(;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))))) |
547 | 2, 2, 155, 11, 88 | divdiv1d 11525 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (𝐴 ·
((log‘2)↑2)))) |
548 | 2, 155 | mulcomd 10740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → (𝐴 · ((log‘2)↑2)) =
(((log‘2)↑2) · 𝐴)) |
549 | 548 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑2))) = (𝐴 / (((log‘2)↑2)
· 𝐴))) |
550 | 547, 549 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑2)) = (𝐴 / (((log‘2)↑2)
· 𝐴))) |
551 | 550 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1))
· ((𝐴 / 𝐴) / ((log‘2)↑2))) =
((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2) · 𝐴)))) |
552 | 546, 551 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((;10 · (𝐴 / (𝐴 · (((log‘𝐴)↑1) · (log‘2))))) + ((2
· ((log‘𝐴)↑1)) · ((𝐴 / 𝐴) / ((log‘2)↑2)))) = ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴)))) + ((2 ·
((log‘𝐴)↑1))
· (𝐴 /
(((log‘2)↑2) · 𝐴))))) |
553 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (1 /
((log‘2)↑4)) = (1 / ((log‘2)↑4))) |
554 | 530 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (1 /
((log‘2)↑4)) = ((𝐴 / 𝐴) /
((log‘2)↑4))) |
555 | 553, 554 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (1 /
((log‘2)↑4)) = ((𝐴 / 𝐴) /
((log‘2)↑4))) |
556 | 555 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3))
· (1 / ((log‘2)↑4))) = ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) /
((log‘2)↑4)))) |
557 | 541, 552,
556 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴)))) + ((2 ·
((log‘𝐴)↑1))
· (𝐴 /
(((log‘2)↑2) · 𝐴)))) ≤ ((4 · ((log‘𝐴)↑3)) · ((𝐴 / 𝐴) /
((log‘2)↑4)))) |
558 | 156, 261 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((log‘𝐴)↑1) ·
((log‘2) · 𝐴))
∈ ℂ) |
559 | 156, 261,
247, 262 | mulne0d 11370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((log‘𝐴)↑1) ·
((log‘2) · 𝐴))
≠ 0) |
560 | 274, 558,
2, 559 | div32d 11517 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) · 𝐴) = (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))))) |
561 | 560 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴)))) = ((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) · 𝐴)) |
562 | 155, 2 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((log‘2)↑2)
· 𝐴) ∈
ℂ) |
563 | 155, 2, 88, 11 | mulne0d 11370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((log‘2)↑2)
· 𝐴) ≠
0) |
564 | 277, 562,
2, 563 | div32d 11517 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) · 𝐴) = ((2 · ((log‘𝐴)↑1)) · (𝐴 / (((log‘2)↑2)
· 𝐴)))) |
565 | 564 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1))
· (𝐴 /
(((log‘2)↑2) · 𝐴))) = (((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) · 𝐴)) |
566 | 561, 565 | oveq12d 7188 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((;10 · (𝐴 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴)))) + ((2 ·
((log‘𝐴)↑1))
· (𝐴 /
(((log‘2)↑2) · 𝐴)))) = (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) · 𝐴) + (((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) · 𝐴))) |
567 | 2, 2, 117, 11, 512 | divdiv1d 11525 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (𝐴 ·
((log‘2)↑4)))) |
568 | 2, 117 | mulcomd 10740 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐴 · ((log‘2)↑4)) =
(((log‘2)↑4) · 𝐴)) |
569 | 568 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐴 / (𝐴 · ((log‘2)↑4))) = (𝐴 / (((log‘2)↑4)
· 𝐴))) |
570 | 567, 569 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐴 / 𝐴) / ((log‘2)↑4)) = (𝐴 / (((log‘2)↑4)
· 𝐴))) |
571 | 570 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3))
· ((𝐴 / 𝐴) / ((log‘2)↑4))) =
((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4) · 𝐴)))) |
572 | 557, 566,
571 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) · 𝐴) + (((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) · 𝐴)) ≤ ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4)
· 𝐴)))) |
573 | 43, 1 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ((log‘2) ·
𝐴) ∈
ℝ) |
574 | 92, 573 | remulcld 10749 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (((log‘𝐴)↑1) ·
((log‘2) · 𝐴))
∈ ℝ) |
575 | 287, 574,
559 | redivcld 11546 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) ∈
ℝ) |
576 | 575 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) ∈
ℂ) |
577 | 157, 94 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) ∈ ℝ) |
578 | 577 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) ∈ ℂ) |
579 | 576, 578,
2 | adddird 10744 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) · 𝐴) = (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) · 𝐴) + (((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) · 𝐴))) |
580 | 579 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) · 𝐴) + (((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴)) · 𝐴)) = (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) · 𝐴)) |
581 | 12, 112 | expcld 13602 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((log‘𝐴)↑3) ∈
ℂ) |
582 | 416, 581 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (4 ·
((log‘𝐴)↑3))
∈ ℂ) |
583 | 117, 2 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((log‘2)↑4)
· 𝐴) ∈
ℂ) |
584 | 117, 2, 512, 11 | mulne0d 11370 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((log‘2)↑4)
· 𝐴) ≠
0) |
585 | 582, 583,
2, 584 | div32d 11517 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (((4 ·
((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴)) · 𝐴) = ((4 · ((log‘𝐴)↑3)) · (𝐴 / (((log‘2)↑4)
· 𝐴)))) |
586 | 585 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3))
· (𝐴 /
(((log‘2)↑4) · 𝐴))) = (((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴)) · 𝐴)) |
587 | 572, 580,
586 | 3brtr3d 5061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴)) · 𝐴)) |
588 | 575, 577 | readdcld 10748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ∈ ℝ) |
589 | 588, 122,
39 | lemul1d 12557 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴)) ↔ (((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) · 𝐴) ≤ (((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴)) · 𝐴))) |
590 | 587, 589 | mpbird 260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((;10 / (((log‘𝐴)↑1) · ((log‘2) ·
𝐴))) + ((2 ·
((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
591 | 271, 590 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((5 · 2) /
(((log‘𝐴)↑1)
· ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
592 | 267, 591 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((5 / ((log‘𝐴)↑1)) · ((2 ·
1) / ((log‘2) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
593 | 259, 592 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((5 · 1) /
((log‘𝐴)↑1))
· ((2 / (log‘2)) · (1 / 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
594 | 254, 593 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((5 · (1 /
((log‘𝐴)↑1)))
· ((2 / (log‘2)) · ((((log‘2)↑5) /
((log‘2)↑5)) / 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
595 | 246, 594 | eqbrtrd 5052 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑-1))
· ((2 / (log‘2)) · (((log‘2)↑5) /
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
596 | 238, 595 | eqbrtrd 5052 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((5 ·
(((log‘𝐴)↑4) /
((log‘𝐴)↑5)))
· ((2 · ((log‘2)↑5)) / ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
597 | 211, 596 | eqbrtrd 5052 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((5 ·
((log‘𝐴)↑4)) /
((log‘𝐴)↑5))
· ((2 · ((log‘2)↑5)) / (((log‘2) ·
((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
598 | 205, 597 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((5 ·
((log‘𝐴)↑4))
· (2 · ((log‘2)↑5))) / (((log‘𝐴)↑5) · (((log‘2) ·
((log‘2)↑5)) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
599 | 198, 598 | eqbrtrd 5052 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((2 ·
((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / (((log‘𝐴)↑5) · ((log‘2) ·
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
600 | 192, 599 | eqbrtrd 5052 |
. . . . . . . . . 10
⊢ (𝜑 → ((((2 ·
((log‘2)↑5)) · (5 · ((log‘𝐴)↑4))) / ((((log‘𝐴)↑5) ·
(log‘2)) · (((log‘2)↑5) · 𝐴))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
601 | 189, 600 | eqbrtrd 5052 |
. . . . . . . . 9
⊢ (𝜑 → ((((2 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) ≤ ((4
· ((log‘𝐴)↑3)) / (((log‘2)↑4)
· 𝐴))) |
602 | 184, 601 | eqbrtrd 5052 |
. . . . . . . 8
⊢ (𝜑 → (((((2 · 1)
· ((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) ≤ ((4
· ((log‘𝐴)↑3)) / (((log‘2)↑4)
· 𝐴))) |
603 | 179, 602 | eqbrtrd 5052 |
. . . . . . 7
⊢ (𝜑 → ((((2 · (1 ·
((log‘2)↑5))) / (((log‘𝐴)↑5) · (log‘2))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) ≤ ((4
· ((log‘𝐴)↑3)) / (((log‘2)↑4)
· 𝐴))) |
604 | 174, 603 | eqbrtrd 5052 |
. . . . . 6
⊢ (𝜑 → (((2 · ((1 ·
((log‘2)↑5)) / (((log‘𝐴)↑5) · (log‘2)))) ·
((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) + ((2
· ((log‘𝐴)↑1)) / (((log‘2)↑2)
· 𝐴))) ≤ ((4
· ((log‘𝐴)↑3)) / (((log‘2)↑4)
· 𝐴))) |
605 | 170, 604 | eqbrtrd 5052 |
. . . . 5
⊢ (𝜑 → ((2 · ((1 /
((((log‘𝐴)↑5)
· (log‘2)) / ((log‘2)↑5))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 · ((log‘𝐴)↑1)) /
(((log‘2)↑2) · 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
606 | 158, 605 | eqbrtrd 5052 |
. . . 4
⊢ (𝜑 → ((2 · ((1 /
((((log‘𝐴)↑5) /
((log‘2)↑5)) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
607 | 95, 111, 122, 149, 606 | letrd 10875 |
. . 3
⊢ (𝜑 → ((2 · ((1 /
(((((log‘𝐴)↑5) /
((log‘2)↑5)) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
608 | 35, 607 | eqbrtrd 5052 |
. 2
⊢ (𝜑 → ((2 · ((1 /
(((((log‘𝐴) /
(log‘2))↑5) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) ≤ ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
609 | 427, 39, 429 | syl2anc 587 |
. . . . . . . . . 10
⊢ (𝜑 → (2 logb 𝐴) = ((log‘𝐴) /
(log‘2))) |
610 | 609 | eqcomd 2744 |
. . . . . . . . 9
⊢ (𝜑 → ((log‘𝐴) / (log‘2)) = (2
logb 𝐴)) |
611 | 610 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑5) = ((2
logb 𝐴)↑5)) |
612 | 611 | oveq1d 7185 |
. . . . . . 7
⊢ (𝜑 → ((((log‘𝐴) / (log‘2))↑5) + 1)
= (((2 logb 𝐴)↑5) + 1)) |
613 | 612 | oveq1d 7185 |
. . . . . 6
⊢ (𝜑 → (((((log‘𝐴) / (log‘2))↑5) + 1)
· (log‘2)) = ((((2 logb 𝐴)↑5) + 1) ·
(log‘2))) |
614 | 613 | oveq2d 7186 |
. . . . 5
⊢ (𝜑 → (1 / (((((log‘𝐴) / (log‘2))↑5) + 1)
· (log‘2))) = (1 / ((((2 logb 𝐴)↑5) + 1) ·
(log‘2)))) |
615 | | 5cn 11804 |
. . . . . . . . . . . . . . 15
⊢ 5 ∈
ℂ |
616 | 615 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 5 ∈
ℂ) |
617 | 616, 207 | mulcld 10739 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (5 ·
((log‘𝐴)↑4))
∈ ℂ) |
618 | 617 | mulid1d 10736 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4))
· 1) = (5 · ((log‘𝐴)↑4))) |
619 | 618 | eqcomd 2744 |
. . . . . . . . . . 11
⊢ (𝜑 → (5 ·
((log‘𝐴)↑4)) =
((5 · ((log‘𝐴)↑4)) · 1)) |
620 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) =
(((log‘2)↑5) · 𝐴)) |
621 | | df-5 11782 |
. . . . . . . . . . . . . . . . . . 19
⊢ 5 = (4 +
1) |
622 | 621 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 5 = (4 +
1)) |
623 | 622 | oveq2d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((log‘2)↑5) =
((log‘2)↑(4 + 1))) |
624 | 18, 91, 77 | expaddd 13604 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((log‘2)↑(4 +
1)) = (((log‘2)↑4) ·
((log‘2)↑1))) |
625 | 623, 624 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((log‘2)↑5) =
(((log‘2)↑4) · ((log‘2)↑1))) |
626 | 476 | oveq2d 7186 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((log‘2)↑4)
· ((log‘2)↑1)) = (((log‘2)↑4) ·
(log‘2))) |
627 | 625, 626 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((log‘2)↑5) =
(((log‘2)↑4) · (log‘2))) |
628 | 627 | oveq1d 7185 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) =
((((log‘2)↑4) · (log‘2)) · 𝐴)) |
629 | 620, 628 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) =
((((log‘2)↑4) · (log‘2)) · 𝐴)) |
630 | 117, 18, 2 | mulassd 10742 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((log‘2)↑4)
· (log‘2)) · 𝐴) = (((log‘2)↑4) ·
((log‘2) · 𝐴))) |
631 | 629, 630 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) =
(((log‘2)↑4) · ((log‘2) · 𝐴))) |
632 | 18, 2 | mulcomd 10740 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((log‘2) ·
𝐴) = (𝐴 · (log‘2))) |
633 | 632 | oveq2d 7186 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((log‘2)↑4)
· ((log‘2) · 𝐴)) = (((log‘2)↑4) · (𝐴 ·
(log‘2)))) |
634 | 631, 633 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘2)↑5)
· 𝐴) =
(((log‘2)↑4) · (𝐴 · (log‘2)))) |
635 | 619, 634 | oveq12d 7188 |
. . . . . . . . . 10
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) · 1) /
(((log‘2)↑4) · (𝐴 · (log‘2))))) |
636 | 2, 18 | mulcld 10739 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 · (log‘2)) ∈
ℂ) |
637 | 2, 18, 11, 26 | mulne0d 11370 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 · (log‘2)) ≠
0) |
638 | 186, 117,
53, 636, 120, 637 | divmuldivd 11535 |
. . . . . . . . . . 11
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑4)) /
((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = (((5 ·
((log‘𝐴)↑4))
· 1) / (((log‘2)↑4) · (𝐴 · (log‘2))))) |
639 | 638 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑4))
· 1) / (((log‘2)↑4) · (𝐴 · (log‘2)))) = (((5 ·
((log‘𝐴)↑4)) /
((log‘2)↑4)) · (1 / (𝐴 · (log‘2))))) |
640 | 635, 639 | eqtrd 2773 |
. . . . . . . . 9
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) = (((5 · ((log‘𝐴)↑4)) /
((log‘2)↑4)) · (1 / (𝐴 · (log‘2))))) |
641 | 206, 207,
117, 120 | divassd 11529 |
. . . . . . . . . 10
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
((log‘2)↑4)) = (5 · (((log‘𝐴)↑4) /
((log‘2)↑4)))) |
642 | 641 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝜑 → (((5 ·
((log‘𝐴)↑4)) /
((log‘2)↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 ·
(((log‘𝐴)↑4) /
((log‘2)↑4))) · (1 / (𝐴 · (log‘2))))) |
643 | 640, 642 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴)↑4) /
((log‘2)↑4))) · (1 / (𝐴 · (log‘2))))) |
644 | 12, 18, 26, 77 | expdivd 13616 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) =
(((log‘𝐴)↑4) /
((log‘2)↑4))) |
645 | 644 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝜑 → (((log‘𝐴)↑4) /
((log‘2)↑4)) = (((log‘𝐴) / (log‘2))↑4)) |
646 | 645 | oveq2d 7186 |
. . . . . . . . 9
⊢ (𝜑 → (5 ·
(((log‘𝐴)↑4) /
((log‘2)↑4))) = (5 · (((log‘𝐴) /
(log‘2))↑4))) |
647 | 646 | oveq1d 7185 |
. . . . . . . 8
⊢ (𝜑 → ((5 ·
(((log‘𝐴)↑4) /
((log‘2)↑4))) · (1 / (𝐴 · (log‘2)))) = ((5 ·
(((log‘𝐴) /
(log‘2))↑4)) · (1 / (𝐴 · (log‘2))))) |
648 | 643, 647 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) = ((5 · (((log‘𝐴) / (log‘2))↑4))
· (1 / (𝐴 ·
(log‘2))))) |
649 | 610 | oveq1d 7185 |
. . . . . . . . 9
⊢ (𝜑 → (((log‘𝐴) / (log‘2))↑4) = ((2
logb 𝐴)↑4)) |
650 | 649 | oveq2d 7186 |
. . . . . . . 8
⊢ (𝜑 → (5 ·
(((log‘𝐴) /
(log‘2))↑4)) = (5 · ((2 logb 𝐴)↑4))) |
651 | 650 | oveq1d 7185 |
. . . . . . 7
⊢ (𝜑 → ((5 ·
(((log‘𝐴) /
(log‘2))↑4)) · (1 / (𝐴 · (log‘2)))) = ((5 ·
((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2))))) |
652 | 648, 651 | eqtrd 2773 |
. . . . . 6
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 ·
(log‘2))))) |
653 | 342, 77 | expcld 13602 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 logb 𝐴)↑4) ∈
ℂ) |
654 | 616, 653 | mulcld 10739 |
. . . . . . . . 9
⊢ (𝜑 → (5 · ((2
logb 𝐴)↑4))
∈ ℂ) |
655 | 39 | rpne0d 12519 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≠ 0) |
656 | 2, 18, 655, 26 | mulne0d 11370 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 · (log‘2)) ≠
0) |
657 | 636, 656 | reccld 11487 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (𝐴 · (log‘2))) ∈
ℂ) |
658 | 654, 657 | mulcld 10739 |
. . . . . . . 8
⊢ (𝜑 → ((5 · ((2
logb 𝐴)↑4))
· (1 / (𝐴 ·
(log‘2)))) ∈ ℂ) |
659 | 658 | addid1d 10918 |
. . . . . . 7
⊢ (𝜑 → (((5 · ((2
logb 𝐴)↑4))
· (1 / (𝐴 ·
(log‘2)))) + 0) = ((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2))))) |
660 | 659 | eqcomd 2744 |
. . . . . 6
⊢ (𝜑 → ((5 · ((2
logb 𝐴)↑4))
· (1 / (𝐴 ·
(log‘2)))) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) +
0)) |
661 | 652, 660 | eqtrd 2773 |
. . . . 5
⊢ (𝜑 → ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)) = (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) +
0)) |
662 | 614, 661 | oveq12d 7188 |
. . . 4
⊢ (𝜑 → ((1 / (((((log‘𝐴) / (log‘2))↑5) + 1)
· (log‘2))) · ((5 · ((log‘𝐴)↑4)) / (((log‘2)↑5)
· 𝐴))) = ((1 / ((((2
logb 𝐴)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) +
0))) |
663 | 662 | oveq2d 7186 |
. . 3
⊢ (𝜑 → (2 · ((1 /
(((((log‘𝐴) /
(log‘2))↑5) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) = (2 · ((1 / ((((2
logb 𝐴)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) +
0)))) |
664 | | 1e2m1 11843 |
. . . . . . 7
⊢ 1 = (2
− 1) |
665 | 664 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 1 = (2 −
1)) |
666 | 665 | oveq2d 7186 |
. . . . 5
⊢ (𝜑 → ((log‘𝐴)↑1) = ((log‘𝐴)↑(2 −
1))) |
667 | 666 | oveq1d 7185 |
. . . 4
⊢ (𝜑 → (((log‘𝐴)↑1) / 𝐴) = (((log‘𝐴)↑(2 − 1)) / 𝐴)) |
668 | 667 | oveq2d 7186 |
. . 3
⊢ (𝜑 → ((2 /
((log‘2)↑2)) · (((log‘𝐴)↑1) / 𝐴)) = ((2 / ((log‘2)↑2)) ·
(((log‘𝐴)↑(2
− 1)) / 𝐴))) |
669 | 663, 668 | oveq12d 7188 |
. 2
⊢ (𝜑 → ((2 · ((1 /
(((((log‘𝐴) /
(log‘2))↑5) + 1) · (log‘2))) · ((5 ·
((log‘𝐴)↑4)) /
(((log‘2)↑5) · 𝐴)))) + ((2 / ((log‘2)↑2))
· (((log‘𝐴)↑1) / 𝐴))) = ((2 · ((1 / ((((2
logb 𝐴)↑5)
+ 1) · (log‘2))) · (((5 · ((2 logb 𝐴)↑4)) · (1 / (𝐴 · (log‘2)))) +
0))) + ((2 / ((log‘2)↑2)) · (((log‘𝐴)↑(2 − 1)) / 𝐴)))) |
670 | | 4cn 11801 |
. . . . 5
⊢ 4 ∈
ℂ |
671 | 670 | a1i 11 |
. . . 4
⊢ (𝜑 → 4 ∈
ℂ) |
672 | 671, 117,
581, 2, 120, 655 | divmuldivd 11535 |
. . 3
⊢ (𝜑 → ((4 /
((log‘2)↑4)) · (((log‘𝐴)↑3) / 𝐴)) = ((4 · ((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴))) |
673 | 672 | eqcomd 2744 |
. 2
⊢ (𝜑 → ((4 ·
((log‘𝐴)↑3)) /
(((log‘2)↑4) · 𝐴)) = ((4 / ((log‘2)↑4)) ·
(((log‘𝐴)↑3) /
𝐴))) |
674 | 608, 669,
673 | 3brtr3d 5061 |
1
⊢ (𝜑 → ((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) / 𝐴))) |