Step |
Hyp |
Ref |
Expression |
1 |
|
log2ublem2.1 |
⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 𝐾 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 𝐵 ) |
2 |
|
log2ublem2.2 |
⊢ 𝐵 ∈ ℕ0 |
3 |
|
log2ublem2.3 |
⊢ 𝐹 ∈ ℕ0 |
4 |
|
log2ublem2.4 |
⊢ 𝑁 ∈ ℕ0 |
5 |
|
log2ublem2.5 |
⊢ ( 𝑁 − 1 ) = 𝐾 |
6 |
|
log2ublem2.6 |
⊢ ( 𝐵 + 𝐹 ) = 𝐺 |
7 |
|
log2ublem2.7 |
⊢ 𝑀 ∈ ℕ0 |
8 |
|
log2ublem2.8 |
⊢ ( 𝑀 + 𝑁 ) = 3 |
9 |
|
log2ublem2.9 |
⊢ ( ( 5 · 7 ) · ( 9 ↑ 𝑀 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) |
10 |
|
fzfid |
⊢ ( ⊤ → ( 0 ... 𝐾 ) ∈ Fin ) |
11 |
|
elfznn0 |
⊢ ( 𝑛 ∈ ( 0 ... 𝐾 ) → 𝑛 ∈ ℕ0 ) |
12 |
11
|
adantl |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 𝐾 ) ) → 𝑛 ∈ ℕ0 ) |
13 |
|
2re |
⊢ 2 ∈ ℝ |
14 |
|
3nn |
⊢ 3 ∈ ℕ |
15 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
16 |
|
nn0mulcl |
⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 ) |
17 |
15 16
|
mpan |
⊢ ( 𝑛 ∈ ℕ0 → ( 2 · 𝑛 ) ∈ ℕ0 ) |
18 |
|
nn0p1nn |
⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) |
19 |
17 18
|
syl |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) |
20 |
|
nnmulcl |
⊢ ( ( 3 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ ) |
21 |
14 19 20
|
sylancr |
⊢ ( 𝑛 ∈ ℕ0 → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ ) |
22 |
|
9nn |
⊢ 9 ∈ ℕ |
23 |
|
nnexpcl |
⊢ ( ( 9 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℕ ) |
24 |
22 23
|
mpan |
⊢ ( 𝑛 ∈ ℕ0 → ( 9 ↑ 𝑛 ) ∈ ℕ ) |
25 |
21 24
|
nnmulcld |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ ) |
26 |
|
nndivre |
⊢ ( ( 2 ∈ ℝ ∧ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ ) |
27 |
13 25 26
|
sylancr |
⊢ ( 𝑛 ∈ ℕ0 → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ ) |
28 |
12 27
|
syl |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 𝐾 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ ) |
29 |
10 28
|
fsumrecl |
⊢ ( ⊤ → Σ 𝑛 ∈ ( 0 ... 𝐾 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ ) |
30 |
29
|
mptru |
⊢ Σ 𝑛 ∈ ( 0 ... 𝐾 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ |
31 |
15 4
|
nn0mulcli |
⊢ ( 2 · 𝑁 ) ∈ ℕ0 |
32 |
|
nn0p1nn |
⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ ) |
33 |
31 32
|
ax-mp |
⊢ ( ( 2 · 𝑁 ) + 1 ) ∈ ℕ |
34 |
14 33
|
nnmulcli |
⊢ ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ∈ ℕ |
35 |
|
nnexpcl |
⊢ ( ( 9 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 9 ↑ 𝑁 ) ∈ ℕ ) |
36 |
22 4 35
|
mp2an |
⊢ ( 9 ↑ 𝑁 ) ∈ ℕ |
37 |
34 36
|
nnmulcli |
⊢ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ∈ ℕ |
38 |
15 2
|
nn0mulcli |
⊢ ( 2 · 𝐵 ) ∈ ℕ0 |
39 |
15 3
|
nn0mulcli |
⊢ ( 2 · 𝐹 ) ∈ ℕ0 |
40 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
41 |
4 40
|
eleqtri |
⊢ 𝑁 ∈ ( ℤ≥ ‘ 0 ) |
42 |
41
|
a1i |
⊢ ( ⊤ → 𝑁 ∈ ( ℤ≥ ‘ 0 ) ) |
43 |
|
elfznn0 |
⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑛 ∈ ℕ0 ) |
44 |
43
|
adantl |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → 𝑛 ∈ ℕ0 ) |
45 |
27
|
recnd |
⊢ ( 𝑛 ∈ ℕ0 → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ ) |
46 |
44 45
|
syl |
⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℂ ) |
47 |
|
oveq2 |
⊢ ( 𝑛 = 𝑁 → ( 2 · 𝑛 ) = ( 2 · 𝑁 ) ) |
48 |
47
|
oveq1d |
⊢ ( 𝑛 = 𝑁 → ( ( 2 · 𝑛 ) + 1 ) = ( ( 2 · 𝑁 ) + 1 ) ) |
49 |
48
|
oveq2d |
⊢ ( 𝑛 = 𝑁 → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) = ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) ) |
50 |
|
oveq2 |
⊢ ( 𝑛 = 𝑁 → ( 9 ↑ 𝑛 ) = ( 9 ↑ 𝑁 ) ) |
51 |
49 50
|
oveq12d |
⊢ ( 𝑛 = 𝑁 → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) = ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) |
52 |
51
|
oveq2d |
⊢ ( 𝑛 = 𝑁 → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) |
53 |
42 46 52
|
fsumm1 |
⊢ ( ⊤ → Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) ) |
54 |
53
|
mptru |
⊢ Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) |
55 |
5
|
oveq2i |
⊢ ( 0 ... ( 𝑁 − 1 ) ) = ( 0 ... 𝐾 ) |
56 |
55
|
sumeq1i |
⊢ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 0 ... 𝐾 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) |
57 |
56
|
oveq1i |
⊢ ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) = ( Σ 𝑛 ∈ ( 0 ... 𝐾 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) |
58 |
54 57
|
eqtri |
⊢ Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 0 ... 𝐾 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 2 / ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ) ) |
59 |
|
2cn |
⊢ 2 ∈ ℂ |
60 |
2
|
nn0cni |
⊢ 𝐵 ∈ ℂ |
61 |
3
|
nn0cni |
⊢ 𝐹 ∈ ℂ |
62 |
59 60 61
|
adddii |
⊢ ( 2 · ( 𝐵 + 𝐹 ) ) = ( ( 2 · 𝐵 ) + ( 2 · 𝐹 ) ) |
63 |
6
|
oveq2i |
⊢ ( 2 · ( 𝐵 + 𝐹 ) ) = ( 2 · 𝐺 ) |
64 |
62 63
|
eqtr3i |
⊢ ( ( 2 · 𝐵 ) + ( 2 · 𝐹 ) ) = ( 2 · 𝐺 ) |
65 |
|
7nn |
⊢ 7 ∈ ℕ |
66 |
65
|
nnnn0i |
⊢ 7 ∈ ℕ0 |
67 |
|
nnexpcl |
⊢ ( ( 3 ∈ ℕ ∧ 7 ∈ ℕ0 ) → ( 3 ↑ 7 ) ∈ ℕ ) |
68 |
14 66 67
|
mp2an |
⊢ ( 3 ↑ 7 ) ∈ ℕ |
69 |
|
5nn |
⊢ 5 ∈ ℕ |
70 |
69 65
|
nnmulcli |
⊢ ( 5 · 7 ) ∈ ℕ |
71 |
68 70
|
nnmulcli |
⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℕ |
72 |
71
|
nnrei |
⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℝ |
73 |
72 13
|
remulcli |
⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 2 ) ∈ ℝ |
74 |
73
|
leidi |
⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 2 ) ≤ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 2 ) |
75 |
14
|
nnnn0i |
⊢ 3 ∈ ℕ0 |
76 |
|
nnexpcl |
⊢ ( ( 9 ∈ ℕ ∧ 3 ∈ ℕ0 ) → ( 9 ↑ 3 ) ∈ ℕ ) |
77 |
22 75 76
|
mp2an |
⊢ ( 9 ↑ 3 ) ∈ ℕ |
78 |
77
|
nncni |
⊢ ( 9 ↑ 3 ) ∈ ℂ |
79 |
70
|
nncni |
⊢ ( 5 · 7 ) ∈ ℂ |
80 |
78 79
|
mulcomi |
⊢ ( ( 9 ↑ 3 ) · ( 5 · 7 ) ) = ( ( 5 · 7 ) · ( 9 ↑ 3 ) ) |
81 |
7
|
nn0cni |
⊢ 𝑀 ∈ ℂ |
82 |
4
|
nn0cni |
⊢ 𝑁 ∈ ℂ |
83 |
81 82
|
addcomi |
⊢ ( 𝑀 + 𝑁 ) = ( 𝑁 + 𝑀 ) |
84 |
8 83
|
eqtr3i |
⊢ 3 = ( 𝑁 + 𝑀 ) |
85 |
84
|
oveq2i |
⊢ ( 9 ↑ 3 ) = ( 9 ↑ ( 𝑁 + 𝑀 ) ) |
86 |
22
|
nncni |
⊢ 9 ∈ ℂ |
87 |
|
expadd |
⊢ ( ( 9 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 9 ↑ ( 𝑁 + 𝑀 ) ) = ( ( 9 ↑ 𝑁 ) · ( 9 ↑ 𝑀 ) ) ) |
88 |
86 4 7 87
|
mp3an |
⊢ ( 9 ↑ ( 𝑁 + 𝑀 ) ) = ( ( 9 ↑ 𝑁 ) · ( 9 ↑ 𝑀 ) ) |
89 |
85 88
|
eqtri |
⊢ ( 9 ↑ 3 ) = ( ( 9 ↑ 𝑁 ) · ( 9 ↑ 𝑀 ) ) |
90 |
89
|
oveq2i |
⊢ ( ( 5 · 7 ) · ( 9 ↑ 3 ) ) = ( ( 5 · 7 ) · ( ( 9 ↑ 𝑁 ) · ( 9 ↑ 𝑀 ) ) ) |
91 |
36
|
nncni |
⊢ ( 9 ↑ 𝑁 ) ∈ ℂ |
92 |
|
nnexpcl |
⊢ ( ( 9 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ) → ( 9 ↑ 𝑀 ) ∈ ℕ ) |
93 |
22 7 92
|
mp2an |
⊢ ( 9 ↑ 𝑀 ) ∈ ℕ |
94 |
93
|
nncni |
⊢ ( 9 ↑ 𝑀 ) ∈ ℂ |
95 |
79 91 94
|
mul12i |
⊢ ( ( 5 · 7 ) · ( ( 9 ↑ 𝑁 ) · ( 9 ↑ 𝑀 ) ) ) = ( ( 9 ↑ 𝑁 ) · ( ( 5 · 7 ) · ( 9 ↑ 𝑀 ) ) ) |
96 |
80 90 95
|
3eqtri |
⊢ ( ( 9 ↑ 3 ) · ( 5 · 7 ) ) = ( ( 9 ↑ 𝑁 ) · ( ( 5 · 7 ) · ( 9 ↑ 𝑀 ) ) ) |
97 |
9
|
oveq2i |
⊢ ( ( 9 ↑ 𝑁 ) · ( ( 5 · 7 ) · ( 9 ↑ 𝑀 ) ) ) = ( ( 9 ↑ 𝑁 ) · ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ) |
98 |
96 97
|
eqtri |
⊢ ( ( 9 ↑ 3 ) · ( 5 · 7 ) ) = ( ( 9 ↑ 𝑁 ) · ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ) |
99 |
98
|
oveq2i |
⊢ ( 3 · ( ( 9 ↑ 3 ) · ( 5 · 7 ) ) ) = ( 3 · ( ( 9 ↑ 𝑁 ) · ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ) ) |
100 |
|
df-7 |
⊢ 7 = ( 6 + 1 ) |
101 |
100
|
oveq2i |
⊢ ( 3 ↑ 7 ) = ( 3 ↑ ( 6 + 1 ) ) |
102 |
|
3cn |
⊢ 3 ∈ ℂ |
103 |
|
6nn0 |
⊢ 6 ∈ ℕ0 |
104 |
|
expp1 |
⊢ ( ( 3 ∈ ℂ ∧ 6 ∈ ℕ0 ) → ( 3 ↑ ( 6 + 1 ) ) = ( ( 3 ↑ 6 ) · 3 ) ) |
105 |
102 103 104
|
mp2an |
⊢ ( 3 ↑ ( 6 + 1 ) ) = ( ( 3 ↑ 6 ) · 3 ) |
106 |
|
expmul |
⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) → ( 3 ↑ ( 2 · 3 ) ) = ( ( 3 ↑ 2 ) ↑ 3 ) ) |
107 |
102 15 75 106
|
mp3an |
⊢ ( 3 ↑ ( 2 · 3 ) ) = ( ( 3 ↑ 2 ) ↑ 3 ) |
108 |
59 102
|
mulcomi |
⊢ ( 2 · 3 ) = ( 3 · 2 ) |
109 |
|
3t2e6 |
⊢ ( 3 · 2 ) = 6 |
110 |
108 109
|
eqtri |
⊢ ( 2 · 3 ) = 6 |
111 |
110
|
oveq2i |
⊢ ( 3 ↑ ( 2 · 3 ) ) = ( 3 ↑ 6 ) |
112 |
|
sq3 |
⊢ ( 3 ↑ 2 ) = 9 |
113 |
112
|
oveq1i |
⊢ ( ( 3 ↑ 2 ) ↑ 3 ) = ( 9 ↑ 3 ) |
114 |
107 111 113
|
3eqtr3i |
⊢ ( 3 ↑ 6 ) = ( 9 ↑ 3 ) |
115 |
114
|
oveq1i |
⊢ ( ( 3 ↑ 6 ) · 3 ) = ( ( 9 ↑ 3 ) · 3 ) |
116 |
105 115
|
eqtri |
⊢ ( 3 ↑ ( 6 + 1 ) ) = ( ( 9 ↑ 3 ) · 3 ) |
117 |
78 102
|
mulcomi |
⊢ ( ( 9 ↑ 3 ) · 3 ) = ( 3 · ( 9 ↑ 3 ) ) |
118 |
101 116 117
|
3eqtri |
⊢ ( 3 ↑ 7 ) = ( 3 · ( 9 ↑ 3 ) ) |
119 |
118
|
oveq1i |
⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) = ( ( 3 · ( 9 ↑ 3 ) ) · ( 5 · 7 ) ) |
120 |
102 78 79
|
mulassi |
⊢ ( ( 3 · ( 9 ↑ 3 ) ) · ( 5 · 7 ) ) = ( 3 · ( ( 9 ↑ 3 ) · ( 5 · 7 ) ) ) |
121 |
119 120
|
eqtri |
⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) = ( 3 · ( ( 9 ↑ 3 ) · ( 5 · 7 ) ) ) |
122 |
33
|
nncni |
⊢ ( ( 2 · 𝑁 ) + 1 ) ∈ ℂ |
123 |
102 122 91
|
mul32i |
⊢ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) = ( ( 3 · ( 9 ↑ 𝑁 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) |
124 |
123
|
oveq1i |
⊢ ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · 𝐹 ) = ( ( ( 3 · ( 9 ↑ 𝑁 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) · 𝐹 ) |
125 |
102 91
|
mulcli |
⊢ ( 3 · ( 9 ↑ 𝑁 ) ) ∈ ℂ |
126 |
125 122 61
|
mulassi |
⊢ ( ( ( 3 · ( 9 ↑ 𝑁 ) ) · ( ( 2 · 𝑁 ) + 1 ) ) · 𝐹 ) = ( ( 3 · ( 9 ↑ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ) |
127 |
122 61
|
mulcli |
⊢ ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ∈ ℂ |
128 |
102 91 127
|
mulassi |
⊢ ( ( 3 · ( 9 ↑ 𝑁 ) ) · ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ) = ( 3 · ( ( 9 ↑ 𝑁 ) · ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ) ) |
129 |
124 126 128
|
3eqtri |
⊢ ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · 𝐹 ) = ( 3 · ( ( 9 ↑ 𝑁 ) · ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 ) ) ) |
130 |
99 121 129
|
3eqtr4i |
⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) = ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · 𝐹 ) |
131 |
130
|
oveq2i |
⊢ ( 2 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) = ( 2 · ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · 𝐹 ) ) |
132 |
68
|
nncni |
⊢ ( 3 ↑ 7 ) ∈ ℂ |
133 |
132 79
|
mulcli |
⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℂ |
134 |
133 59
|
mulcomi |
⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 2 ) = ( 2 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) |
135 |
37
|
nncni |
⊢ ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) ∈ ℂ |
136 |
135 59 61
|
mul12i |
⊢ ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · ( 2 · 𝐹 ) ) = ( 2 · ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · 𝐹 ) ) |
137 |
131 134 136
|
3eqtr4i |
⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 2 ) = ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · ( 2 · 𝐹 ) ) |
138 |
74 137
|
breqtri |
⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 2 ) ≤ ( ( ( 3 · ( ( 2 · 𝑁 ) + 1 ) ) · ( 9 ↑ 𝑁 ) ) · ( 2 · 𝐹 ) ) |
139 |
1 30 15 37 38 39 58 64 138
|
log2ublem1 |
⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 𝐺 ) |