Metamath Proof Explorer


Theorem log2ublem2

Description: Lemma for log2ub . (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Hypotheses log2ublem2.1 ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 𝐾 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 𝐵 )
log2ublem2.2 𝐵 ∈ ℕ0
log2ublem2.3 𝐹 ∈ ℕ0
log2ublem2.4 𝑁 ∈ ℕ0
log2ublem2.5 ( 𝑁 − 1 ) = 𝐾
log2ublem2.6 ( 𝐵 + 𝐹 ) = 𝐺
log2ublem2.7 𝑀 ∈ ℕ0
log2ublem2.8 ( 𝑀 + 𝑁 ) = 3
log2ublem2.9 ( ( 5 · 7 ) · ( 9 ↑ 𝑀 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · 𝐹 )
Assertion log2ublem2 ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 𝑁 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 2 · 𝐺 )

Proof

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 · 𝐺 )