Certified arcsine potential bounds (U56)

theorem Zeta5Irrational.U_676_1 : Uω (aρ 1) (bρ 1) (7226461069683 / 8000000000000) ≤ -(108859842802811722997 / 1000000000000000000000)

theorem Zeta5Irrational.U_676_2 : Uω (aρ 2) (bρ 2) (7226461069683 / 8000000000000) ≤ -(223049730527027750149 / 2000000000000000000000)

theorem Zeta5Irrational.U_676_3 : Uω (aρ 3) (bρ 3) (7226461069683 / 8000000000000) ≤ -(1168711495788115444963 / 10000000000000000000000)

theorem Zeta5Irrational.U_676_4 : Uω (aρ 4) (bρ 4) (7226461069683 / 8000000000000) ≤ -(628991572116585160863 / 5000000000000000000000)

theorem Zeta5Irrational.U_676_5 : Uω (aρ 5) (bρ 5) (7226461069683 / 8000000000000) ≤ -(55802843000971698371 / 400000000000000000000)

theorem Zeta5Irrational.U_676_6 : Uω (aρ 6) (bρ 6) (7226461069683 / 8000000000000) ≤ -(398517382703400588829 / 2500000000000000000000)

theorem Zeta5Irrational.U_676_7 : Uω (aρ 7) (bρ 7) (7226461069683 / 8000000000000) ≤ -(1870052209910470026807 / 10000000000000000000000)

theorem Zeta5Irrational.U_676_8 : Uω (aρ 8) (bρ 8) (7226461069683 / 8000000000000) ≤ -(1118883342221099544697 / 5000000000000000000000)

theorem Zeta5Irrational.U_676_9 : Uω (aρ 9) (bρ 9) (7226461069683 / 8000000000000) ≤ -(2710035841923158558309 / 10000000000000000000000)

theorem Zeta5Irrational.U_676_10 : Uω (aρ 10) (bρ 10) (7226461069683 / 8000000000000) ≤ -(3295663745591862291993 / 10000000000000000000000)

theorem Zeta5Irrational.U_676_11 : Uω (aρ 11) (bρ 11) (7226461069683 / 8000000000000) ≤ -(999108980076215164303 / 2500000000000000000000)

theorem Zeta5Irrational.U_676_12 : Uω (aρ 12) (bρ 12) (7226461069683 / 8000000000000) ≤ -(4802404152764222826933 / 10000000000000000000000)

theorem Zeta5Irrational.U_676_13 : Uω (aρ 13) (bρ 13) (7226461069683 / 8000000000000) ≤ -(2842013848850894396079 / 5000000000000000000000)

theorem Zeta5Irrational.U_676_14 : Uω (aρ 14) (bρ 14) (7226461069683 / 8000000000000) ≤ -(6579422346950211503277 / 10000000000000000000000)

theorem Zeta5Irrational.U_676_15 : Uω (aρ 15) (bρ 15) (7226461069683 / 8000000000000) ≤ -(7377973537692901902479 / 10000000000000000000000)

theorem Zeta5Irrational.U_676_16 : Uω (aρ 16) (bρ 16) (7226461069683 / 8000000000000) ≤ -(7917178800593945107141 / 10000000000000000000000)

theorem Zeta5Irrational.U_676 : Uρ (7226461069683 / 8000000000000) ≤ -(352383937996564167861 / 1250000000000000000000)

theorem Zeta5Irrational.U_677_1 : Uω (aρ 1) (bρ 1) (30159206983063 / 32000000000000) ≤ -(82643010106364090371 / 1250000000000000000000)

theorem Zeta5Irrational.U_677_2 : Uω (aρ 2) (bρ 2) (30159206983063 / 32000000000000) ≤ -(85834148424330625231 / 1250000000000000000000)

theorem Zeta5Irrational.U_677_3 : Uω (aρ 3) (bρ 3) (30159206983063 / 32000000000000) ≤ -(368936939244914093781 / 5000000000000000000000)

theorem Zeta5Irrational.U_677_4 : Uω (aρ 4) (bρ 4) (30159206983063 / 32000000000000) ≤ -(82332884107747569223 / 1000000000000000000000)

