\$( THEOREM=log2ub LOC_AFTER=? * ` 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, 1-Apr-2015.) 1::df-4 |- 4 = ( 3 + 1 ) 2:1:oveq1i |- ( 4 - 1 ) = ( ( 3 + 1 ) - 1 ) 3::3cn |- 3 e. CC 4::ax-1cn |- 1 e. CC 5::pncan |- ( ( 3 e. CC /\ 1 e. CC ) -> ( ( 3 + 1 ) - 1 ) = 3 ) 6:3,4,5:mp2an |- ( ( 3 + 1 ) - 1 ) = 3 7:2,6:eqtri |- ( 4 - 1 ) = 3 8:7:oveq2i |- ( 0 ... ( 4 - 1 ) ) = ( 0 ... 3 ) 9:8: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 ) ) ) 10:9: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 ) ) ) ) 11::4nn0 |- 4 e. NN0 12::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 ) ) ) ) ) 13:11,12: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 ) ) ) ) 14:10,13: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 ) ) ) ) 15::0re |- 0 e. RR 16::3re |- 3 e. RR 17::4nn |- 4 e. NN 18::2nn0 |- 2 e. NN0 19::1nn |- 1 e. NN 20:18,11,19:numnncl |- ( ( 2 x. 4 ) + 1 ) e. NN 21:17,20:nnmulcli |- ( 4 x. ( ( 2 x. 4 ) + 1 ) ) e. NN 22::9nn |- 9 e. NN 23::nnexpcl |- ( ( 9 e. NN /\ 4 e. NN0 ) -> ( 9 ^ 4 ) e. NN ) 24:22,11,23:mp2an |- ( 9 ^ 4 ) e. NN 25:21,24:nnmulcli |- ( ( 4 x. ( ( 2 x. 4 ) + 1 ) ) x. ( 9 ^ 4 ) ) e. NN 26::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 ) 27:16,25,26:mp2an |- ( 3 / ( ( 4 x. ( ( 2 x. 4 ) + 1 ) ) x. ( 9 ^ 4 ) ) ) e. RR 28:15,27: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 ) ) ) ) ) 29:14,28: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 ) ) ) ) 30:29: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 ) ) ) 31::2re |- 2 e. RR 32::2pos |- 0 < 2 33:31,32:elrpii |- 2 e. RR+ 34::relogcl |- ( 2 e. RR+ -> ( log ` 2 ) e. RR ) 35:33,34:ax-mp |- ( log ` 2 ) e. RR 36::fzfid |- ( T. -> ( 0 ... 3 ) e. Fin ) 37::3nn |- 3 e. NN 38::elfznn0 |- ( n e. ( 0 ... 3 ) -> n e. NN0 ) 39:38:adantl |- ( ( T. /\ n e. ( 0 ... 3 ) ) -> n e. NN0 ) 40::nn0mulcl |- ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 ) 41:18,39,40:sylancr |- ( ( T. /\ n e. ( 0 ... 3 ) ) -> ( 2 x. n ) e. NN0 ) 42::nn0p1nn |- ( ( 2 x. n ) e. NN0 -> ( ( 2 x. n ) + 1 ) e. NN ) 43:41,42:syl |- ( ( T. /\ n e. ( 0 ... 3 ) ) -> ( ( 2 x. n ) + 1 ) e. NN ) 44::nnmulcl |- ( ( 3 e. NN /\ ( ( 2 x. n ) + 1 ) e. NN ) -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN ) 45:37,43,44:sylancr |- ( ( T. /\ n e. ( 0 ... 3 ) ) -> ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN ) 46::nnexpcl |- ( ( 9 e. NN /\ n e. NN0 ) -> ( 9 ^ n ) e. NN ) 47:22,39,46:sylancr |- ( ( T. /\ n e. ( 0 ... 3 ) ) -> ( 9 ^ n ) e. NN ) 48::nnmulcl |- ( ( ( 3 x. ( ( 2 x. n ) + 1 ) ) e. NN /\ ( 9 ^ n ) e. NN ) -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. NN ) 49:45,47,48:syl2anc |- ( ( T. /\ n e. ( 0 ... 3 ) ) -> ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) e. NN ) 50::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 ) 51:31,49,50:sylancr |- ( ( T. /\ n e. ( 0 ... 3 ) ) -> ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR ) 52:36,51:fsumrecl |- ( T. -> sum_ n e. ( 0 ... 3 ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR ) 53:52:trud |- sum_ n e. ( 0 ... 3 ) ( 2 / ( ( 3 x. ( ( 2 x. n ) + 1 ) ) x. ( 9 ^ n ) ) ) e. RR 54:35,53,27: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 ) ) ) ) ) 55:30,54: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 ) ) ) ) 56::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 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:: |- ( 5 x. 7 ) < ( 4 x. ( ( 2 x. 4 ) + 1 ) ) 60::5nn |- 5 e. NN 61::7nn |- 7 e. NN 62:60,61:nnmulcli |- ( 5 x. 7 ) e. NN 63:62:nnrei |- ( 5 x. 7 ) e. RR 64:21:nnrei |- ( 4 x. ( ( 2 x. 4 ) + 1 ) ) e. RR 66:63,64,59:ltleii |- ( 5 x. 7 ) <_ ( 4 x. ( ( 2 x. 4 ) + 1 ) ) 67:24:nngt0i |- 0 < ( 9 ^ 4 ) 68:24:nnrei |- ( 9 ^ 4 ) e. RR 69:63,64,68: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 ) ) ) ) ) 70:67,69: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 ) ) ) ) 71:66,70:mpbi |- ( ( 9 ^ 4 ) x. ( 5 x. 7 ) ) <_ ( ( 9 ^ 4 ) x. ( 4 x. ( ( 2 x. 4 ) + 1 ) ) ) 72::7nn |- 7 e. NN 74:61:nnnn0i |- 7 e. NN0 75::nnexpcl |- ( ( 3 e. NN /\ 7 e. NN0 ) -> ( 3 ^ 7 ) e. NN ) 76:37,74,75:mp2an |- ( 3 ^ 7 ) e. NN 77:76:nncni |- ( 3 ^ 7 ) e. CC 78:62:nncni |- ( 5 x. 7 ) e. CC 79:77,78,3:mul32i |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 3 ) = ( ( ( 3 ^ 7 ) x. 3 ) x. ( 5 x. 7 ) ) 80:17:nncni |- 4 e. CC 81:31:recni |- 2 e. CC 82:80,81:mulcomi |- ( 4 x. 2 ) = ( 2 x. 4 ) 83::df-8 |- 8 = ( 7 + 1 ) 84::4t2e8 |- ( 4 x. 2 ) = 8 85:84,82,83:3eqtr3i |- ( 2 x. 4 ) = ( 7 + 1 ) 86:85:oveq2i |- ( 3 ^ ( 2 x. 4 ) ) = ( 3 ^ ( 7 + 1 ) ) 87::expmul |- ( ( 3 e. CC /\ 2 e. NN0 /\ 4 e. NN0 ) -> ( 3 ^ ( 2 x. 4 ) ) = ( ( 3 ^ 2 ) ^ 4 ) ) 88:3,18,11,87:mp3an |- ( 3 ^ ( 2 x. 4 ) ) = ( ( 3 ^ 2 ) ^ 4 ) 89:86,88:eqtr3i |- ( 3 ^ ( 7 + 1 ) ) = ( ( 3 ^ 2 ) ^ 4 ) 90::expp1 |- ( ( 3 e. CC /\ 7 e. NN0 ) -> ( 3 ^ ( 7 + 1 ) ) = ( ( 3 ^ 7 ) x. 3 ) ) 91:3,74,90:mp2an |- ( 3 ^ ( 7 + 1 ) ) = ( ( 3 ^ 7 ) x. 3 ) 92::sq3 |- ( 3 ^ 2 ) = 9 93:92:oveq1i |- ( ( 3 ^ 2 ) ^ 4 ) = ( 9 ^ 4 ) 94:89,91,93:3eqtr3i |- ( ( 3 ^ 7 ) x. 3 ) = ( 9 ^ 4 ) 95:94:oveq1i |- ( ( ( 3 ^ 7 ) x. 3 ) x. ( 5 x. 7 ) ) = ( ( 9 ^ 4 ) x. ( 5 x. 7 ) ) 96:79,95:eqtri |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 3 ) = ( ( 9 ^ 4 ) x. ( 5 x. 7 ) ) 97:21:nncni |- ( 4 x. ( ( 2 x. 4 ) + 1 ) ) e. CC 98:24:nncni |- ( 9 ^ 4 ) e. CC 99:97,98:mulcomi |- ( ( 4 x. ( ( 2 x. 4 ) + 1 ) ) x. ( 9 ^ 4 ) ) = ( ( 9 ^ 4 ) x. ( 4 x. ( ( 2 x. 4 ) + 1 ) ) ) 100:99:oveq1i |- ( ( ( 4 x. ( ( 2 x. 4 ) + 1 ) ) x. ( 9 ^ 4 ) ) x. 1 ) = ( ( ( 9 ^ 4 ) x. ( 4 x. ( ( 2 x. 4 ) + 1 ) ) ) x. 1 ) 101:98,97:mulcli |- ( ( 9 ^ 4 ) x. ( 4 x. ( ( 2 x. 4 ) + 1 ) ) ) e. CC 102:101:mulid1i |- ( ( ( 9 ^ 4 ) x. ( 4 x. ( ( 2 x. 4 ) + 1 ) ) ) x. 1 ) = ( ( 9 ^ 4 ) x. ( 4 x. ( ( 2 x. 4 ) + 1 ) ) ) 103:100,102:eqtri |- ( ( ( 4 x. ( ( 2 x. 4 ) + 1 ) ) x. ( 9 ^ 4 ) ) x. 1 ) = ( ( 9 ^ 4 ) x. ( 4 x. ( ( 2 x. 4 ) + 1 ) ) ) 104:71,96,103:3brtr4i |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) x. 3 ) <_ ( ( ( 4 x. ( ( 2 x. 4 ) + 1 ) ) x. ( 9 ^ 4 ) ) x. 1 ) 105:37:nnnn0i |- 3 e. NN0 106:: |- ; ; ; ; 5 3 0 5 6 e. NN0 107:: |- ( ; ; ; ; 5 3 0 5 6 + 1 ) = ; ; ; ; 5 3 0 5 7 108:56,53,105,25,106,57,58,107,104: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 109:53,27: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 110:76,62:nnmulcli |- ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. NN 111:110:nnrei |- ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. RR 112:110:nngt0i |- 0 < ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) 113:111,112:pm3.2i |- ( ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) e. RR /\ 0 < ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) ) 114::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 ) ) ) ) ) 115:: |- ; ; ; ; 5 3 0 5 7 e. NN0 116:115:nn0rei |- ; ; ; ; 5 3 0 5 7 e. RR 117:109,116,113,114: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 ) ) ) ) 118:108,117: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 ) ) ) 119::5re |- 5 e. RR 120:: |- ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) e. NN0 121:120:nn0rei |- ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) e. RR 122:: |- ( ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) x. 7 ) e. NN0 123:122:nn0rei |- ( ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) x. 7 ) e. RR 124:121,123,119:ltmul1i |- ( 0 < 5 -> ( ( ; ; ; ; 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 ) ) ) 125::5pos |- 0 < 5 126:125,124:ax-mp |- ( ( ; ; ; ; 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 ) ) 127:: |- ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) < ( ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) x. 7 ) 128:127,126:mpbi |- ( ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) x. 5 ) < ( ( ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) x. 7 ) x. 5 ) 129:: |- ; ; ; ; 5 3 0 5 7 e. CC 130:: |- ; 7 3 e. CC 131:119:recni |- 5 e. CC 132:129,130,131:mulassi |- ( ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) x. 5 ) = ( ; ; ; ; 5 3 0 5 7 x. ( ; 7 3 x. 5 ) ) 133:: |- ; ; 3 6 5 e. NN 134:133:nnrei |- ; ; 3 6 5 e. RR 135:133:nngt0i |- 0 < ; ; 3 6 5 136:134,135:pm3.2i |- ( ; ; 3 6 5 e. RR /\ 0 < ; ; 3 6 5 ) 137:: |- ; ; 2 5 3 e. NN0 138:137:nn0rei |- ; ; 2 5 3 e. RR 139::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 ) ) ) 140:116,136,138,113,139: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 ) ) 141:: |- ( ; ; ; ; 5 3 0 5 7 x. ; ; 3 6 5 ) < ( ; ; 2 5 3 x. ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) ) 142:141,140:mpbi |- ( ; ; ; ; 5 3 0 5 7 / ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) ) < ( ; ; 2 5 3 / ; ; 3 6 5 ) 143::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 ) 144:116,110,143:mp2an |- ( ; ; ; ; 5 3 0 5 7 / ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) ) e. RR 145::nndivre |- ( ( ; ; 2 5 3 e. RR /\ ; ; 3 6 5 e. NN ) -> ( ; ; 2 5 3 / ; ; 3 6 5 ) e. RR ) 146:138,133,145:mp2an |- ( ; ; 2 5 3 / ; ; 3 6 5 ) e. RR 147:109,144,146: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 ) ) 148:118,142,147: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 ) 149:35,109,146: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 ) ) qed:55,148,149:mp2an |- ( log ` 2 ) < ( ; ; 2 5 3 / ; ; 3 6 5 ) \$)