$( 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 ) ) ) ) a1::7nn |- 7 e. NN a2:a1:nncni |- 7 e. CC a3::5nn |- 5 e. NN a4:a3:nncni |- 5 e. CC a5::7t5e35 |- ( 7 x. 5 ) = ; 3 5 a6:a2,a4,a5:mulcomli |- ( 5 x. 7 ) = ; 3 5 a7::3nn0 |- 3 e. NN0 a8::5nn0 |- 5 e. NN0 a9::6nn |- 6 e. NN a10::5lt6 |- 5 < 6 a11:a7,a8,a9,a10:declt |- ; 3 5 < ; 3 6 a12:17:nncni |- 4 e. CC a13::2cn |- 2 e. CC a14::4t2e8 |- ( 4 x. 2 ) = 8 a15:a12,a13,a14:mulcomli |- ( 2 x. 4 ) = 8 a16:a15:oveq1i |- ( ( 2 x. 4 ) + 1 ) = ( 8 + 1 ) a17::8p1e9 |- ( 8 + 1 ) = 9 a18:a16,a17:eqtri |- ( ( 2 x. 4 ) + 1 ) = 9 a19:a18:oveq2i |- ( 4 x. ( ( 2 x. 4 ) + 1 ) ) = ( 4 x. 9 ) a20:22:nncni |- 9 e. CC a21::9t4e36 |- ( 9 x. 4 ) = ; 3 6 a22:a20,a12,a21:mulcomli |- ( 4 x. 9 ) = ; 3 6 a23:a19,a22:eqtri |- ( 4 x. ( ( 2 x. 4 ) + 1 ) ) = ; 3 6 a24:a11,a23:breqtrri |- ; 3 5 < ( 4 x. ( ( 2 x. 4 ) + 1 ) ) 59:a6,a24:eqbrtri |- ( 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 a25:a8,105:deccl |- ; 5 3 e. NN0 a26::0nn0 |- 0 e. NN0 a27:a25,a26:deccl |- ; ; 5 3 0 e. NN0 a28:a27,a8:deccl |- ; ; ; 5 3 0 5 e. NN0 a29::6nn0 |- 6 e. NN0 106:a28,a29:deccl |- ; ; ; ; 5 3 0 5 6 e. NN0 a30::6p1e7 |- ( 6 + 1 ) = 7 a31::eqid |- 6 = 6 a32:a31:oveq1i |- ( 6 + 1 ) = ( 6 + 1 ) a33:a30,a32:eqtri |- ( 6 + 1 ) = 7 a34::eqid |- ; ; ; ; 5 3 0 5 6 = ; ; ; ; 5 3 0 5 6 107:a28,a29,a33,a34:decsuc |- ( ; ; ; ; 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:a28,74:deccl |- ; ; ; ; 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 a35:74,105:deccl |- ; 7 3 e. NN0 120:115,a35:nn0mulcli |- ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) e. NN0 121:120:nn0rei |- ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) e. RR a36:18,a8:deccl |- ; 2 5 e. NN0 a37:a36,105:deccl |- ; ; 2 5 3 e. NN0 a38:105,74:nn0expcli |- ( 3 ^ 7 ) e. NN0 a39:a37,a38:nn0mulcli |- ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) e. NN0 122:a39,74:nn0mulcli |- ( ( ; ; 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 ) ) a40::eqid |- ; 7 3 = ; 7 3 a41:57,a8:deccl |- ; 1 5 e. NN0 a42::9nn0 |- 9 e. NN0 a43:a41,a42:deccl |- ; ; 1 5 9 e. NN0 a44:a43,57:deccl |- ; ; ; 1 5 9 1 e. NN0 a45:a44,74:deccl |- ; ; ; ; 1 5 9 1 7 e. NN0 a46::eqid |- ; ; ; ; 5 3 0 5 7 = ; ; ; ; 5 3 0 5 7 a47::eqid |- ; ; ; ; 1 5 9 1 7 = ; ; ; ; 1 5 9 1 7 a48::eqid |- ; ; ; 5 3 0 5 = ; ; ; 5 3 0 5 a49::eqid |- ; ; ; 1 5 9 1 = ; ; ; 1 5 9 1 a50::5p1e6 |- ( 5 + 1 ) = 6 a51:a4,4,a50:addcomli |- ( 1 + 5 ) = 6 a52:a43,57,a8,a49,a51:decaddi |- ( ; ; ; 1 5 9 1 + 5 ) = ; ; ; 1 5 9 6 a53:57,a29:deccl |- ; 1 6 e. NN0 a54::eqid |- ; ; 5 3 0 = ; ; 5 3 0 a55::eqid |- ; ; 1 5 9 = ; ; 1 5 9 a56::eqid |- ; 1 5 = ; 1 5 a57:57,a8,a50,a56:decsuc |- ( ; 1 5 + 1 ) = ; 1 6 a58::9p4e13 |- ( 9 + 4 ) = ; 1 3 a59:a41,a42,11,a55,a57,105,a58:decaddci |- ( ; ; 1 5 9 + 4 ) = ; ; 1 6 3 a60::eqid |- ; 5 3 = ; 5 3 a61:a53:nn0cni |- ; 1 6 e. CC a62:a61:addid1i |- ( ; 1 6 + 0 ) = ; 1 6 a63::2p1e3 |- ( 2 + 1 ) = 3 a64:81,4,a63:addcomli |- ( 1 + 2 ) = 3 a65:a64:oveq2i |- ( ( 5 x. 7 ) + ( 1 + 2 ) ) = ( ( 5 x. 7 ) + 3 ) a66::5p3e8 |- ( 5 + 3 ) = 8 a67:105,a8,105,a6,a66:decaddi |- ( ( 5 x. 7 ) + 3 ) = ; 3 8 a68:a65,a67:eqtri |- ( ( 5 x. 7 ) + ( 1 + 2 ) ) = ; 3 8 a69::7t3e21 |- ( 7 x. 3 ) = ; 2 1 a70:a2,3,a69:mulcomli |- ( 3 x. 7 ) = ; 2 1 a71:a9:nncni |- 6 e. CC a72:a71,4,a33:addcomli |- ( 1 + 6 ) = 7 a73:18,57,a29,a70,a72:decaddi |- ( ( 3 x. 7 ) + 6 ) = ; 2 7 a74:a8,105,57,a29,a60,a62,74,74,18,a68,a73:decmac |- ( ( ; 5 3 x. 7 ) + ( ; 1 6 + 0 ) ) = ; ; 3 8 7 a75:a2:mul02i |- ( 0 x. 7 ) = 0 a76:a75:oveq1i |- ( ( 0 x. 7 ) + 3 ) = ( 0 + 3 ) a77:3:addid2i |- ( 0 + 3 ) = 3 a78:a76,a77:eqtri |- ( ( 0 x. 7 ) + 3 ) = 3 a79:105:dec0h |- 3 = ; 0 3 a80:a78,a79:eqtri |- ( ( 0 x. 7 ) + 3 ) = ; 0 3 a81:a25,a26,a53,105,a54,a59,74,105,a26,a74,a80:decmac |- ( ( ; ; 5 3 0 x. 7 ) + ( ; ; 1 5 9 + 4 ) ) = ; ; ; 3 8 7 3 a82::3p1e4 |- ( 3 + 1 ) = 4 a83::eqid |- 3 = 3 a84:a83:oveq1i |- ( 3 + 1 ) = ( 3 + 1 ) a85:a82,a84:eqtri |- ( 3 + 1 ) = 4 a86::6p5e11 |- ( 6 + 5 ) = ; 1 1 a87:a71,a4,a86:addcomli |- ( 5 + 6 ) = ; 1 1 a88:105,a8,a29,a6,a85,57,a87:decaddci |- ( ( 5 x. 7 ) + 6 ) = ; 4 1 a89:a27,a8,a43,a29,a48,a52,74,57,11,a81,a88:decmac |- ( ( ; ; ; 5 3 0 5 x. 7 ) + ( ; ; ; 1 5 9 1 + 5 ) ) = ; ; ; ; 3 8 7 3 1 a90::7t7e49 |- ( 7 x. 7 ) = ; 4 9 a91::4p1e5 |- ( 4 + 1 ) = 5 a92::eqid |- 4 = 4 a93:a92:oveq1i |- ( 4 + 1 ) = ( 4 + 1 ) a94:a91,a93:eqtri |- ( 4 + 1 ) = 5 a95::9p7e16 |- ( 9 + 7 ) = ; 1 6 a96:11,a42,74,a90,a94,a29,a95:decaddci |- ( ( 7 x. 7 ) + 7 ) = ; 5 6 a97:a28,74,a44,74,a46,a47,74,a29,a8,a89,a96:decmac |- ( ( ; ; ; ; 5 3 0 5 7 x. 7 ) + ; ; ; ; 1 5 9 1 7 ) = ; ; ; ; ; 3 8 7 3 1 6 a98:18:dec0h |- 2 = ; 0 2 a99:4:addid2i |- ( 0 + 1 ) = 1 a100::eqid |- 0 = 0 a101:a100:oveq1i |- ( 0 + 1 ) = ( 0 + 1 ) a102:a99,a101:eqtri |- ( 0 + 1 ) = 1 a103:57:dec0h |- 1 = ; 0 1 a104:a102,a103:eqtri |- ( 0 + 1 ) = ; 0 1 a105::0cn |- 0 e. CC a106:a105:addid1i |- ( 0 + 0 ) = 0 a107:a26:dec0h |- 0 = ; 0 0 a108:a106,a107:eqtri |- ( 0 + 0 ) = ; 0 0 a109:a106:oveq2i |- ( ( 5 x. 3 ) + ( 0 + 0 ) ) = ( ( 5 x. 3 ) + 0 ) a110::5t3e15 |- ( 5 x. 3 ) = ; 1 5 a111:a110:oveq1i |- ( ( 5 x. 3 ) + 0 ) = ( ; 1 5 + 0 ) a112:a41:nn0cni |- ; 1 5 e. CC a113:a112:addid1i |- ( ; 1 5 + 0 ) = ; 1 5 a114:a111,a113:eqtri |- ( ( 5 x. 3 ) + 0 ) = ; 1 5 a115:a109,a114:eqtri |- ( ( 5 x. 3 ) + ( 0 + 0 ) ) = ; 1 5 a116::3t3e9 |- ( 3 x. 3 ) = 9 a117:a116:oveq1i |- ( ( 3 x. 3 ) + 0 ) = ( 9 + 0 ) a118:a20:addid1i |- ( 9 + 0 ) = 9 a119:a117,a118:eqtri |- ( ( 3 x. 3 ) + 0 ) = 9 a120:a42:dec0h |- 9 = ; 0 9 a121:a119,a120:eqtri |- ( ( 3 x. 3 ) + 0 ) = ; 0 9 a122:a8,105,a26,a26,a60,a108,105,a42,a26,a115,a121:decmac |- ( ( ; 5 3 x. 3 ) + ( 0 + 0 ) ) = ; ; 1 5 9 a123:3:mul02i |- ( 0 x. 3 ) = 0 a124:a123:oveq1i |- ( ( 0 x. 3 ) + 1 ) = ( 0 + 1 ) a125:a102,a124:eqtri |- ( ( 0 x. 3 ) + 1 ) = 1 a126:a125,a103:eqtri |- ( ( 0 x. 3 ) + 1 ) = ; 0 1 a127:a25,a26,a26,57,a54,a104,105,57,a26,a122,a126:decmac |- ( ( ; ; 5 3 0 x. 3 ) + ( 0 + 1 ) ) = ; ; ; 1 5 9 1 a128::5p2e7 |- ( 5 + 2 ) = 7 a129:57,a8,18,a110,a128:decaddi |- ( ( 5 x. 3 ) + 2 ) = ; 1 7 a130:a27,a8,a26,18,a48,a98,105,74,57,a127,a129:decmac |- ( ( ; ; ; 5 3 0 5 x. 3 ) + 2 ) = ; ; ; ; 1 5 9 1 7 a131:105,a28,74,a46,57,18,a130,a69:decmul1c |- ( ; ; ; ; 5 3 0 5 7 x. 3 ) = ; ; ; ; ; 1 5 9 1 7 1 a132:115,74,105,a40,57,a45,a97,a131:decmul2c |- ( ; ; ; ; 5 3 0 5 7 x. ; 7 3 ) = ; ; ; ; ; ; 3 8 7 3 1 6 1 a133::8nn0 |- 8 e. NN0 a134:105,a133:deccl |- ; 3 8 e. NN0 a135:a134,74:deccl |- ; ; 3 8 7 e. NN0 a136:a135,105:deccl |- ; ; ; 3 8 7 3 e. NN0 a137:a136,57:deccl |- ; ; ; ; 3 8 7 3 1 e. NN0 a138:a137,a29:deccl |- ; ; ; ; ; 3 8 7 3 1 6 e. NN0 a139:a137,74:deccl |- ; ; ; ; ; 3 8 7 3 1 7 e. NN0 a140::1lt10 |- 1 < 10 a141::6lt7 |- 6 < 7 a142:a137,a29,72,a141:declt |- ; ; ; ; ; 3 8 7 3 1 6 < ; ; ; ; ; 3 8 7 3 1 7 a143:a138,a139,57,74,a140,a142:decltc |- ; ; ; ; ; ; 3 8 7 3 1 6 1 < ; ; ; ; ; ; 3 8 7 3 1 7 7 a144:a8,a8:deccl |- ; 5 5 e. NN0 a145:a144,105:deccl |- ; ; 5 5 3 e. NN0 a146:a145,105:deccl |- ; ; ; 5 5 3 3 e. NN0 a147:a146,57:deccl |- ; ; ; ; 5 5 3 3 1 e. NN0 a148:18,57:deccl |- ; 2 1 e. NN0 a149:a148,a133:deccl |- ; ; 2 1 8 e. NN0 a150:74,18:deccl |- ; 7 2 e. NN0 a151:18,11:deccl |- ; 2 4 e. NN0 a152:92:oveq1i |- ( ( 3 ^ 2 ) x. 3 ) = ( 9 x. 3 ) a153::9t3e27 |- ( 9 x. 3 ) = ; 2 7 a154:a152,a153:eqtri |- ( ( 3 ^ 2 ) x. 3 ) = ; 2 7 a155:105,18,a63,a154:numexpp1 |- ( 3 ^ 3 ) = ; 2 7 a156::3t2e6 |- ( 3 x. 2 ) = 6 a157:3,81,a156:mulcomli |- ( 2 x. 3 ) = 6 a158:a157:oveq1i |- ( ( 2 x. 3 ) + 2 ) = ( 6 + 2 ) a159::6p2e8 |- ( 6 + 2 ) = 8 a160:a158,a159:eqtri |- ( ( 2 x. 3 ) + 2 ) = 8 a161:105,18,74,a155,57,18,a160,a69:decmul1c |- ( ( 3 ^ 3 ) x. 3 ) = ; 8 1 a162:105,105,a85,a161:numexpp1 |- ( 3 ^ 4 ) = ; 8 1 a163::8t3e24 |- ( 8 x. 3 ) = ; 2 4 a164:a163:oveq1i |- ( ( 8 x. 3 ) + 0 ) = ( ; 2 4 + 0 ) a165:a151:nn0cni |- ; 2 4 e. CC a166:a165:addid1i |- ( ; 2 4 + 0 ) = ; 2 4 a167:a164,a166:eqtri |- ( ( 8 x. 3 ) + 0 ) = ; 2 4 a168:3:mulid2i |- ( 1 x. 3 ) = 3 a169:a168,a79:eqtri |- ( 1 x. 3 ) = ; 0 3 a170:105,a133,57,a162,105,a26,a167,a169:decmul1c |- ( ( 3 ^ 4 ) x. 3 ) = ; ; 2 4 3 a171:105,11,a94,a170:numexpp1 |- ( 3 ^ 5 ) = ; ; 2 4 3 a172::eqid |- ; 2 4 = ; 2 4 a173:a157:oveq1i |- ( ( 2 x. 3 ) + 1 ) = ( 6 + 1 ) a174:a33,a173:eqtri |- ( ( 2 x. 3 ) + 1 ) = 7 a175::4t3e12 |- ( 4 x. 3 ) = ; 1 2 a176:105,18,11,a172,18,57,a174,a175:decmul1c |- ( ; 2 4 x. 3 ) = ; 7 2 a177:a176:oveq1i |- ( ( ; 2 4 x. 3 ) + 0 ) = ( ; 7 2 + 0 ) a178:a150:nn0cni |- ; 7 2 e. CC a179:a178:addid1i |- ( ; 7 2 + 0 ) = ; 7 2 a180:a177,a179:eqtri |- ( ( ; 2 4 x. 3 ) + 0 ) = ; 7 2 a181:a116,a120:eqtri |- ( 3 x. 3 ) = ; 0 9 a182:105,a151,105,a171,a42,a26,a180,a181:decmul1c |- ( ( 3 ^ 5 ) x. 3 ) = ; ; 7 2 9 a183:105,a8,a50,a182:numexpp1 |- ( 3 ^ 6 ) = ; ; 7 2 9 a184::eqid |- ; 7 2 = ; 7 2 a185:a106:oveq2i |- ( ( 7 x. 3 ) + ( 0 + 0 ) ) = ( ( 7 x. 3 ) + 0 ) a186:a69:oveq1i |- ( ( 7 x. 3 ) + 0 ) = ( ; 2 1 + 0 ) a187:a148:nn0cni |- ; 2 1 e. CC a188:a187:addid1i |- ( ; 2 1 + 0 ) = ; 2 1 a189:a186,a188:eqtri |- ( ( 7 x. 3 ) + 0 ) = ; 2 1 a190:a185,a189:eqtri |- ( ( 7 x. 3 ) + ( 0 + 0 ) ) = ; 2 1 a191:a133:dec0h |- 8 = ; 0 8 a192:a160,a191:eqtri |- ( ( 2 x. 3 ) + 2 ) = ; 0 8 a193:74,18,a26,18,a184,a98,105,a133,a26,a190,a192:decmac |- ( ( ; 7 2 x. 3 ) + 2 ) = ; ; 2 1 8 a194:105,a150,a42,a183,74,18,a193,a153:decmul1c |- ( ( 3 ^ 6 ) x. 3 ) = ; ; ; 2 1 8 7 a195:105,a29,a33,a194:numexpp1 |- ( 3 ^ 7 ) = ; ; ; 2 1 8 7 a196:57,74:deccl |- ; 1 7 e. NN0 a197:a196,74:deccl |- ; ; 1 7 7 e. NN0 a198::eqid |- ; ; 2 1 8 = ; ; 2 1 8 a199::eqid |- ; ; 1 7 7 = ; ; 1 7 7 a200:18,a26:deccl |- ; 2 0 e. NN0 a201:a200,105:deccl |- ; ; 2 0 3 e. NN0 a202:18,18:deccl |- ; 2 2 e. NN0 a203::eqid |- ; 2 1 = ; 2 1 a204::eqid |- ; 1 7 = ; 1 7 a205::eqid |- ; ; 2 0 3 = ; ; 2 0 3 a206::1p1e2 |- ( 1 + 1 ) = 2 a207::eqid |- 1 = 1 a208:a207:oveq1i |- ( 1 + 1 ) = ( 1 + 1 ) a209:a206,a208:eqtri |- ( 1 + 1 ) = 2 a210::eqid |- ; 2 0 = ; 2 0 a211:81:addid2i |- ( 0 + 2 ) = 2 a212:4:addid1i |- ( 1 + 0 ) = 1 a213:a26,57,18,a26,a103,a210,a211,a212:decadd |- ( 1 + ; 2 0 ) = ; 2 1 a214:18,57,a209,a213:decsuc |- ( ( 1 + ; 2 0 ) + 1 ) = ; 2 2 a215::7p3e10 |- ( 7 + 3 ) = 10 a216:57,74,a200,105,a204,a205,a214,a215:decaddc2 |- ( ; 1 7 + ; ; 2 0 3 ) = ; ; 2 2 0 a217::eqid |- ; ; 2 5 3 = ; ; 2 5 3 a218::eqid |- ; 2 2 = ; 2 2 a219::eqid |- ; 2 5 = ; 2 5 a220::2p2e4 |- ( 2 + 2 ) = 4 a221:a4,81,a128:addcomli |- ( 2 + 5 ) = 7 a222:18,18,18,a8,a218,a219,a220,a221:decadd |- ( ; 2 2 + ; 2 5 ) = ; 4 7 a223:a8:dec0h |- 5 = ; 0 5 a224:a94,a223:eqtri |- ( 4 + 1 ) = ; 0 5 a225::2t2e4 |- ( 2 x. 2 ) = 4 a226:a225,a102:oveq12i |- ( ( 2 x. 2 ) + ( 0 + 1 ) ) = ( 4 + 1 ) a227:a226,a94:eqtri |- ( ( 2 x. 2 ) + ( 0 + 1 ) ) = 5 a228::5t2e10 |- ( 5 x. 2 ) = 10 a229::dec10 |- 10 = ; 1 0 a230:a228,a229:eqtri |- ( 5 x. 2 ) = ; 1 0 a231:a4:addid2i |- ( 0 + 5 ) = 5 a232:57,a26,a8,a230,a231:decaddi |- ( ( 5 x. 2 ) + 5 ) = ; 1 5 a233:18,a8,a26,a8,a219,a224,18,a8,57,a227,a232:decmac |- ( ( ; 2 5 x. 2 ) + ( 4 + 1 ) ) = ; 5 5 a234:a156:oveq1i |- ( ( 3 x. 2 ) + 7 ) = ( 6 + 7 ) a235::7p6e13 |- ( 7 + 6 ) = ; 1 3 a236:a2,a71,a235:addcomli |- ( 6 + 7 ) = ; 1 3 a237:a234,a236:eqtri |- ( ( 3 x. 2 ) + 7 ) = ; 1 3 a238:a36,105,11,74,a217,a222,18,105,57,a233,a237:decmac |- ( ( ; ; 2 5 3 x. 2 ) + ( ; 2 2 + ; 2 5 ) ) = ; ; 5 5 3 a239:a37:nn0cni |- ; ; 2 5 3 e. CC a240:a239:mulid1i |- ( ; ; 2 5 3 x. 1 ) = ; ; 2 5 3 a241:a240:oveq1i |- ( ( ; ; 2 5 3 x. 1 ) + 0 ) = ( ; ; 2 5 3 + 0 ) a242:a239:addid1i |- ( ; ; 2 5 3 + 0 ) = ; ; 2 5 3 a243:a241,a242:eqtri |- ( ( ; ; 2 5 3 x. 1 ) + 0 ) = ; ; 2 5 3 a244:18,57,a202,a26,a203,a216,a37,105,a36,a238,a243:decma2c |- ( ( ; ; 2 5 3 x. ; 2 1 ) + ( ; 1 7 + ; ; 2 0 3 ) ) = ; ; ; 5 5 3 3 a245:74:dec0h |- 7 = ; 0 7 a246:a77,a79:eqtri |- ( 0 + 3 ) = ; 0 3 a247:80:addid2i |- ( 0 + 4 ) = 4 a248:a247:oveq2i |- ( ( 2 x. 8 ) + ( 0 + 4 ) ) = ( ( 2 x. 8 ) + 4 ) a249::8nn |- 8 e. NN a250:a249:nncni |- 8 e. CC a251::8t2e16 |- ( 8 x. 2 ) = ; 1 6 a252:a250,81,a251:mulcomli |- ( 2 x. 8 ) = ; 1 6 a253::6p4e10 |- ( 6 + 4 ) = 10 a254:57,a29,11,a252,a209,a253:decaddci2 |- ( ( 2 x. 8 ) + 4 ) = ; 2 0 a255:a248,a254:eqtri |- ( ( 2 x. 8 ) + ( 0 + 4 ) ) = ; 2 0 a256::8t5e40 |- ( 8 x. 5 ) = ; 4 0 a257:a250,a4,a256:mulcomli |- ( 5 x. 8 ) = ; 4 0 a258:11,a26,105,a257,a77:decaddi |- ( ( 5 x. 8 ) + 3 ) = ; 4 3 a259:18,a8,a26,105,a219,a246,a133,105,11,a255,a258:decmac |- ( ( ; 2 5 x. 8 ) + ( 0 + 3 ) ) = ; ; 2 0 3 a260:a250,3,a163:mulcomli |- ( 3 x. 8 ) = ; 2 4 a261::7p4e11 |- ( 7 + 4 ) = ; 1 1 a262:a2,80,a261:addcomli |- ( 4 + 7 ) = ; 1 1 a263:18,11,74,a260,a63,57,a262:decaddci |- ( ( 3 x. 8 ) + 7 ) = ; 3 1 a264:a36,105,a26,74,a217,a245,a133,57,105,a259,a263:decmac |- ( ( ; ; 2 5 3 x. 8 ) + 7 ) = ; ; ; 2 0 3 1 a265:a148,a133,a196,74,a198,a199,a37,57,a201,a244,a264:decma2c |- ( ( ; ; 2 5 3 x. ; ; 2 1 8 ) + ; ; 1 7 7 ) = ; ; ; ; 5 5 3 3 1 a266:a77:oveq2i |- ( ( 2 x. 7 ) + ( 0 + 3 ) ) = ( ( 2 x. 7 ) + 3 ) a267::7t2e14 |- ( 7 x. 2 ) = ; 1 4 a268:a2,81,a267:mulcomli |- ( 2 x. 7 ) = ; 1 4 a269::4p3e7 |- ( 4 + 3 ) = 7 a270:57,11,105,a268,a269:decaddi |- ( ( 2 x. 7 ) + 3 ) = ; 1 7 a271:a266,a270:eqtri |- ( ( 2 x. 7 ) + ( 0 + 3 ) ) = ; 1 7 a272:105,a8,18,a6,a128:decaddi |- ( ( 5 x. 7 ) + 2 ) = ; 3 7 a273:18,a8,a26,18,a219,a98,74,74,105,a271,a272:decmac |- ( ( ; 2 5 x. 7 ) + 2 ) = ; ; 1 7 7 a274:74,a36,105,a217,57,18,a273,a70:decmul1c |- ( ; ; 2 5 3 x. 7 ) = ; ; ; 1 7 7 1 a275:a37,a149,74,a195,57,a197,a265,a274:decmul2c |- ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) = ; ; ; ; ; 5 5 3 3 1 1 a276::eqid |- ; ; ; ; 5 5 3 3 1 = ; ; ; ; 5 5 3 3 1 a277::eqid |- ; ; ; 5 5 3 3 = ; ; ; 5 5 3 3 a278::eqid |- ; ; 5 5 3 = ; ; 5 5 3 a279::eqid |- ; 5 5 = ; 5 5 a280:a211,a98:eqtri |- ( 0 + 2 ) = ; 0 2 a281:a77:oveq2i |- ( ( 5 x. 7 ) + ( 0 + 3 ) ) = ( ( 5 x. 7 ) + 3 ) a282:a281,a67:eqtri |- ( ( 5 x. 7 ) + ( 0 + 3 ) ) = ; 3 8 a283:a8,a8,a26,18,a279,a280,74,74,105,a282,a272:decmac |- ( ( ; 5 5 x. 7 ) + ( 0 + 2 ) ) = ; ; 3 8 7 a284:18,57,18,a70,a64:decaddi |- ( ( 3 x. 7 ) + 2 ) = ; 2 3 a285:a144,105,a26,18,a278,a98,74,105,18,a283,a284:decmac |- ( ( ; ; 5 5 3 x. 7 ) + 2 ) = ; ; ; 3 8 7 3 a286:74,a145,105,a277,57,18,a285,a70:decmul1c |- ( ; ; ; 5 5 3 3 x. 7 ) = ; ; ; ; 3 8 7 3 1 a287:a286:oveq1i |- ( ( ; ; ; 5 5 3 3 x. 7 ) + 0 ) = ( ; ; ; ; 3 8 7 3 1 + 0 ) a288:a137:nn0cni |- ; ; ; ; 3 8 7 3 1 e. CC a289:a288:addid1i |- ( ; ; ; ; 3 8 7 3 1 + 0 ) = ; ; ; ; 3 8 7 3 1 a290:a287,a289:eqtri |- ( ( ; ; ; 5 5 3 3 x. 7 ) + 0 ) = ; ; ; ; 3 8 7 3 1 a291:a2:mulid2i |- ( 1 x. 7 ) = 7 a292:a291,a245:eqtri |- ( 1 x. 7 ) = ; 0 7 a293:74,a146,57,a276,74,a26,a290,a292:decmul1c |- ( ; ; ; ; 5 5 3 3 1 x. 7 ) = ; ; ; ; ; 3 8 7 3 1 7 a294:a293:oveq1i |- ( ( ; ; ; ; 5 5 3 3 1 x. 7 ) + 0 ) = ( ; ; ; ; ; 3 8 7 3 1 7 + 0 ) a295:a139:nn0cni |- ; ; ; ; ; 3 8 7 3 1 7 e. CC a296:a295:addid1i |- ( ; ; ; ; ; 3 8 7 3 1 7 + 0 ) = ; ; ; ; ; 3 8 7 3 1 7 a297:a294,a296:eqtri |- ( ( ; ; ; ; 5 5 3 3 1 x. 7 ) + 0 ) = ; ; ; ; ; 3 8 7 3 1 7 a298:74,a147,57,a275,74,a26,a297,a292:decmul1c |- ( ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) x. 7 ) = ; ; ; ; ; ; 3 8 7 3 1 7 7 a299:a143,a298:breqtrri |- ; ; ; ; ; ; 3 8 7 3 1 6 1 < ( ( ; ; 2 5 3 x. ( 3 ^ 7 ) ) x. 7 ) 127:a132,a299:eqbrtri |- ( ; ; ; ; 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:115:nn0cni |- ; ; ; ; 5 3 0 5 7 e. CC 130:a35:nn0cni |- ; 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 ) ) a300:105,a29:deccl |- ; 3 6 e. NN0 133:a300,60:decnncl |- ; ; 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::#a37 |- ; ; 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 ) ) a301::eqid |- ; ; 3 6 5 = ; ; 3 6 5 a302:18,a29:deccl |- ; 2 6 e. NN0 a303:a302,a8:deccl |- ; ; 2 6 5 e. NN0 a304:a303,18:deccl |- ; ; ; 2 6 5 2 e. NN0 a305:a304,a133:deccl |- ; ; ; ; 2 6 5 2 8 e. NN0 a306::eqid |- ; 3 6 = ; 3 6 a307::eqid |- ; ; ; ; 2 6 5 2 8 = ; ; ; ; 2 6 5 2 8 a308:105,57:deccl |- ; 3 1 e. NN0 a309:a308,a133:deccl |- ; ; 3 1 8 e. NN0 a310:a309,105:deccl |- ; ; ; 3 1 8 3 e. NN0 a311:a310,a8:deccl |- ; ; ; ; 3 1 8 3 5 e. NN0 a312:105,11:deccl |- ; 3 4 e. NN0 a313:a312,11:deccl |- ; ; 3 4 4 e. NN0 a314:a313,a133:deccl |- ; ; ; 3 4 4 8 e. NN0 a315::eqid |- ; ; ; 2 6 5 2 = ; ; ; 2 6 5 2 a316::eqid |- ; ; ; ; 3 1 8 3 5 = ; ; ; ; 3 1 8 3 5 a317::eqid |- ; ; 2 6 5 = ; ; 2 6 5 a318::eqid |- ; ; ; 3 1 8 3 = ; ; ; 3 1 8 3 a319::eqid |- ; 2 6 = ; 2 6 a320::eqid |- ; ; 3 1 8 = ; ; 3 1 8 a321::eqid |- ; 3 1 = ; 3 1 a322:a26,18,105,57,a98,a321,a77,a63:decadd |- ( 2 + ; 3 1 ) = ; 3 3 a323:105,105,a85,a322:decsuc |- ( ( 2 + ; 3 1 ) + 1 ) = ; 3 4 a324::8p6e14 |- ( 8 + 6 ) = ; 1 4 a325:a250,a71,a324:addcomli |- ( 6 + 8 ) = ; 1 4 a326:18,a29,a308,a133,a319,a320,a323,11,a325:decaddc |- ( ; 2 6 + ; ; 3 1 8 ) = ; ; 3 4 4 a327:a302,a8,a309,105,a317,a318,a326,a66:decadd |- ( ; ; 2 6 5 + ; ; ; 3 1 8 3 ) = ; ; ; 3 4 4 8 a328:a303,18,a310,a8,a315,a316,a327,a221:decadd |- ( ; ; ; 2 6 5 2 + ; ; ; ; 3 1 8 3 5 ) = ; ; ; ; 3 4 4 8 7 a329:a312,a8:deccl |- ; ; 3 4 5 e. NN0 a330::eqid |- ; ; ; 3 4 4 8 = ; ; ; 3 4 4 8 a331::eqid |- ; ; 3 4 4 = ; ; 3 4 4 a332:a312,11,a94,a331:decsuc |- ( ; ; 3 4 4 + 1 ) = ; ; 3 4 5 a333::8p2e10 |- ( 8 + 2 ) = 10 a334:a313,a133,18,a330,a332,a333:decaddci2 |- ( ; ; ; 3 4 4 8 + 2 ) = ; ; ; 3 4 5 0 a335::eqid |- ; ; 3 4 5 = ; ; 3 4 5 a336:a312,a8,a50,a335:decsuc |- ( ; ; 3 4 5 + 1 ) = ; ; 3 4 6 a337:a312:nn0cni |- ; 3 4 e. CC a338:a337:addid1i |- ( ; 3 4 + 0 ) = ; 3 4 a339:a85:oveq2i |- ( ( 5 x. 3 ) + ( 3 + 1 ) ) = ( ( 5 x. 3 ) + 4 ) a340::5p4e9 |- ( 5 + 4 ) = 9 a341:57,a8,11,a110,a340:decaddi |- ( ( 5 x. 3 ) + 4 ) = ; 1 9 a342:a339,a341:eqtri |- ( ( 5 x. 3 ) + ( 3 + 1 ) ) = ; 1 9 a343:a116:oveq1i |- ( ( 3 x. 3 ) + 4 ) = ( 9 + 4 ) a344:a343,a58:eqtri |- ( ( 3 x. 3 ) + 4 ) = ; 1 3 a345:a8,105,105,11,a60,a338,105,105,57,a342,a344:decmac |- ( ( ; 5 3 x. 3 ) + ( ; 3 4 + 0 ) ) = ; ; 1 9 3 a346:a123:oveq1i |- ( ( 0 x. 3 ) + 6 ) = ( 0 + 6 ) a347:a71:addid2i |- ( 0 + 6 ) = 6 a348:a346,a347:eqtri |- ( ( 0 x. 3 ) + 6 ) = 6 a349:a29:dec0h |- 6 = ; 0 6 a350:a348,a349:eqtri |- ( ( 0 x. 3 ) + 6 ) = ; 0 6 a351:a25,a26,a312,a29,a54,a336,105,a29,a26,a345,a350:decmac |- ( ( ; ; 5 3 0 x. 3 ) + ( ; ; 3 4 5 + 1 ) ) = ; ; ; 1 9 3 6 a352:a27,a8,a329,a26,a48,a334,105,a8,57,a351,a114:decmac |- ( ( ; ; ; 5 3 0 5 x. 3 ) + ( ; ; ; 3 4 4 8 + 2 ) ) = ; ; ; ; 1 9 3 6 5 a353::7p1e8 |- ( 7 + 1 ) = 8 a354:a2,4,a353:addcomli |- ( 1 + 7 ) = 8 a355:18,57,74,a69,a354:decaddi |- ( ( 7 x. 3 ) + 7 ) = ; 2 8 a356:a28,74,a314,74,a46,a328,105,a133,18,a352,a355:decmac |- ( ( ; ; ; ; 5 3 0 5 7 x. 3 ) + ( ; ; ; 2 6 5 2 + ; ; ; ; 3 1 8 3 5 ) ) = ; ; ; ; ; 1 9 3 6 5 8 a357:a231,a223:eqtri |- ( 0 + 5 ) = ; 0 5 a358:a102:oveq2i |- ( ( 5 x. 6 ) + ( 0 + 1 ) ) = ( ( 5 x. 6 ) + 1 ) a359::6t5e30 |- ( 6 x. 5 ) = ; 3 0 a360:a71,131,a359:mulcomli |- ( 5 x. 6 ) = ; 3 0 a361:105,a26,a102,a360:decsuc |- ( ( 5 x. 6 ) + 1 ) = ; 3 1 a362:a358,a361:eqtri |- ( ( 5 x. 6 ) + ( 0 + 1 ) ) = ; 3 1 a363::6t3e18 |- ( 6 x. 3 ) = ; 1 8 a364:a71,3,a363:mulcomli |- ( 3 x. 6 ) = ; 1 8 a365:a364:oveq1i |- ( ( 3 x. 6 ) + 0 ) = ( ; 1 8 + 0 ) a366:57,a133:deccl |- ; 1 8 e. NN0 a367:a366:nn0cni |- ; 1 8 e. CC a368:a367:addid1i |- ( ; 1 8 + 0 ) = ; 1 8 a369:a365,a368:eqtri |- ( ( 3 x. 6 ) + 0 ) = ; 1 8 a370:a8,105,a26,a26,a60,a108,a29,a133,57,a362,a369:decmac |- ( ( ; 5 3 x. 6 ) + ( 0 + 0 ) ) = ; ; 3 1 8 a371:a71:mul02i |- ( 0 x. 6 ) = 0 a372:a371:oveq1i |- ( ( 0 x. 6 ) + 3 ) = ( 0 + 3 ) a373:a372,a77:eqtri |- ( ( 0 x. 6 ) + 3 ) = 3 a374:a373,a79:eqtri |- ( ( 0 x. 6 ) + 3 ) = ; 0 3 a375:a25,a26,a26,105,a54,a246,a29,105,a26,a370,a374:decmac |- ( ( ; ; 5 3 0 x. 6 ) + ( 0 + 3 ) ) = ; ; ; 3 1 8 3 a376:105,a26,a8,a360,a231:decaddi |- ( ( 5 x. 6 ) + 5 ) = ; 3 5 a377:a27,a8,a26,a8,a48,a357,a29,a8,105,a375,a376:decmac |- ( ( ; ; ; 5 3 0 5 x. 6 ) + ( 0 + 5 ) ) = ; ; ; ; 3 1 8 3 5 a378::7t6e42 |- ( 7 x. 6 ) = ; 4 2 a379:a250,81,a333:addcomli |- ( 2 + 8 ) = 10 a380:11,18,a133,a378,a94,a379:decaddci2 |- ( ( 7 x. 6 ) + 8 ) = ; 5 0 a381:a28,74,a26,a133,a46,a191,a29,a26,a8,a377,a380:decmac |- ( ( ; ; ; ; 5 3 0 5 7 x. 6 ) + 8 ) = ; ; ; ; ; 3 1 8 3 5 0 a382:105,a29,a304,a133,a306,a307,115,a26,a311,a356,a381:decma2c |- ( ( ; ; ; ; 5 3 0 5 7 x. ; 3 6 ) + ; ; ; ; 2 6 5 2 8 ) = ; ; ; ; ; ; 1 9 3 6 5 8 0 a383:a102:oveq2i |- ( ( 5 x. 5 ) + ( 0 + 1 ) ) = ( ( 5 x. 5 ) + 1 ) a384::5t5e25 |- ( 5 x. 5 ) = ; 2 5 a385:18,a8,a50,a384:decsuc |- ( ( 5 x. 5 ) + 1 ) = ; 2 6 a386:a383,a385:eqtri |- ( ( 5 x. 5 ) + ( 0 + 1 ) ) = ; 2 6 a387:131,3,a110:mulcomli |- ( 3 x. 5 ) = ; 1 5 a388:a387:oveq1i |- ( ( 3 x. 5 ) + 0 ) = ( ; 1 5 + 0 ) a389:a388,a113:eqtri |- ( ( 3 x. 5 ) + 0 ) = ; 1 5 a390:a8,105,a26,a26,a60,a108,a8,a8,57,a386,a389:decmac |- ( ( ; 5 3 x. 5 ) + ( 0 + 0 ) ) = ; ; 2 6 5 a391:131:mul02i |- ( 0 x. 5 ) = 0 a392:a391:oveq1i |- ( ( 0 x. 5 ) + 2 ) = ( 0 + 2 ) a393:a392,a211:eqtri |- ( ( 0 x. 5 ) + 2 ) = 2 a394:a393,a98:eqtri |- ( ( 0 x. 5 ) + 2 ) = ; 0 2 a395:a25,a26,a26,18,a54,a280,a8,18,a26,a390,a394:decmac |- ( ( ; ; 5 3 0 x. 5 ) + ( 0 + 2 ) ) = ; ; ; 2 6 5 2 a396:18,a8,105,a384,a66:decaddi |- ( ( 5 x. 5 ) + 3 ) = ; 2 8 a397:a27,a8,a26,105,a48,a79,a8,a133,18,a395,a396:decmac |- ( ( ; ; ; 5 3 0 5 x. 5 ) + 3 ) = ; ; ; ; 2 6 5 2 8 a398:a8,a28,74,a46,a8,105,a397,a5:decmul1c |- ( ; ; ; ; 5 3 0 5 7 x. 5 ) = ; ; ; ; ; 2 6 5 2 8 5 a399:115,a300,a8,a301,a8,a305,a382,a398:decmul2c |- ( ; ; ; ; 5 3 0 5 7 x. ; ; 3 6 5 ) = ; ; ; ; ; ; ; 1 9 3 6 5 8 0 5 a400:57,a42:deccl |- ; 1 9 e. NN0 a401:a400,105:deccl |- ; ; 1 9 3 e. NN0 a402:a401,a29:deccl |- ; ; ; 1 9 3 6 e. NN0 a403:a402,a8:deccl |- ; ; ; ; 1 9 3 6 5 e. NN0 a404:a403,a133:deccl |- ; ; ; ; ; 1 9 3 6 5 8 e. NN0 a405:a404,a26:deccl |- ; ; ; ; ; ; 1 9 3 6 5 8 0 e. NN0 a406:a404,a133:deccl |- ; ; ; ; ; ; 1 9 3 6 5 8 8 e. NN0 a407::5lt10 |- 5 < 10 a408::8pos |- 0 < 8 a409:a404,a26,a249,a408:declt |- ; ; ; ; ; ; 1 9 3 6 5 8 0 < ; ; ; ; ; ; 1 9 3 6 5 8 8 a410:a405,a406,a8,a8,a407,a409:decltc |- ; ; ; ; ; ; ; 1 9 3 6 5 8 0 5 < ; ; ; ; ; ; ; 1 9 3 6 5 8 8 5 a411:74,a29:deccl |- ; 7 6 e. NN0 a412:a411,a8:deccl |- ; ; 7 6 5 e. NN0 a413:a412,11:deccl |- ; ; ; 7 6 5 4 e. NN0 a414::10nn0 |- 10 e. NN0 a415:a414,a42:deccl |- ; 10 9 e. NN0 a416:a415,105:deccl |- ; ; 10 9 3 e. NN0 a417::eqid |- ; ; 10 9 3 = ; ; 10 9 3 a418:57,57:deccl |- ; 1 1 e. NN0 a419::eqid |- ; 10 9 = ; 10 9 a420:57,a26,a102,a229:decsuc |- ( 10 + 1 ) = ; 1 1 a421::9p2e11 |- ( 9 + 2 ) = ; 1 1 a422:a414,a42,18,a419,a420,57,a421:decaddci |- ( ; 10 9 + 2 ) = ; ; 1 1 1 a423::eqid |- ; 1 1 = ; 1 1 a424:57,57,18,a423,a64:decaddi |- ( ; 1 1 + 2 ) = ; 1 3 a425:a157,a212:oveq12i |- ( ( 2 x. 3 ) + ( 1 + 0 ) ) = ( 6 + 1 ) a426:a425,a33:eqtri |- ( ( 2 x. 3 ) + ( 1 + 0 ) ) = 7 a427:a168:oveq1i |- ( ( 1 x. 3 ) + 3 ) = ( 3 + 3 ) a428::3p3e6 |- ( 3 + 3 ) = 6 a429:a427,a428:eqtri |- ( ( 1 x. 3 ) + 3 ) = 6 a430:a429,a349:eqtri |- ( ( 1 x. 3 ) + 3 ) = ; 0 6 a431:18,57,57,105,a203,a424,105,a29,a26,a426,a430:decmac |- ( ( ; 2 1 x. 3 ) + ( ; 1 1 + 2 ) ) = ; 7 6 a432:18,11,a94,a163:decsuc |- ( ( 8 x. 3 ) + 1 ) = ; 2 5 a433:a148,a133,a418,57,a198,a422,105,a8,18,a431,a432:decmac |- ( ( ; ; 2 1 8 x. 3 ) + ( ; 10 9 + 2 ) ) = ; ; 7 6 5 a434:3,4,a85:addcomli |- ( 1 + 3 ) = 4 a435:18,57,105,a69,a434:decaddi |- ( ( 7 x. 3 ) + 3 ) = ; 2 4 a436:a149,74,a415,105,a195,a417,105,11,18,a433,a435:decmac |- ( ( ( 3 ^ 7 ) x. 3 ) + ; ; 10 9 3 ) = ; ; ; 7 6 5 4 a437:11:dec0h |- 4 = ; 0 4 a438:a247,a437:eqtri |- ( 0 + 4 ) = ; 0 4 a439:131,81,a228:mulcomli |- ( 2 x. 5 ) = 10 a440:a439,a106:oveq12i |- ( ( 2 x. 5 ) + ( 0 + 0 ) ) = ( 10 + 0 ) a441::10nn |- 10 e. NN a442:a441:nncni |- 10 e. CC a443:a442:addid1i |- ( 10 + 0 ) = 10 a444:a440,a443:eqtri |- ( ( 2 x. 5 ) + ( 0 + 0 ) ) = 10 a445:131:mulid2i |- ( 1 x. 5 ) = 5 a446:a445:oveq1i |- ( ( 1 x. 5 ) + 4 ) = ( 5 + 4 ) a447:a446,a340:eqtri |- ( ( 1 x. 5 ) + 4 ) = 9 a448:a447,a120:eqtri |- ( ( 1 x. 5 ) + 4 ) = ; 0 9 a449:18,57,a26,11,a203,a438,a8,a42,a26,a444,a448:decmac |- ( ( ; 2 1 x. 5 ) + ( 0 + 4 ) ) = ; 10 9 a450:11,a26,105,a256,a77:decaddi |- ( ( 8 x. 5 ) + 3 ) = ; 4 3 a451:a148,a133,a26,105,a198,a79,a8,105,11,a449,a450:decmac |- ( ( ; ; 2 1 8 x. 5 ) + 3 ) = ; ; 10 9 3 a452:a8,a149,74,a195,a8,105,a451,a5:decmul1c |- ( ( 3 ^ 7 ) x. 5 ) = ; ; ; 10 9 3 5 a453:a38,105,a8,a6,a8,a416,a436,a452:decmul2c |- ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) = ; ; ; ; 7 6 5 4 5 a454:57,18:deccl |- ; 1 2 e. NN0 a455:a454,a29:deccl |- ; ; 1 2 6 e. NN0 a456::eqid |- ; ; ; 7 6 5 4 = ; ; ; 7 6 5 4 a457::eqid |- ; ; 1 2 6 = ; ; 1 2 6 a458:a414,57:deccl |- ; 10 1 e. NN0 a459::eqid |- ; ; 7 6 5 = ; ; 7 6 5 a460::eqid |- ; 1 2 = ; 1 2 a461::eqid |- ; 10 1 = ; 10 1 a462:a26,57,57,a26,a103,a229,a102,a212:decadd |- ( 1 + 10 ) = ; 1 1 a463:57,18,a414,57,a460,a461,a462,a63:decadd |- ( ; 1 2 + ; 10 1 ) = ; ; 1 1 3 a464:57,105:deccl |- ; 1 3 e. NN0 a465::eqid |- ; 7 6 = ; 7 6 a466:a26,57,57,18,a103,a460,a102,a64:decadd |- ( 1 + ; 1 2 ) = ; 1 3 a467:57,57,a454,a29,a423,a457,a466,a72:decadd |- ( ; 1 1 + ; ; 1 2 6 ) = ; ; 1 3 7 a468:a41,18:deccl |- ; ; 1 5 2 e. NN0 a469::eqid |- ; 1 3 = ; 1 3 a470::eqid |- ; ; 1 5 2 = ; ; 1 5 2 a471:a26,57,57,a8,a103,a56,a102,a51:decadd |- ( 1 + ; 1 5 ) = ; 1 6 a472::3p2e5 |- ( 3 + 2 ) = 5 a473:57,105,a41,18,a469,a470,a471,a472:decadd |- ( ; 1 3 + ; ; 1 5 2 ) = ; ; 1 6 5 a474::eqid |- ; 1 6 = ; 1 6 a475:57,a29,18,a474,a159:decaddi |- ( ; 1 6 + 2 ) = ; 1 8 a476:80,4,a94:addcomli |- ( 1 + 4 ) = 5 a477:a476:oveq2i |- ( ( 2 x. 7 ) + ( 1 + 4 ) ) = ( ( 2 x. 7 ) + 5 ) a478:131,80,a340:addcomli |- ( 4 + 5 ) = 9 a479:57,11,a8,a268,a478:decaddi |- ( ( 2 x. 7 ) + 5 ) = ; 1 9 a480:a477,a479:eqtri |- ( ( 2 x. 7 ) + ( 1 + 4 ) ) = ; 1 9 a481::8p5e13 |- ( 8 + 5 ) = ; 1 3 a482:a250,131,a481:addcomli |- ( 5 + 8 ) = ; 1 3 a483:105,a8,a133,a6,a85,105,a482:decaddci |- ( ( 5 x. 7 ) + 8 ) = ; 4 3 a484:18,a8,57,a133,a219,a475,74,105,11,a480,a483:decmac |- ( ( ; 2 5 x. 7 ) + ( ; 1 6 + 2 ) ) = ; ; 1 9 3 a485:18,57,a8,a70,a51:decaddi |- ( ( 3 x. 7 ) + 5 ) = ; 2 6 a486:a36,105,a53,a8,a217,a473,74,a29,18,a484,a485:decmac |- ( ( ; ; 2 5 3 x. 7 ) + ( ; 1 3 + ; ; 1 5 2 ) ) = ; ; ; 1 9 3 6 a487:a77:oveq2i |- ( ( 2 x. 6 ) + ( 0 + 3 ) ) = ( ( 2 x. 6 ) + 3 ) a488::6t2e12 |- ( 6 x. 2 ) = ; 1 2 a489:a71,81,a488:mulcomli |- ( 2 x. 6 ) = ; 1 2 a490:3,81,a472:addcomli |- ( 2 + 3 ) = 5 a491:57,18,105,a489,a490:decaddi |- ( ( 2 x. 6 ) + 3 ) = ; 1 5 a492:a487,a491:eqtri |- ( ( 2 x. 6 ) + ( 0 + 3 ) ) = ; 1 5 a493:105,a26,18,a360,a211:decaddi |- ( ( 5 x. 6 ) + 2 ) = ; 3 2 a494:18,a8,a26,18,a219,a280,a29,18,105,a492,a493:decmac |- ( ( ; 2 5 x. 6 ) + ( 0 + 2 ) ) = ; ; 1 5 2 a495::8p7e15 |- ( 8 + 7 ) = ; 1 5 a496:57,a133,74,a364,a209,a8,a495:decaddci |- ( ( 3 x. 6 ) + 7 ) = ; 2 5 a497:a36,105,a26,74,a217,a245,a29,a8,18,a494,a496:decmac |- ( ( ; ; 2 5 3 x. 6 ) + 7 ) = ; ; ; 1 5 2 5 a498:74,a29,a464,74,a465,a467,137,a8,a468,a486,a497:decma2c |- ( ( ; ; 2 5 3 x. ; 7 6 ) + ( ; 1 1 + ; ; 1 2 6 ) ) = ; ; ; ; 1 9 3 6 5 a499:a211:oveq2i |- ( ( 2 x. 5 ) + ( 0 + 2 ) ) = ( ( 2 x. 5 ) + 2 ) a500:a439,a229:eqtri |- ( 2 x. 5 ) = ; 1 0 a501:57,a26,18,a500,a211:decaddi |- ( ( 2 x. 5 ) + 2 ) = ; 1 2 a502:a499,a501:eqtri |- ( ( 2 x. 5 ) + ( 0 + 2 ) ) = ; 1 2 a503:18,a8,a26,57,a219,a104,a8,a29,18,a502,a385:decmac |- ( ( ; 2 5 x. 5 ) + ( 0 + 1 ) ) = ; ; 1 2 6 a504:57,a8,105,a387,a66:decaddi |- ( ( 3 x. 5 ) + 3 ) = ; 1 8 a505:a36,105,a26,105,a217,a79,a8,a133,57,a503,a504:decmac |- ( ( ; ; 2 5 3 x. 5 ) + 3 ) = ; ; ; 1 2 6 8 a506:a411,a8,a418,105,a459,a463,137,a133,a455,a498,a505:decma2c |- ( ( ; ; 2 5 3 x. ; ; 7 6 5 ) + ( ; 1 2 + ; 10 1 ) ) = ; ; ; ; ; 1 9 3 6 5 8 a507:a15,a211:oveq12i |- ( ( 2 x. 4 ) + ( 0 + 2 ) ) = ( 8 + 2 ) a508:a507,a333:eqtri |- ( ( 2 x. 4 ) + ( 0 + 2 ) ) = 10 a509::5t4e20 |- ( 5 x. 4 ) = ; 2 0 a510:18,a26,a102,a509:decsuc |- ( ( 5 x. 4 ) + 1 ) = ; 2 1 a511:18,a8,a26,57,a219,a104,11,57,18,a508,a510:decmac |- ( ( ; 2 5 x. 4 ) + ( 0 + 1 ) ) = ; 10 1 a512:80,3,a175:mulcomli |- ( 3 x. 4 ) = ; 1 2 a513:a71,81,a159:addcomli |- ( 2 + 6 ) = 8 a514:57,18,a29,a512,a513:decaddi |- ( ( 3 x. 4 ) + 6 ) = ; 1 8 a515:a36,105,a26,a29,a217,a349,11,a133,57,a511,a514:decmac |- ( ( ; ; 2 5 3 x. 4 ) + 6 ) = ; ; 10 1 8 a516:a412,11,a454,a29,a456,a457,137,a133,a458,a506,a515:decma2c |- ( ( ; ; 2 5 3 x. ; ; ; 7 6 5 4 ) + ; ; 1 2 6 ) = ; ; ; ; ; ; 1 9 3 6 5 8 8 a517:18,a8,a26,57,a219,a103,a8,a29,18,a502,a385:decmac |- ( ( ; 2 5 x. 5 ) + 1 ) = ; ; 1 2 6 a518:a8,a36,105,a217,a8,57,a517,a387:decmul1c |- ( ; ; 2 5 3 x. 5 ) = ; ; ; 1 2 6 5 a519:137,a413,a8,a453,a8,a455,a516,a518:decmul2c |- ( ; ; 2 5 3 x. ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) ) = ; ; ; ; ; ; ; 1 9 3 6 5 8 8 5 a520:a410,a519:breqtrri |- ; ; ; ; ; ; ; 1 9 3 6 5 8 0 5 < ( ; ; 2 5 3 x. ( ( 3 ^ 7 ) x. ( 5 x. 7 ) ) ) 141:a399,a520:eqbrtri |- ( ; ; ; ; 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 ) $)