theorem Zeta5Irrational.U_677_5 : Uω (aρ 5) (bρ 5) (30159206983063 / 32000000000000) ≤ -(477229023155082316277 / 5000000000000000000000)

theorem Zeta5Irrational.U_677_6 : Uω (aρ 6) (bρ 6) (30159206983063 / 32000000000000) ≤ -(1144589866729602112133 / 10000000000000000000000)

theorem Zeta5Irrational.U_677_7 : Uω (aρ 7) (bρ 7) (30159206983063 / 32000000000000) ≤ -(1407832126127480045027 / 10000000000000000000000)

theorem Zeta5Irrational.U_677_8 : Uω (aρ 8) (bρ 8) (30159206983063 / 32000000000000) ≤ -(1757720990443800197271 / 10000000000000000000000)

theorem Zeta5Irrational.U_677_9 : Uω (aρ 9) (bρ 9) (30159206983063 / 32000000000000) ≤ -(2205550341869910017897 / 10000000000000000000000)

theorem Zeta5Irrational.U_677_10 : Uω (aρ 10) (bρ 10) (30159206983063 / 32000000000000) ≤ -(2758186921991172196263 / 10000000000000000000000)

theorem Zeta5Irrational.U_677_11 : Uω (aρ 11) (bρ 11) (30159206983063 / 32000000000000) ≤ -(426875502031516809391 / 1250000000000000000000)

theorem Zeta5Irrational.U_677_12 : Uω (aρ 12) (bρ 12) (30159206983063 / 32000000000000) ≤ -(4163275610179741765353 / 10000000000000000000000)

theorem Zeta5Irrational.U_677_13 : Uω (aρ 13) (bρ 13) (30159206983063 / 32000000000000) ≤ -(4971061494768781944211 / 10000000000000000000000)

theorem Zeta5Irrational.U_677_14 : Uω (aρ 14) (bρ 14) (30159206983063 / 32000000000000) ≤ -(2888495107361552193757 / 5000000000000000000000)

theorem Zeta5Irrational.U_677_15 : Uω (aρ 15) (bρ 15) (30159206983063 / 32000000000000) ≤ -(810002854756473131841 / 1250000000000000000000)

theorem Zeta5Irrational.U_677_16 : Uω (aρ 16) (bρ 16) (30159206983063 / 32000000000000) ≤ -(434015474906195459093 / 625000000000000000000)

theorem Zeta5Irrational.U_677 : Uρ (30159206983063 / 32000000000000) ≤ -(2318547818050359873459 / 10000000000000000000000)

theorem Zeta5Irrational.U_678_1 : Uω (aρ 1) (bρ 1) (15706284843697 / 16000000000000) ≤ -(31401869492385685679 / 1250000000000000000000)

theorem Zeta5Irrational.U_678_2 : Uω (aρ 2) (bρ 2) (15706284843697 / 16000000000000) ≤ -(275713462460201346549 / 10000000000000000000000)

theorem Zeta5Irrational.U_678_3 : Uω (aρ 3) (bρ 3) (15706284843697 / 16000000000000) ≤ -(20302229308895077003 / 625000000000000000000)

theorem Zeta5Irrational.U_678_4 : Uω (aρ 4) (bρ 4) (15706284843697 / 16000000000000) ≤ -(81357388672044063251 / 2000000000000000000000)

theorem Zeta5Irrational.U_678_5 : Uω (aρ 5) (bρ 5) (15706284843697 / 16000000000000) ≤ -(532453962168235848837 / 10000000000000000000000)

theorem Zeta5Irrational.U_678_6 : Uω (aρ 6) (bρ 6) (15706284843697 / 16000000000000) ≤ -(357237988318402216991 / 5000000000000000000000)

theorem Zeta5Irrational.U_678_7 : Uω (aρ 7) (bρ 7) (15706284843697 / 16000000000000) ≤ -(966103549437018389189 / 10000000000000000000000)

theorem Zeta5Irrational.U_678_8 : Uω (aρ 8) (bρ 8) (15706284843697 / 16000000000000) ≤ -(1299819252231914866819 / 10000000000000000000000)

