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