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