theorem Zeta5Irrational.U_678_9 : Uω (aρ 9) (bρ 9) (15706284843697 / 16000000000000) ≤ -(172562545086624586799 / 1000000000000000000000)

theorem Zeta5Irrational.U_678_10 : Uω (aρ 10) (bρ 10) (15706284843697 / 16000000000000) ≤ -(2248820499400769661627 / 10000000000000000000000)

theorem Zeta5Irrational.U_678_11 : Uω (aρ 11) (bρ 11) (15706284843697 / 16000000000000) ≤ -(286694897106712835459 / 1000000000000000000000)

theorem Zeta5Irrational.U_678_12 : Uω (aρ 12) (bρ 12) (15706284843697 / 16000000000000) ≤ -(44567725956253433693 / 125000000000000000000)

theorem Zeta5Irrational.U_678_13 : Uω (aρ 13) (bρ 13) (15706284843697 / 16000000000000) ≤ -(4311189061635353508999 / 10000000000000000000000)

theorem Zeta5Irrational.U_678_14 : Uω (aρ 14) (bρ 14) (15706284843697 / 16000000000000) ≤ -(504471450642891062021 / 1000000000000000000000)

theorem Zeta5Irrational.U_678_15 : Uω (aρ 15) (bρ 15) (15706284843697 / 16000000000000) ≤ -(1134783711466407468651 / 2000000000000000000000)

theorem Zeta5Irrational.U_678_16 : Uω (aρ 16) (bρ 16) (15706284843697 / 16000000000000) ≤ -(1520695928810576621543 / 2500000000000000000000)

theorem Zeta5Irrational.U_678 : Uρ (15706284843697 / 16000000000000) ≤ -(92343274023702849147 / 500000000000000000000)

theorem Zeta5Irrational.U_679_1 : Uω (aρ 1) (bρ 1) (4239911887007 / 4000000000000) ≤ 32589570407983029189 / 625000000000000000000

theorem Zeta5Irrational.U_679_2 : Uω (aρ 2) (bρ 2) (4239911887007 / 4000000000000) ≤ 99752968003727494617 / 2000000000000000000000

theorem Zeta5Irrational.U_679_3 : Uω (aρ 3) (bρ 3) (4239911887007 / 4000000000000) ≤ 226665678130179312083 / 5000000000000000000000

theorem Zeta5Irrational.U_679_4 : Uω (aρ 4) (bρ 4) (4239911887007 / 4000000000000) ≤ 75518162225807609173 / 2000000000000000000000

theorem Zeta5Irrational.U_679_5 : Uω (aρ 5) (bρ 5) (4239911887007 / 4000000000000) ≤ 261587752722163667687 / 10000000000000000000000

theorem Zeta5Irrational.U_679_6 : Uω (aρ 6) (bρ 6) (4239911887007 / 4000000000000) ≤ 23468035726243644037 / 2500000000000000000000

theorem Zeta5Irrational.U_679_7 : Uω (aρ 7) (bρ 7) (4239911887007 / 4000000000000) ≤ -(17169293930414594967 / 1250000000000000000000)

theorem Zeta5Irrational.U_679_8 : Uω (aρ 8) (bρ 8) (4239911887007 / 4000000000000) ≤ -(13838695655646965701 / 312500000000000000000)

theorem Zeta5Irrational.U_679_9 : Uω (aρ 9) (bρ 9) (4239911887007 / 4000000000000) ≤ -(4152692092358634187 / 50000000000000000000)

theorem Zeta5Irrational.U_679_10 : Uω (aρ 10) (bρ 10) (4239911887007 / 4000000000000) ≤ -(325854264266228926319 / 2500000000000000000000)

theorem Zeta5Irrational.U_679_11 : Uω (aρ 11) (bρ 11) (4239911887007 / 4000000000000) ≤ -(928275361804200092781 / 5000000000000000000000)

theorem Zeta5Irrational.U_679_12 : Uω (aρ 12) (bρ 12) (4239911887007 / 4000000000000) ≤ -(98932252879129752837 / 400000000000000000000)

theorem Zeta5Irrational.U_679_13 : Uω (aρ 13) (bρ 13) (4239911887007 / 4000000000000) ≤ -(1560256889330704127261 / 5000000000000000000000)

