Metamath Proof Explorer

Theorem log2ub

Description: log 2 is less than 2 5 3 / 3 6 5 . If written in decimal, this is because log 2 = 0.693147... is less than 253/365 = 0.693151... , so this is a very tight bound, at five decimal places. (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 16-Sep-2021)

Ref Expression
Assertion log2ub ( log ‘ 2 ) < ( 2 5 3 / 3 6 5 )

Proof

Step Hyp Ref Expression
1 4m1e3 ⊢ ( 4 − 1 ) = 3
2 1 oveq2i ⊢ ( 0 ... ( 4 − 1 ) ) = ( 0 ... 3 )
3 2 sumeq1i ⊢ Σ 𝑛 ∈ ( 0 ... ( 4 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) )
4 3 oveq2i ⊢ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 4 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) = ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) )
5 4nn0 ⊢ 4 ∈ ℕ0
6 log2tlbnd ⊢ ( 4 ∈ ℕ0 → ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 4 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) )
7 5 6 ax-mp ⊢ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... ( 4 − 1 ) ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) )
8 4 7 eqeltrri ⊢ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) )
9 0re ⊢ 0 ∈ ℝ
10 3re ⊢ 3 ∈ ℝ
11 4nn ⊢ 4 ∈ ℕ
12 2nn0 ⊢ 2 ∈ ℕ0
13 1nn ⊢ 1 ∈ ℕ
14 12 5 13 numnncl ⊢ ( ( 2 · 4 ) + 1 ) ∈ ℕ
15 11 14 nnmulcli ⊢ ( 4 · ( ( 2 · 4 ) + 1 ) ) ∈ ℕ
16 9nn ⊢ 9 ∈ ℕ
17 nnexpcl ⊢ ( ( 9 ∈ ℕ ∧ 4 ∈ ℕ0 ) → ( 9 ↑ 4 ) ∈ ℕ )
18 16 5 17 mp2an ⊢ ( 9 ↑ 4 ) ∈ ℕ
19 15 18 nnmulcli ⊢ ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ∈ ℕ
20 nndivre ⊢ ( ( 3 ∈ ℝ ∧ ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ∈ ℕ ) → ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ∈ ℝ )
21 10 19 20 mp2an ⊢ ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ∈ ℝ
22 9 21 elicc2i ⊢ ( ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ( 0 [,] ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ↔ ( ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∧ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) )
23 8 22 mpbi ⊢ ( ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ∧ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) )
24 23 simp3i ⊢ ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) )
25 2rp ⊢ 2 ∈ ℝ+
26 relogcl ⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
27 25 26 ax-mp ⊢ ( log ‘ 2 ) ∈ ℝ
28 fzfid ⊢ ( ⊤ → ( 0 ... 3 ) ∈ Fin )
29 2re ⊢ 2 ∈ ℝ
30 3nn ⊢ 3 ∈ ℕ
31 elfznn0 ⊢ ( 𝑛 ∈ ( 0 ... 3 ) → 𝑛 ∈ ℕ0 )
32 31 adantl ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 3 ) ) → 𝑛 ∈ ℕ0 )
33 nn0mulcl ⊢ ( ( 2 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ) → ( 2 · 𝑛 ) ∈ ℕ0 )
34 12 32 33 sylancr ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 3 ) ) → ( 2 · 𝑛 ) ∈ ℕ0 )
35 nn0p1nn ⊢ ( ( 2 · 𝑛 ) ∈ ℕ0 → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
36 34 35 syl ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 3 ) ) → ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ )
37 nnmulcl ⊢ ( ( 3 ∈ ℕ ∧ ( ( 2 · 𝑛 ) + 1 ) ∈ ℕ ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
38 30 36 37 sylancr ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 3 ) ) → ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) ∈ ℕ )
39 nnexpcl ⊢ ( ( 9 ∈ ℕ ∧ 𝑛 ∈ ℕ0 ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
40 16 32 39 sylancr ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 3 ) ) → ( 9 ↑ 𝑛 ) ∈ ℕ )
41 38 40 nnmulcld ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 3 ) ) → ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ )
42 nndivre ⊢ ( ( 2 ∈ ℝ ∧ ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ∈ ℕ ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
43 29 41 42 sylancr ⊢ ( ( ⊤ ∧ 𝑛 ∈ ( 0 ... 3 ) ) → ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
44 28 43 fsumrecl ⊢ ( ⊤ → Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ )
45 44 mptru ⊢ Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ∈ ℝ
46 27 45 21 lesubadd2i ⊢ ( ( ( log ‘ 2 ) − Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ↔ ( log ‘ 2 ) ≤ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) )
47 24 46 mpbi ⊢ ( log ‘ 2 ) ≤ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) )
48 log2ublem3 ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) ) ≤ 5 3 0 5 6
49 3nn0 ⊢ 3 ∈ ℕ0
50 5nn0 ⊢ 5 ∈ ℕ0
51 50 49 deccl ⊢ 5 3 ∈ ℕ0
52 0nn0 ⊢ 0 ∈ ℕ0
53 51 52 deccl ⊢ 5 3 0 ∈ ℕ0
54 53 50 deccl ⊢ 5 3 0 5 ∈ ℕ0
55 6nn0 ⊢ 6 ∈ ℕ0
56 54 55 deccl ⊢ 5 3 0 5 6 ∈ ℕ0
57 1nn0 ⊢ 1 ∈ ℕ0
58 eqid ⊢ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) = ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) )
59 6p1e7 ⊢ ( 6 + 1 ) = 7
60 eqid ⊢ 5 3 0 5 6 = 5 3 0 5 6
61 54 55 59 60 decsuc ⊢ ( 5 3 0 5 6 + 1 ) = 5 3 0 5 7
62 5nn ⊢ 5 ∈ ℕ
63 7nn ⊢ 7 ∈ ℕ
64 62 63 nnmulcli ⊢ ( 5 · 7 ) ∈ ℕ
65 64 nnrei ⊢ ( 5 · 7 ) ∈ ℝ
66 15 nnrei ⊢ ( 4 · ( ( 2 · 4 ) + 1 ) ) ∈ ℝ
67 6nn ⊢ 6 ∈ ℕ
68 5lt6 ⊢ 5 < 6
69 49 50 67 68 declt ⊢ 3 5 < 3 6
70 7cn ⊢ 7 ∈ ℂ
71 5cn ⊢ 5 ∈ ℂ
72 7t5e35 ⊢ ( 7 · 5 ) = 3 5
73 70 71 72 mulcomli ⊢ ( 5 · 7 ) = 3 5
74 4cn ⊢ 4 ∈ ℂ
75 2cn ⊢ 2 ∈ ℂ
76 4t2e8 ⊢ ( 4 · 2 ) = 8
77 74 75 76 mulcomli ⊢ ( 2 · 4 ) = 8
78 77 oveq1i ⊢ ( ( 2 · 4 ) + 1 ) = ( 8 + 1 )
79 8p1e9 ⊢ ( 8 + 1 ) = 9
80 78 79 eqtri ⊢ ( ( 2 · 4 ) + 1 ) = 9
81 80 oveq2i ⊢ ( 4 · ( ( 2 · 4 ) + 1 ) ) = ( 4 · 9 )
82 9cn ⊢ 9 ∈ ℂ
83 9t4e36 ⊢ ( 9 · 4 ) = 3 6
84 82 74 83 mulcomli ⊢ ( 4 · 9 ) = 3 6
85 81 84 eqtri ⊢ ( 4 · ( ( 2 · 4 ) + 1 ) ) = 3 6
86 69 73 85 3brtr4i ⊢ ( 5 · 7 ) < ( 4 · ( ( 2 · 4 ) + 1 ) )
87 65 66 86 ltleii ⊢ ( 5 · 7 ) ≤ ( 4 · ( ( 2 · 4 ) + 1 ) )
88 18 nngt0i ⊢ 0 < ( 9 ↑ 4 )
89 18 nnrei ⊢ ( 9 ↑ 4 ) ∈ ℝ
90 65 66 89 lemul2i ⊢ ( 0 < ( 9 ↑ 4 ) → ( ( 5 · 7 ) ≤ ( 4 · ( ( 2 · 4 ) + 1 ) ) ↔ ( ( 9 ↑ 4 ) · ( 5 · 7 ) ) ≤ ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) ) ) )
91 88 90 ax-mp ⊢ ( ( 5 · 7 ) ≤ ( 4 · ( ( 2 · 4 ) + 1 ) ) ↔ ( ( 9 ↑ 4 ) · ( 5 · 7 ) ) ≤ ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) ) )
92 87 91 mpbi ⊢ ( ( 9 ↑ 4 ) · ( 5 · 7 ) ) ≤ ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) )
93 7nn0 ⊢ 7 ∈ ℕ0
94 nnexpcl ⊢ ( ( 3 ∈ ℕ ∧ 7 ∈ ℕ0 ) → ( 3 ↑ 7 ) ∈ ℕ )
95 30 93 94 mp2an ⊢ ( 3 ↑ 7 ) ∈ ℕ
96 95 nncni ⊢ ( 3 ↑ 7 ) ∈ ℂ
97 64 nncni ⊢ ( 5 · 7 ) ∈ ℂ
98 3cn ⊢ 3 ∈ ℂ
99 96 97 98 mul32i ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 3 ) = ( ( ( 3 ↑ 7 ) · 3 ) · ( 5 · 7 ) )
100 74 75 mulcomi ⊢ ( 4 · 2 ) = ( 2 · 4 )
101 df-8 ⊢ 8 = ( 7 + 1 )
102 76 100 101 3eqtr3i ⊢ ( 2 · 4 ) = ( 7 + 1 )
103 102 oveq2i ⊢ ( 3 ↑ ( 2 · 4 ) ) = ( 3 ↑ ( 7 + 1 ) )
104 expmul ⊢ ( ( 3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) → ( 3 ↑ ( 2 · 4 ) ) = ( ( 3 ↑ 2 ) ↑ 4 ) )
105 98 12 5 104 mp3an ⊢ ( 3 ↑ ( 2 · 4 ) ) = ( ( 3 ↑ 2 ) ↑ 4 )
106 103 105 eqtr3i ⊢ ( 3 ↑ ( 7 + 1 ) ) = ( ( 3 ↑ 2 ) ↑ 4 )
107 expp1 ⊢ ( ( 3 ∈ ℂ ∧ 7 ∈ ℕ0 ) → ( 3 ↑ ( 7 + 1 ) ) = ( ( 3 ↑ 7 ) · 3 ) )
108 98 93 107 mp2an ⊢ ( 3 ↑ ( 7 + 1 ) ) = ( ( 3 ↑ 7 ) · 3 )
109 sq3 ⊢ ( 3 ↑ 2 ) = 9
110 109 oveq1i ⊢ ( ( 3 ↑ 2 ) ↑ 4 ) = ( 9 ↑ 4 )
111 106 108 110 3eqtr3i ⊢ ( ( 3 ↑ 7 ) · 3 ) = ( 9 ↑ 4 )
112 111 oveq1i ⊢ ( ( ( 3 ↑ 7 ) · 3 ) · ( 5 · 7 ) ) = ( ( 9 ↑ 4 ) · ( 5 · 7 ) )
113 99 112 eqtri ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 3 ) = ( ( 9 ↑ 4 ) · ( 5 · 7 ) )
114 15 nncni ⊢ ( 4 · ( ( 2 · 4 ) + 1 ) ) ∈ ℂ
115 18 nncni ⊢ ( 9 ↑ 4 ) ∈ ℂ
116 114 115 mulcomi ⊢ ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) = ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) )
117 116 oveq1i ⊢ ( ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) · 1 ) = ( ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) ) · 1 )
118 115 114 mulcli ⊢ ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) ) ∈ ℂ
119 118 mulid1i ⊢ ( ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) ) · 1 ) = ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) )
120 117 119 eqtri ⊢ ( ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) · 1 ) = ( ( 9 ↑ 4 ) · ( 4 · ( ( 2 · 4 ) + 1 ) ) )
121 92 113 120 3brtr4i ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · 3 ) ≤ ( ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) · 1 )
122 48 45 49 19 56 57 58 61 121 log2ublem1 ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ) ≤ 5 3 0 5 7
123 45 21 readdcli ⊢ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ∈ ℝ
124 54 93 deccl ⊢ 5 3 0 5 7 ∈ ℕ0
125 124 nn0rei ⊢ 5 3 0 5 7 ∈ ℝ
126 95 64 nnmulcli ⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℕ
127 126 nnrei ⊢ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℝ
128 126 nngt0i ⊢ 0 < ( ( 3 ↑ 7 ) · ( 5 · 7 ) )
129 127 128 pm3.2i ⊢ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℝ ∧ 0 < ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) )
130 lemuldiv2 ⊢ ( ( ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ∈ ℝ ∧ 5 3 0 5 7 ∈ ℝ ∧ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℝ ∧ 0 < ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ) → ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ) ≤ 5 3 0 5 7 ↔ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ≤ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ) )
131 123 125 129 130 mp3an ⊢ ( ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) · ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ) ≤ 5 3 0 5 7 ↔ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ≤ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) )
132 122 131 mpbi ⊢ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ≤ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) )
133 8nn0 ⊢ 8 ∈ ℕ0
134 49 133 deccl ⊢ 3 8 ∈ ℕ0
135 134 93 deccl ⊢ 3 8 7 ∈ ℕ0
136 135 49 deccl ⊢ 3 8 7 3 ∈ ℕ0
137 136 57 deccl ⊢ 3 8 7 3 1 ∈ ℕ0
138 137 55 deccl ⊢ 3 8 7 3 1 6 ∈ ℕ0
139 137 93 deccl ⊢ 3 8 7 3 1 7 ∈ ℕ0
140 1lt10 ⊢ 1 < 1 0
141 6lt7 ⊢ 6 < 7
142 137 55 63 141 declt ⊢ 3 8 7 3 1 6 < 3 8 7 3 1 7
143 138 139 57 93 140 142 decltc ⊢ 3 8 7 3 1 6 1 < 3 8 7 3 1 7 7
144 eqid ⊢ 7 3 = 7 3
145 57 50 deccl ⊢ 1 5 ∈ ℕ0
146 9nn0 ⊢ 9 ∈ ℕ0
147 145 146 deccl ⊢ 1 5 9 ∈ ℕ0
148 147 57 deccl ⊢ 1 5 9 1 ∈ ℕ0
149 148 93 deccl ⊢ 1 5 9 1 7 ∈ ℕ0
150 eqid ⊢ 5 3 0 5 7 = 5 3 0 5 7
151 eqid ⊢ 1 5 9 1 7 = 1 5 9 1 7
152 eqid ⊢ 5 3 0 5 = 5 3 0 5
153 eqid ⊢ 1 5 9 1 = 1 5 9 1
154 ax-1cn ⊢ 1 ∈ ℂ
155 5p1e6 ⊢ ( 5 + 1 ) = 6
156 71 154 155 addcomli ⊢ ( 1 + 5 ) = 6
157 147 57 50 153 156 decaddi ⊢ ( 1 5 9 1 + 5 ) = 1 5 9 6
158 57 55 deccl ⊢ 1 6 ∈ ℕ0
159 eqid ⊢ 5 3 0 = 5 3 0
160 eqid ⊢ 1 5 9 = 1 5 9
161 eqid ⊢ 1 5 = 1 5
162 57 50 155 161 decsuc ⊢ ( 1 5 + 1 ) = 1 6
163 9p4e13 ⊢ ( 9 + 4 ) = 1 3
164 145 146 5 160 162 49 163 decaddci ⊢ ( 1 5 9 + 4 ) = 1 6 3
165 eqid ⊢ 5 3 = 5 3
166 158 nn0cni ⊢ 1 6 ∈ ℂ
167 166 addid1i ⊢ ( 1 6 + 0 ) = 1 6
168 1p2e3 ⊢ ( 1 + 2 ) = 3
169 168 oveq2i ⊢ ( ( 5 · 7 ) + ( 1 + 2 ) ) = ( ( 5 · 7 ) + 3 )
170 5p3e8 ⊢ ( 5 + 3 ) = 8
171 49 50 49 73 170 decaddi ⊢ ( ( 5 · 7 ) + 3 ) = 3 8
172 169 171 eqtri ⊢ ( ( 5 · 7 ) + ( 1 + 2 ) ) = 3 8
173 7t3e21 ⊢ ( 7 · 3 ) = 2 1
174 70 98 173 mulcomli ⊢ ( 3 · 7 ) = 2 1
175 6cn ⊢ 6 ∈ ℂ
176 175 154 59 addcomli ⊢ ( 1 + 6 ) = 7
177 12 57 55 174 176 decaddi ⊢ ( ( 3 · 7 ) + 6 ) = 2 7
178 50 49 57 55 165 167 93 93 12 172 177 decmac ⊢ ( ( 5 3 · 7 ) + ( 1 6 + 0 ) ) = 3 8 7
179 70 mul02i ⊢ ( 0 · 7 ) = 0
180 179 oveq1i ⊢ ( ( 0 · 7 ) + 3 ) = ( 0 + 3 )
181 98 addid2i ⊢ ( 0 + 3 ) = 3
182 49 dec0h ⊢ 3 = 0 3
183 181 182 eqtri ⊢ ( 0 + 3 ) = 0 3
184 180 183 eqtri ⊢ ( ( 0 · 7 ) + 3 ) = 0 3
185 51 52 158 49 159 164 93 49 52 178 184 decmac ⊢ ( ( 5 3 0 · 7 ) + ( 1 5 9 + 4 ) ) = 3 8 7 3
186 3p1e4 ⊢ ( 3 + 1 ) = 4
187 6p5e11 ⊢ ( 6 + 5 ) = 1 1
188 175 71 187 addcomli ⊢ ( 5 + 6 ) = 1 1
189 49 50 55 73 186 57 188 decaddci ⊢ ( ( 5 · 7 ) + 6 ) = 4 1
190 53 50 147 55 152 157 93 57 5 185 189 decmac ⊢ ( ( 5 3 0 5 · 7 ) + ( 1 5 9 1 + 5 ) ) = 3 8 7 3 1
191 7t7e49 ⊢ ( 7 · 7 ) = 4 9
192 4p1e5 ⊢ ( 4 + 1 ) = 5
193 9p7e16 ⊢ ( 9 + 7 ) = 1 6
194 5 146 93 191 192 55 193 decaddci ⊢ ( ( 7 · 7 ) + 7 ) = 5 6
195 54 93 148 93 150 151 93 55 50 190 194 decmac ⊢ ( ( 5 3 0 5 7 · 7 ) + 1 5 9 1 7 ) = 3 8 7 3 1 6
196 12 dec0h ⊢ 2 = 0 2
197 154 addid2i ⊢ ( 0 + 1 ) = 1
198 57 dec0h ⊢ 1 = 0 1
199 197 198 eqtri ⊢ ( 0 + 1 ) = 0 1
200 00id ⊢ ( 0 + 0 ) = 0
201 52 dec0h ⊢ 0 = 0 0
202 200 201 eqtri ⊢ ( 0 + 0 ) = 0 0
203 5t3e15 ⊢ ( 5 · 3 ) = 1 5
204 203 oveq1i ⊢ ( ( 5 · 3 ) + 0 ) = ( 1 5 + 0 )
205 145 nn0cni ⊢ 1 5 ∈ ℂ
206 205 addid1i ⊢ ( 1 5 + 0 ) = 1 5
207 204 206 eqtri ⊢ ( ( 5 · 3 ) + 0 ) = 1 5
208 3t3e9 ⊢ ( 3 · 3 ) = 9
209 208 oveq1i ⊢ ( ( 3 · 3 ) + 0 ) = ( 9 + 0 )
210 82 addid1i ⊢ ( 9 + 0 ) = 9
211 209 210 eqtri ⊢ ( ( 3 · 3 ) + 0 ) = 9
212 50 49 52 52 165 202 49 207 211 decma ⊢ ( ( 5 3 · 3 ) + ( 0 + 0 ) ) = 1 5 9
213 98 mul02i ⊢ ( 0 · 3 ) = 0
214 213 oveq1i ⊢ ( ( 0 · 3 ) + 1 ) = ( 0 + 1 )
215 214 199 eqtri ⊢ ( ( 0 · 3 ) + 1 ) = 0 1
216 51 52 52 57 159 199 49 57 52 212 215 decmac ⊢ ( ( 5 3 0 · 3 ) + ( 0 + 1 ) ) = 1 5 9 1
217 5p2e7 ⊢ ( 5 + 2 ) = 7
218 57 50 12 203 217 decaddi ⊢ ( ( 5 · 3 ) + 2 ) = 1 7
219 53 50 52 12 152 196 49 93 57 216 218 decmac ⊢ ( ( 5 3 0 5 · 3 ) + 2 ) = 1 5 9 1 7
220 49 54 93 150 57 12 219 173 decmul1c ⊢ ( 5 3 0 5 7 · 3 ) = 1 5 9 1 7 1
221 124 93 49 144 57 149 195 220 decmul2c ⊢ ( 5 3 0 5 7 · 7 3 ) = 3 8 7 3 1 6 1
222 50 50 deccl ⊢ 5 5 ∈ ℕ0
223 222 49 deccl ⊢ 5 5 3 ∈ ℕ0
224 223 49 deccl ⊢ 5 5 3 3 ∈ ℕ0
225 224 57 deccl ⊢ 5 5 3 3 1 ∈ ℕ0
226 12 50 deccl ⊢ 2 5 ∈ ℕ0
227 226 49 deccl ⊢ 2 5 3 ∈ ℕ0
228 12 57 deccl ⊢ 2 1 ∈ ℕ0
229 228 133 deccl ⊢ 2 1 8 ∈ ℕ0
230 93 12 deccl ⊢ 7 2 ∈ ℕ0
231 3t2e6 ⊢ ( 3 · 2 ) = 6
232 98 75 231 mulcomli ⊢ ( 2 · 3 ) = 6
233 3exp3 ⊢ ( 3 ↑ 3 ) = 2 7
234 12 93 deccl ⊢ 2 7 ∈ ℕ0
235 eqid ⊢ 2 7 = 2 7
236 57 133 deccl ⊢ 1 8 ∈ ℕ0
237 eqid ⊢ 1 8 = 1 8
238 2t2e4 ⊢ ( 2 · 2 ) = 4
239 238 168 oveq12i ⊢ ( ( 2 · 2 ) + ( 1 + 2 ) ) = ( 4 + 3 )
240 4p3e7 ⊢ ( 4 + 3 ) = 7
241 239 240 eqtri ⊢ ( ( 2 · 2 ) + ( 1 + 2 ) ) = 7
242 7t2e14 ⊢ ( 7 · 2 ) = 1 4
243 1p1e2 ⊢ ( 1 + 1 ) = 2
244 8cn ⊢ 8 ∈ ℂ
245 8p4e12 ⊢ ( 8 + 4 ) = 1 2
246 244 74 245 addcomli ⊢ ( 4 + 8 ) = 1 2
247 57 5 133 242 243 12 246 decaddci ⊢ ( ( 7 · 2 ) + 8 ) = 2 2
248 12 93 57 133 235 237 12 12 12 241 247 decmac ⊢ ( ( 2 7 · 2 ) + 1 8 ) = 7 2
249 70 75 242 mulcomli ⊢ ( 2 · 7 ) = 1 4
250 4p4e8 ⊢ ( 4 + 4 ) = 8
251 57 5 5 249 250 decaddi ⊢ ( ( 2 · 7 ) + 4 ) = 1 8
252 93 12 93 235 146 5 251 191 decmul1c ⊢ ( 2 7 · 7 ) = 1 8 9
253 234 12 93 235 146 236 248 252 decmul2c ⊢ ( 2 7 · 2 7 ) = 7 2 9
254 49 49 232 233 253 numexp2x ⊢ ( 3 ↑ 6 ) = 7 2 9
255 eqid ⊢ 7 2 = 7 2
256 232 oveq1i ⊢ ( ( 2 · 3 ) + 2 ) = ( 6 + 2 )
257 6p2e8 ⊢ ( 6 + 2 ) = 8
258 256 257 eqtri ⊢ ( ( 2 · 3 ) + 2 ) = 8
259 93 12 12 255 49 173 258 decrmanc ⊢ ( ( 7 2 · 3 ) + 2 ) = 2 1 8
260 9t3e27 ⊢ ( 9 · 3 ) = 2 7
261 49 230 146 254 93 12 259 260 decmul1c ⊢ ( ( 3 ↑ 6 ) · 3 ) = 2 1 8 7
262 49 55 59 261 numexpp1 ⊢ ( 3 ↑ 7 ) = 2 1 8 7
263 57 93 deccl ⊢ 1 7 ∈ ℕ0
264 263 93 deccl ⊢ 1 7 7 ∈ ℕ0
265 eqid ⊢ 2 1 8 = 2 1 8
266 eqid ⊢ 1 7 7 = 1 7 7
267 12 52 deccl ⊢ 2 0 ∈ ℕ0
268 267 49 deccl ⊢ 2 0 3 ∈ ℕ0
269 12 12 deccl ⊢ 2 2 ∈ ℕ0
270 eqid ⊢ 2 1 = 2 1
271 eqid ⊢ 1 7 = 1 7
272 eqid ⊢ 2 0 3 = 2 0 3
273 eqid ⊢ 2 0 = 2 0
274 75 addid2i ⊢ ( 0 + 2 ) = 2
275 154 addid1i ⊢ ( 1 + 0 ) = 1
276 52 57 12 52 198 273 274 275 decadd ⊢ ( 1 + 2 0 ) = 2 1
277 12 57 243 276 decsuc ⊢ ( ( 1 + 2 0 ) + 1 ) = 2 2
278 7p3e10 ⊢ ( 7 + 3 ) = 1 0
279 57 93 267 49 271 272 277 278 decaddc2 ⊢ ( 1 7 + 2 0 3 ) = 2 2 0
280 eqid ⊢ 2 5 3 = 2 5 3
281 eqid ⊢ 2 2 = 2 2
282 eqid ⊢ 2 5 = 2 5
283 2p2e4 ⊢ ( 2 + 2 ) = 4
284 71 75 217 addcomli ⊢ ( 2 + 5 ) = 7
285 12 12 12 50 281 282 283 284 decadd ⊢ ( 2 2 + 2 5 ) = 4 7
286 50 dec0h ⊢ 5 = 0 5
287 192 286 eqtri ⊢ ( 4 + 1 ) = 0 5
288 238 197 oveq12i ⊢ ( ( 2 · 2 ) + ( 0 + 1 ) ) = ( 4 + 1 )
289 288 192 eqtri ⊢ ( ( 2 · 2 ) + ( 0 + 1 ) ) = 5
290 5t2e10 ⊢ ( 5 · 2 ) = 1 0
291 71 addid2i ⊢ ( 0 + 5 ) = 5
292 57 52 50 290 291 decaddi ⊢ ( ( 5 · 2 ) + 5 ) = 1 5
293 12 50 52 50 282 287 12 50 57 289 292 decmac ⊢ ( ( 2 5 · 2 ) + ( 4 + 1 ) ) = 5 5
294 231 oveq1i ⊢ ( ( 3 · 2 ) + 7 ) = ( 6 + 7 )
295 7p6e13 ⊢ ( 7 + 6 ) = 1 3
296 70 175 295 addcomli ⊢ ( 6 + 7 ) = 1 3
297 294 296 eqtri ⊢ ( ( 3 · 2 ) + 7 ) = 1 3
298 226 49 5 93 280 285 12 49 57 293 297 decmac ⊢ ( ( 2 5 3 · 2 ) + ( 2 2 + 2 5 ) ) = 5 5 3
299 227 nn0cni ⊢ 2 5 3 ∈ ℂ
300 299 mulid1i ⊢ ( 2 5 3 · 1 ) = 2 5 3
301 300 oveq1i ⊢ ( ( 2 5 3 · 1 ) + 0 ) = ( 2 5 3 + 0 )
302 299 addid1i ⊢ ( 2 5 3 + 0 ) = 2 5 3
303 301 302 eqtri ⊢ ( ( 2 5 3 · 1 ) + 0 ) = 2 5 3
304 12 57 269 52 270 279 227 49 226 298 303 decma2c ⊢ ( ( 2 5 3 · 2 1 ) + ( 1 7 + 2 0 3 ) ) = 5 5 3 3
305 93 dec0h ⊢ 7 = 0 7
306 74 addid2i ⊢ ( 0 + 4 ) = 4
307 306 oveq2i ⊢ ( ( 2 · 8 ) + ( 0 + 4 ) ) = ( ( 2 · 8 ) + 4 )
308 8t2e16 ⊢ ( 8 · 2 ) = 1 6
309 244 75 308 mulcomli ⊢ ( 2 · 8 ) = 1 6
310 6p4e10 ⊢ ( 6 + 4 ) = 1 0
311 57 55 5 309 243 310 decaddci2 ⊢ ( ( 2 · 8 ) + 4 ) = 2 0
312 307 311 eqtri ⊢ ( ( 2 · 8 ) + ( 0 + 4 ) ) = 2 0
313 8t5e40 ⊢ ( 8 · 5 ) = 4 0
314 244 71 313 mulcomli ⊢ ( 5 · 8 ) = 4 0
315 5 52 49 314 181 decaddi ⊢ ( ( 5 · 8 ) + 3 ) = 4 3
316 12 50 52 49 282 183 133 49 5 312 315 decmac ⊢ ( ( 2 5 · 8 ) + ( 0 + 3 ) ) = 2 0 3
317 8t3e24 ⊢ ( 8 · 3 ) = 2 4
318 244 98 317 mulcomli ⊢ ( 3 · 8 ) = 2 4
319 2p1e3 ⊢ ( 2 + 1 ) = 3
320 7p4e11 ⊢ ( 7 + 4 ) = 1 1
321 70 74 320 addcomli ⊢ ( 4 + 7 ) = 1 1
322 12 5 93 318 319 57 321 decaddci ⊢ ( ( 3 · 8 ) + 7 ) = 3 1
323 226 49 52 93 280 305 133 57 49 316 322 decmac ⊢ ( ( 2 5 3 · 8 ) + 7 ) = 2 0 3 1
324 228 133 263 93 265 266 227 57 268 304 323 decma2c ⊢ ( ( 2 5 3 · 2 1 8 ) + 1 7 7 ) = 5 5 3 3 1
325 57 5 49 249 240 decaddi ⊢ ( ( 2 · 7 ) + 3 ) = 1 7
326 49 50 12 73 217 decaddi ⊢ ( ( 5 · 7 ) + 2 ) = 3 7
327 12 50 12 282 93 93 49 325 326 decrmac ⊢ ( ( 2 5 · 7 ) + 2 ) = 1 7 7
328 93 226 49 280 57 12 327 174 decmul1c ⊢ ( 2 5 3 · 7 ) = 1 7 7 1
329 227 229 93 262 57 264 324 328 decmul2c ⊢ ( 2 5 3 · ( 3 ↑ 7 ) ) = 5 5 3 3 1 1
330 eqid ⊢ 5 5 3 3 1 = 5 5 3 3 1
331 eqid ⊢ 5 5 3 3 = 5 5 3 3
332 eqid ⊢ 5 5 3 = 5 5 3
333 eqid ⊢ 5 5 = 5 5
334 274 196 eqtri ⊢ ( 0 + 2 ) = 0 2
335 181 oveq2i ⊢ ( ( 5 · 7 ) + ( 0 + 3 ) ) = ( ( 5 · 7 ) + 3 )
336 335 171 eqtri ⊢ ( ( 5 · 7 ) + ( 0 + 3 ) ) = 3 8
337 50 50 52 12 333 334 93 93 49 336 326 decmac ⊢ ( ( 5 5 · 7 ) + ( 0 + 2 ) ) = 3 8 7
338 12 57 12 174 168 decaddi ⊢ ( ( 3 · 7 ) + 2 ) = 2 3
339 222 49 52 12 332 196 93 49 12 337 338 decmac ⊢ ( ( 5 5 3 · 7 ) + 2 ) = 3 8 7 3
340 93 223 49 331 57 12 339 174 decmul1c ⊢ ( 5 5 3 3 · 7 ) = 3 8 7 3 1
341 70 mulid2i ⊢ ( 1 · 7 ) = 7
342 93 224 57 330 340 341 decmul1 ⊢ ( 5 5 3 3 1 · 7 ) = 3 8 7 3 1 7
343 93 225 57 329 342 341 decmul1 ⊢ ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) = 3 8 7 3 1 7 7
344 143 221 343 3brtr4i ⊢ ( 5 3 0 5 7 · 7 3 ) < ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 )
345 93 49 deccl ⊢ 7 3 ∈ ℕ0
346 124 345 nn0mulcli ⊢ ( 5 3 0 5 7 · 7 3 ) ∈ ℕ0
347 346 nn0rei ⊢ ( 5 3 0 5 7 · 7 3 ) ∈ ℝ
348 49 93 nn0expcli ⊢ ( 3 ↑ 7 ) ∈ ℕ0
349 227 348 nn0mulcli ⊢ ( 2 5 3 · ( 3 ↑ 7 ) ) ∈ ℕ0
350 349 93 nn0mulcli ⊢ ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) ∈ ℕ0
351 350 nn0rei ⊢ ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) ∈ ℝ
352 62 nnrei ⊢ 5 ∈ ℝ
353 62 nngt0i ⊢ 0 < 5
354 347 351 352 353 ltmul1ii ⊢ ( ( 5 3 0 5 7 · 7 3 ) < ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) ↔ ( ( 5 3 0 5 7 · 7 3 ) · 5 ) < ( ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) · 5 ) )
355 344 354 mpbi ⊢ ( ( 5 3 0 5 7 · 7 3 ) · 5 ) < ( ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) · 5 )
356 124 nn0cni ⊢ 5 3 0 5 7 ∈ ℂ
357 345 nn0cni ⊢ 7 3 ∈ ℂ
358 356 357 71 mulassi ⊢ ( ( 5 3 0 5 7 · 7 3 ) · 5 ) = ( 5 3 0 5 7 · ( 7 3 · 5 ) )
359 49 50 155 72 decsuc ⊢ ( ( 7 · 5 ) + 1 ) = 3 6
360 71 98 203 mulcomli ⊢ ( 3 · 5 ) = 1 5
361 50 93 49 144 50 57 359 360 decmul1c ⊢ ( 7 3 · 5 ) = 3 6 5
362 361 oveq2i ⊢ ( 5 3 0 5 7 · ( 7 3 · 5 ) ) = ( 5 3 0 5 7 · 3 6 5 )
363 358 362 eqtri ⊢ ( ( 5 3 0 5 7 · 7 3 ) · 5 ) = ( 5 3 0 5 7 · 3 6 5 )
364 299 96 mulcli ⊢ ( 2 5 3 · ( 3 ↑ 7 ) ) ∈ ℂ
365 364 70 71 mulassi ⊢ ( ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) · 5 ) = ( ( 2 5 3 · ( 3 ↑ 7 ) ) · ( 7 · 5 ) )
366 70 71 mulcomi ⊢ ( 7 · 5 ) = ( 5 · 7 )
367 366 oveq2i ⊢ ( ( 2 5 3 · ( 3 ↑ 7 ) ) · ( 7 · 5 ) ) = ( ( 2 5 3 · ( 3 ↑ 7 ) ) · ( 5 · 7 ) )
368 299 96 97 mulassi ⊢ ( ( 2 5 3 · ( 3 ↑ 7 ) ) · ( 5 · 7 ) ) = ( 2 5 3 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) )
369 367 368 eqtri ⊢ ( ( 2 5 3 · ( 3 ↑ 7 ) ) · ( 7 · 5 ) ) = ( 2 5 3 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) )
370 365 369 eqtri ⊢ ( ( ( 2 5 3 · ( 3 ↑ 7 ) ) · 7 ) · 5 ) = ( 2 5 3 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) )
371 355 363 370 3brtr3i ⊢ ( 5 3 0 5 7 · 3 6 5 ) < ( 2 5 3 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) )
372 49 55 deccl ⊢ 3 6 ∈ ℕ0
373 372 62 decnncl ⊢ 3 6 5 ∈ ℕ
374 373 nnrei ⊢ 3 6 5 ∈ ℝ
375 373 nngt0i ⊢ 0 < 3 6 5
376 374 375 pm3.2i ⊢ ( 3 6 5 ∈ ℝ ∧ 0 < 3 6 5 )
377 227 nn0rei ⊢ 2 5 3 ∈ ℝ
378 lt2mul2div ⊢ ( ( ( 5 3 0 5 7 ∈ ℝ ∧ ( 3 6 5 ∈ ℝ ∧ 0 < 3 6 5 ) ) ∧ ( 2 5 3 ∈ ℝ ∧ ( ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℝ ∧ 0 < ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ) ) → ( ( 5 3 0 5 7 · 3 6 5 ) < ( 2 5 3 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ↔ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) < ( 2 5 3 / 3 6 5 ) ) )
379 125 376 377 129 378 mp4an ⊢ ( ( 5 3 0 5 7 · 3 6 5 ) < ( 2 5 3 · ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ↔ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) < ( 2 5 3 / 3 6 5 ) )
380 371 379 mpbi ⊢ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) < ( 2 5 3 / 3 6 5 )
381 nndivre ⊢ ( ( 5 3 0 5 7 ∈ ℝ ∧ ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ∈ ℕ ) → ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ∈ ℝ )
382 125 126 381 mp2an ⊢ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ∈ ℝ
383 nndivre ⊢ ( ( 2 5 3 ∈ ℝ ∧ 3 6 5 ∈ ℕ ) → ( 2 5 3 / 3 6 5 ) ∈ ℝ )
384 377 373 383 mp2an ⊢ ( 2 5 3 / 3 6 5 ) ∈ ℝ
385 123 382 384 lelttri ⊢ ( ( ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ≤ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) ∧ ( 5 3 0 5 7 / ( ( 3 ↑ 7 ) · ( 5 · 7 ) ) ) < ( 2 5 3 / 3 6 5 ) ) → ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) < ( 2 5 3 / 3 6 5 ) )
386 132 380 385 mp2an ⊢ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) < ( 2 5 3 / 3 6 5 )
387 27 123 384 lelttri ⊢ ( ( ( log ‘ 2 ) ≤ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) ∧ ( Σ 𝑛 ∈ ( 0 ... 3 ) ( 2 / ( ( 3 · ( ( 2 · 𝑛 ) + 1 ) ) · ( 9 ↑ 𝑛 ) ) ) + ( 3 / ( ( 4 · ( ( 2 · 4 ) + 1 ) ) · ( 9 ↑ 4 ) ) ) ) < ( 2 5 3 / 3 6 5 ) ) → ( log ‘ 2 ) < ( 2 5 3 / 3 6 5 ) )
388 47 386 387 mp2an ⊢ ( log ‘ 2 ) < ( 2 5 3 / 3 6 5 )