theorem Zeta5Irrational.U_679_14 : Uω (aρ 14) (bρ 14) (4239911887007 / 4000000000000) ≤ -(748717128402485919173 / 2000000000000000000000)

theorem Zeta5Irrational.U_679_15 : Uω (aρ 15) (bρ 15) (4239911887007 / 4000000000000) ≤ -(2132701068385280181461 / 5000000000000000000000)

theorem Zeta5Irrational.U_679_16 : Uω (aρ 16) (bρ 16) (4239911887007 / 4000000000000) ≤ -(2298623924628737086939 / 5000000000000000000000)

theorem Zeta5Irrational.U_679 : Uρ (4239911887007 / 4000000000000) ≤ -(976182167040415310791 / 10000000000000000000000)

theorem Zeta5Irrational.U_680_1 : Uω (aρ 1) (bρ 1) (18213010252359 / 16000000000000) ≤ 1238640559424707941031 / 10000000000000000000000

theorem Zeta5Irrational.U_680_2 : Uω (aρ 2) (bρ 2) (18213010252359 / 16000000000000) ≤ 121754804071227033031 / 1000000000000000000000

theorem Zeta5Irrational.U_680_3 : Uω (aρ 3) (bρ 3) (18213010252359 / 16000000000000) ≤ 117528797438582498587 / 1000000000000000000000

theorem Zeta5Irrational.U_680_4 : Uω (aρ 4) (bρ 4) (18213010252359 / 16000000000000) ≤ 17263797762555920119 / 156250000000000000000

theorem Zeta5Irrational.U_680_5 : Uω (aρ 5) (bρ 5) (18213010252359 / 16000000000000) ≤ 49858176718355945399 / 500000000000000000000

theorem Zeta5Irrational.U_680_6 : Uω (aρ 6) (bρ 6) (18213010252359 / 16000000000000) ≤ 841668503982988491161 / 10000000000000000000000

theorem Zeta5Irrational.U_680_7 : Uω (aρ 7) (bρ 7) (18213010252359 / 16000000000000) ≤ 125556082777140847159 / 2000000000000000000000

theorem Zeta5Irrational.U_680_8 : Uω (aρ 8) (bρ 8) (18213010252359 / 16000000000000) ≤ 34611624805998184127 / 1000000000000000000000

theorem Zeta5Irrational.U_680_9 : Uω (aρ 9) (bρ 9) (18213010252359 / 16000000000000) ≤ -(9759515284691867981 / 10000000000000000000000)

theorem Zeta5Irrational.U_680_10 : Uω (aρ 10) (bρ 10) (18213010252359 / 16000000000000) ≤ -(441205039158688405329 / 10000000000000000000000)

theorem Zeta5Irrational.U_680_11 : Uω (aρ 11) (bρ 11) (18213010252359 / 16000000000000) ≤ -(235459762249886509823 / 2500000000000000000000)

theorem Zeta5Irrational.U_680_12 : Uω (aρ 12) (bρ 12) (18213010252359 / 16000000000000) ≤ -(186784175247454332741 / 1250000000000000000000)

theorem Zeta5Irrational.U_680_13 : Uω (aρ 13) (bρ 13) (18213010252359 / 16000000000000) ≤ -(2066466640027391588759 / 10000000000000000000000)

theorem Zeta5Irrational.U_680_14 : Uω (aρ 14) (bρ 14) (18213010252359 / 16000000000000) ≤ -(521780271597462009859 / 2000000000000000000000)

theorem Zeta5Irrational.U_680_15 : Uω (aρ 15) (bρ 15) (18213010252359 / 16000000000000) ≤ -(3055850814904569992253 / 10000000000000000000000)

theorem Zeta5Irrational.U_680_16 : Uω (aρ 16) (bρ 16) (18213010252359 / 16000000000000) ≤ -(834040341612878975103 / 2500000000000000000000)

theorem Zeta5Irrational.U_680 : Uρ (18213010252359 / 16000000000000) ≤ -(185691588642492027487 / 10000000000000000000000)

theorem Zeta5Irrational.U_681_1 : Uω (aρ 1) (bρ 1) (1946637295669 / 1600000000000) ≤ 381566729181073695513 / 2000000000000000000000

theorem Zeta5Irrational.U_681_2 : Uω (aρ 2) (bρ 2) (1946637295669 / 1600000000000) ≤ 944056028915092092057 / 5000000000000000000000

theorem Zeta5Irrational.U_681_3 : Uω (aρ 3) (bρ 3) (1946637295669 / 1600000000000) ≤ 1848611035360319879371 / 10000000000000000000000

theorem Zeta5Irrational.U_681_4 : Uω (aρ 4) (bρ 4) (1946637295669 / 1600000000000) ≤ 44570985859756852759 / 250000000000000000000

theorem Zeta5Irrational.U_681_5 : Uω (aρ 5) (bρ 5) (1946637295669 / 1600000000000) ≤ 210287390033879084137 / 1250000000000000000000

theorem Zeta5Irrational.U_681_6 : Uω (aρ 6) (bρ 6) (1946637295669 / 1600000000000) ≤ 38434103813816542803 / 250000000000000000000

theorem Zeta5Irrational.U_681_7 : Uω (aρ 7) (bρ 7) (1946637295669 / 1600000000000) ≤ 1338393787175108167323 / 10000000000000000000000

theorem Zeta5Irrational.U_681_8 : Uω (aρ 8) (bρ 8) (1946637295669 / 1600000000000) ≤ 538549030281882261609 / 5000000000000000000000

theorem Zeta5Irrational.U_681_9 : Uω (aρ 9) (bρ 9) (1946637295669 / 1600000000000) ≤ 748204042513207311507 / 10000000000000000000000

theorem Zeta5Irrational.U_681_10 : Uω (aρ 10) (bρ 10) (1946637295669 / 1600000000000) ≤ 351480511177384359847 / 10000000000000000000000

theorem Zeta5Irrational.U_681_11 : Uω (aρ 11) (bρ 11) (1946637295669 / 1600000000000) ≤ -(26459032811501839539 / 2500000000000000000000)

theorem Zeta5Irrational.U_681_12 : Uω (aρ 12) (bρ 12) (1946637295669 / 1600000000000) ≤ -(151566259945222584619 / 2500000000000000000000)

theorem Zeta5Irrational.U_681_13 : Uω (aρ 13) (bρ 13) (1946637295669 / 1600000000000) ≤ -(1119336165660419824783 / 10000000000000000000000)

theorem Zeta5Irrational.U_681_14 : Uω (aρ 14) (bρ 14) (1946637295669 / 1600000000000) ≤ -(800052579600481050621 / 5000000000000000000000)

theorem Zeta5Irrational.U_681_15 : Uω (aρ 15) (bρ 15) (1946637295669 / 1600000000000) ≤ -(1991591901709806684277 / 10000000000000000000000)

theorem Zeta5Irrational.U_681_16 : Uω (aρ 16) (bρ 16) (1946637295669 / 1600000000000) ≤ -(1117370294237785446319 / 5000000000000000000000)

theorem Zeta5Irrational.U_681 : Uρ (1946637295669 / 1600000000000) ≤ 539206832017378636869 / 10000000000000000000000

theorem Zeta5Irrational.U_682_1 : Uω (aρ 1) (bρ 1) (2746637295669 / 2000000000000) ≤ 1562609017187395006033 / 5000000000000000000000

theorem Zeta5Irrational.U_682_2 : Uω (aρ 2) (bρ 2) (2746637295669 / 2000000000000) ≤ 621553036055481657661 / 2000000000000000000000

theorem Zeta5Irrational.U_682_3 : Uω (aρ 3) (bρ 3) (2746637295669 / 2000000000000) ≤ 768206569321752291863 / 2500000000000000000000

theorem Zeta5Irrational.U_682_4 : Uω (aρ 4) (bρ 4) (2746637295669 / 2000000000000) ≤ 3014704537217327050923 / 10000000000000000000000

theorem Zeta5Irrational.U_682_5 : Uω (aρ 5) (bρ 5) (2746637295669 / 2000000000000) ≤ 585197835390417916143 / 2000000000000000000000

theorem Zeta5Irrational.U_682_6 : Uω (aρ 6) (bρ 6) (2746637295669 / 2000000000000) ≤ 1399192462686000616281 / 5000000000000000000000

theorem Zeta5Irrational.U_682_7 : Uω (aρ 7) (bρ 7) (2746637295669 / 2000000000000) ≤ 40996380119763539301 / 156250000000000000000

theorem Zeta5Irrational.U_682_8 : Uω (aρ 8) (bρ 8) (2746637295669 / 2000000000000) ≤ 2395479286330499915887 / 10000000000000000000000

theorem Zeta5Irrational.U_682_9 : Uω (aρ 9) (bρ 9) (2746637295669 / 2000000000000) ≤ 2109866511084314583863 / 10000000000000000000000

theorem Zeta5Irrational.U_682_10 : Uω (aρ 10) (bρ 10) (2746637295669 / 2000000000000) ≤ 1768087379828123108613 / 10000000000000000000000

theorem Zeta5Irrational.U_682_11 : Uω (aρ 11) (bρ 11) (2746637295669 / 2000000000000) ≤ 1378108348866220666213 / 10000000000000000000000

theorem Zeta5Irrational.U_682_12 : Uω (aρ 12) (bρ 12) (2746637295669 / 2000000000000) ≤ 956720482436799679737 / 10000000000000000000000

theorem Zeta5Irrational.U_682_13 : Uω (aρ 13) (bρ 13) (2746637295669 / 2000000000000) ≤ 531080877900712560969 / 10000000000000000000000

theorem Zeta5Irrational.U_682_14 : Uω (aρ 14) (bρ 14) (2746637295669 / 2000000000000) ≤ 34680649393365873701 / 2500000000000000000000

theorem Zeta5Irrational.U_682_15 : Uω (aρ 15) (bρ 15) (2746637295669 / 2000000000000) ≤ -(175689130303678076623 / 10000000000000000000000)

theorem Zeta5Irrational.U_682_16 : Uω (aρ 16) (bρ 16) (2746637295669 / 2000000000000) ≤ -(368491277579048029599 / 10000000000000000000000)

theorem Zeta5Irrational.U_682 : Uρ (2746637295669 / 2000000000000) ≤ 1832301135489243993659 / 10000000000000000000000

theorem Zeta5Irrational.U_683_1 : Uω (aρ 1) (bρ 1) (6746637295669 / 4000000000000) ≤ 648647470165495546441 / 1250000000000000000000

theorem Zeta5Irrational.U_683_2 : Uω (aρ 2) (bρ 2) (6746637295669 / 4000000000000) ≤ 646873916084388180027 / 1250000000000000000000

theorem Zeta5Irrational.U_683_3 : Uω (aρ 3) (bρ 3) (6746637295669 / 4000000000000) ≤ 5146608484439031249377 / 10000000000000000000000

theorem Zeta5Irrational.U_683_4 : Uω (aρ 4) (bρ 4) (6746637295669 / 4000000000000) ≤ 637431915769893316069 / 1250000000000000000000

theorem Zeta5Irrational.U_683_5 : Uω (aρ 5) (bρ 5) (6746637295669 / 4000000000000) ≤ 15711355649568528379 / 31250000000000000000

theorem Zeta5Irrational.U_683_6 : Uω (aρ 6) (bρ 6) (6746637295669 / 4000000000000) ≤ 1231163739354149495203 / 2500000000000000000000

theorem Zeta5Irrational.U_683_7 : Uω (aρ 7) (bρ 7) (6746637295669 / 4000000000000) ≤ 4784372414919632677529 / 10000000000000000000000

theorem Zeta5Irrational.U_683_8 : Uω (aρ 8) (bρ 8) (6746637295669 / 4000000000000) ≤ 1150527614874777660297 / 2500000000000000000000

theorem Zeta5Irrational.U_683_9 : Uω (aρ 9) (bρ 9) (6746637295669 / 4000000000000) ≤ 4375967434278497798067 / 10000000000000000000000

theorem Zeta5Irrational.U_683_10 : Uω (aρ 10) (bρ 10) (6746637295669 / 4000000000000) ≤ 4108233282580037516371 / 10000000000000000000000

theorem Zeta5Irrational.U_683_11 : Uω (aρ 11) (bρ 11) (6746637295669 / 4000000000000) ≤ 761357075335845670987 / 2000000000000000000000

theorem Zeta5Irrational.U_683_12 : Uω (aρ 12) (bρ 12) (6746637295669 / 4000000000000) ≤ 139448290184602758597 / 400000000000000000000

theorem Zeta5Irrational.U_683_13 : Uω (aρ 13) (bρ 13) (6746637295669 / 4000000000000) ≤ 3168189274869361871549 / 10000000000000000000000

theorem Zeta5Irrational.U_683_14 : Uω (aρ 14) (bρ 14) (6746637295669 / 4000000000000) ≤ 288054402101994101473 / 1000000000000000000000

theorem Zeta5Irrational.U_683_15 : Uω (aρ 15) (bρ 15) (6746637295669 / 4000000000000) ≤ 1327044432574458074269 / 5000000000000000000000

theorem Zeta5Irrational.U_683_16 : Uω (aρ 16) (bρ 16) (6746637295669 / 4000000000000) ≤ 2517089256916817378273 / 10000000000000000000000

theorem Zeta5Irrational.U_683 : Uρ (6746637295669 / 4000000000000) ≤ 991641173695049392639 / 2500000000000000000000

theorem Zeta5Irrational.U_684_1 : Uω (aρ 1) (bρ 1) 2 ≤ 431197938622519678389 / 625000000000000000000

theorem Zeta5Irrational.U_684_2 : Uω (aρ 2) (bρ 2) 2 ≤ 1721803564318625397281 / 2500000000000000000000

theorem Zeta5Irrational.U_684_3 : Uω (aρ 3) (bρ 3) 2 ≤ 3431657896680287743107 / 5000000000000000000000

theorem Zeta5Irrational.U_684_4 : Uω (aρ 4) (bρ 4) 2 ≤ 6823648472170288821807 / 10000000000000000000000

theorem Zeta5Irrational.U_684_5 : Uω (aρ 5) (bρ 5) 2 ≤ 6763315653946060878467 / 10000000000000000000000

theorem Zeta5Irrational.U_684_6 : Uω (aρ 6) (bρ 6) 2 ≤ 333849709093393011791 / 500000000000000000000

theorem Zeta5Irrational.U_684_7 : Uω (aρ 7) (bρ 7) 2 ≤ 3279879678491493456121 / 5000000000000000000000

theorem Zeta5Irrational.U_684_8 : Uω (aρ 8) (bρ 8) 2 ≤ 6408070500101273547501 / 10000000000000000000000

theorem Zeta5Irrational.U_684_9 : Uω (aρ 9) (bρ 9) 2 ≤ 3110439556119279087301 / 5000000000000000000000

theorem Zeta5Irrational.U_684_10 : Uω (aρ 10) (bρ 10) 2 ≤ 6000773764786687711391 / 10000000000000000000000

theorem Zeta5Irrational.U_684_11 : Uω (aρ 11) (bρ 11) 2 ≤ 5755005827102536483859 / 10000000000000000000000

theorem Zeta5Irrational.U_684_12 : Uω (aρ 12) (bρ 12) 2 ≤ 1099230232572658765387 / 2000000000000000000000

theorem Zeta5Irrational.U_684_13 : Uω (aρ 13) (bρ 13) 2 ≤ 2621030225880535406049 / 5000000000000000000000

theorem Zeta5Irrational.U_684_14 : Uω (aρ 14) (bρ 14) 2 ≤ 250733810854960598567 / 500000000000000000000

theorem Zeta5Irrational.U_684_15 : Uω (aρ 15) (bρ 15) 2 ≤ 2418686312017971573191 / 5000000000000000000000

theorem Zeta5Irrational.U_684_16 : Uω (aρ 16) (bρ 16) 2 ≤ 4730867613563951102639 / 10000000000000000000000

theorem Zeta5Irrational.U_684 : Uρ 2 ≤ 1138744120442109294651 / 2000000000000000000000