Certified arcsine potential bounds (U44)

theorem Zeta5Irrational.U_532_1 : Uω (aρ 1) (bρ 1) (9733558271547 / 16000000000000) ≤ -(1015344587023385956413 / 2000000000000000000000)

theorem Zeta5Irrational.U_532_2 : Uω (aρ 2) (bρ 2) (9733558271547 / 16000000000000) ≤ -(2558270898826269298443 / 5000000000000000000000)

theorem Zeta5Irrational.U_532_3 : Uω (aρ 3) (bρ 3) (9733558271547 / 16000000000000) ≤ -(12991658015855303567 / 25000000000000000000)

theorem Zeta5Irrational.U_532_4 : Uω (aρ 4) (bρ 4) (9733558271547 / 16000000000000) ≤ -(5331181911364434298457 / 10000000000000000000000)

theorem Zeta5Irrational.U_532_5 : Uω (aρ 5) (bρ 5) (9733558271547 / 16000000000000) ≤ -(2769801986054336931911 / 5000000000000000000000)

theorem Zeta5Irrational.U_532_6 : Uω (aρ 6) (bρ 6) (9733558271547 / 16000000000000) ≤ -(58463779834278348057 / 100000000000000000000)

theorem Zeta5Irrational.U_532_7 : Uω (aρ 7) (bρ 7) (9733558271547 / 16000000000000) ≤ -(6280854844228632773047 / 10000000000000000000000)

theorem Zeta5Irrational.U_532_8 : Uω (aρ 8) (bρ 8) (9733558271547 / 16000000000000) ≤ -(343910265860526981271 / 500000000000000000000)

theorem Zeta5Irrational.U_532_9 : Uω (aρ 9) (bρ 9) (9733558271547 / 16000000000000) ≤ -(7682410227718395423797 / 10000000000000000000000)

theorem Zeta5Irrational.U_532_10 : Uω (aρ 10) (bρ 10) (9733558271547 / 16000000000000) ≤ -(1750874840954918337967 / 2000000000000000000000)

theorem Zeta5Irrational.U_532_11 : Uω (aρ 11) (bρ 11) (9733558271547 / 16000000000000) ≤ -(2548920187344628660401 / 2500000000000000000000)

theorem Zeta5Irrational.U_532_12 : Uω (aρ 12) (bρ 12) (9733558271547 / 16000000000000) ≤ -(3060087048242988541479 / 2500000000000000000000)

theorem Zeta5Irrational.U_532_13 : Uω (aρ 13) (bρ 13) (9733558271547 / 16000000000000) ≤ -(16115495756291320341457 / 10000000000000000000000)

theorem Zeta5Irrational.U_532_14 : Uω (aρ 14) (bρ 14) (9733558271547 / 16000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_532_15 : Uω (aρ 15) (bρ 15) (9733558271547 / 16000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_532_16 : Uω (aρ 16) (bρ 16) (9733558271547 / 16000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_532 : Uρ (9733558271547 / 16000000000000) ≤ -(4092119036616476838689 / 5000000000000000000000)

theorem Zeta5Irrational.U_533_1 : Uω (aρ 1) (bρ 1) (312024205529 / 512000000000) ≤ -(2529440222003763779621 / 5000000000000000000000)

theorem Zeta5Irrational.U_533_2 : Uω (aρ 2) (bρ 2) (312024205529 / 512000000000) ≤ -(5098627734197961890647 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_3 : Uω (aρ 3) (bρ 3) (312024205529 / 512000000000) ≤ -(5178603814400613640559 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_4 : Uω (aρ 4) (bρ 4) (312024205529 / 512000000000) ≤ -(5312874499598534674163 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_5 : Uω (aρ 5) (bρ 5) (312024205529 / 512000000000) ≤ -(5520902007877414746151 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_6 : Uω (aρ 6) (bρ 6) (312024205529 / 512000000000) ≤ -(2913535717514371392481 / 5000000000000000000000)

theorem Zeta5Irrational.U_533_7 : Uω (aρ 7) (bρ 7) (312024205529 / 512000000000) ≤ -(6260639779296802408789 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_8 : Uω (aρ 8) (bρ 8) (312024205529 / 512000000000) ≤ -(6856629979244132857753 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_9 : Uω (aρ 9) (bρ 9) (312024205529 / 512000000000) ≤ -(3829383450332178808059 / 5000000000000000000000)

theorem Zeta5Irrational.U_533_10 : Uω (aρ 10) (bρ 10) (312024205529 / 512000000000) ≤ -(272732777028236039401 / 312500000000000000000)

theorem Zeta5Irrational.U_533_11 : Uω (aρ 11) (bρ 11) (312024205529 / 512000000000) ≤ -(10163034798815418328541 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_12 : Uω (aρ 12) (bρ 12) (312024205529 / 512000000000) ≤ -(12195252362156481322259 / 10000000000000000000000)

theorem Zeta5Irrational.U_533_13 : Uω (aρ 13) (bρ 13) (312024205529 / 512000000000) ≤ -(3999156105056330198967 / 2500000000000000000000)

theorem Zeta5Irrational.U_533_14 : Uω (aρ 14) (bρ 14) (312024205529 / 512000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_533_15 : Uω (aρ 15) (bρ 15) (312024205529 / 512000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_533_16 : Uω (aρ 16) (bρ 16) (312024205529 / 512000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_533 : Uρ (312024205529 / 512000000000) ≤ -(8158113287143502076381 / 10000000000000000000000)

theorem Zeta5Irrational.U_534_1 : Uω (aρ 1) (bρ 1) (19535909148031 / 32000000000000) ≤ -(2520534865968170005413 / 5000000000000000000000)

theorem Zeta5Irrational.U_534_2 : Uω (aρ 2) (bρ 2) (19535909148031 / 32000000000000) ≤ -(5080745706614145080733 / 10000000000000000000000)

theorem Zeta5Irrational.U_534_3 : Uω (aρ 3) (bρ 3) (19535909148031 / 32000000000000) ≤ -(258028849230606099 / 500000000000000000)

theorem Zeta5Irrational.U_534_4 : Uω (aρ 4) (bρ 4) (19535909148031 / 32000000000000) ≤ -(5294600563066589342857 / 10000000000000000000000)

theorem Zeta5Irrational.U_534_5 : Uω (aρ 5) (bρ 5) (19535909148031 / 32000000000000) ≤ -(1100447002148356538251 / 2000000000000000000000)

theorem Zeta5Irrational.U_534_6 : Uω (aρ 6) (bρ 6) (19535909148031 / 32000000000000) ≤ -(1161560447106391500073 / 2000000000000000000000)

theorem Zeta5Irrational.U_534_7 : Uω (aρ 7) (bρ 7) (19535909148031 / 32000000000000) ≤ -(1560116466927709879407 / 2500000000000000000000)

theorem Zeta5Irrational.U_534_8 : Uω (aρ 8) (bρ 8) (19535909148031 / 32000000000000) ≤ -(3417551010603838729737 / 5000000000000000000000)

theorem Zeta5Irrational.U_534_9 : Uω (aρ 9) (bρ 9) (19535909148031 / 32000000000000) ≤ -(7635181723425072818701 / 10000000000000000000000)

theorem Zeta5Irrational.U_534_10 : Uω (aρ 10) (bρ 10) (19535909148031 / 32000000000000) ≤ -(8700602322136267647359 / 10000000000000000000000)

theorem Zeta5Irrational.U_534_11 : Uω (aρ 11) (bρ 11) (19535909148031 / 32000000000000) ≤ -(10130515627069486294957 / 10000000000000000000000)

theorem Zeta5Irrational.U_534_12 : Uω (aρ 12) (bρ 12) (19535909148031 / 32000000000000) ≤ -(6075226774800110837489 / 5000000000000000000000)

theorem Zeta5Irrational.U_534_13 : Uω (aρ 13) (bρ 13) (19535909148031 / 32000000000000) ≤ -(3970586139317389642427 / 2500000000000000000000)

theorem Zeta5Irrational.U_534_14 : Uω (aρ 14) (bρ 14) (19535909148031 / 32000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_534_15 : Uω (aρ 15) (bρ 15) (19535909148031 / 32000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_534_16 : Uω (aρ 16) (bρ 16) (19535909148031 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_534 : Uρ (19535909148031 / 32000000000000) ≤ -(8132319092386912548451 / 10000000000000000000000)

theorem Zeta5Irrational.U_535_1 : Uω (aρ 1) (bρ 1) (39140610900999 / 64000000000000) ≤ -(2511645342950552390927 / 5000000000000000000000)

theorem Zeta5Irrational.U_535_2 : Uω (aρ 2) (bρ 2) (39140610900999 / 64000000000000) ≤ -(5062895600518868362853 / 10000000000000000000000)

theorem Zeta5Irrational.U_535_3 : Uω (aρ 3) (bρ 3) (39140610900999 / 64000000000000) ≤ -(1028516519948136732061 / 2000000000000000000000)

theorem Zeta5Irrational.U_535_4 : Uω (aρ 4) (bρ 4) (39140610900999 / 64000000000000) ≤ -(263817998974931911661 / 500000000000000000000)

theorem Zeta5Irrational.U_535_5 : Uω (aρ 5) (bρ 5) (39140610900999 / 64000000000000) ≤ -(685450356247687421249 / 1250000000000000000000)

theorem Zeta5Irrational.U_535_6 : Uω (aρ 6) (bρ 6) (39140610900999 / 64000000000000) ≤ -(5788570240149873008043 / 10000000000000000000000)

theorem Zeta5Irrational.U_535_7 : Uω (aρ 7) (bρ 7) (39140610900999 / 64000000000000) ≤ -(3110166470379501080453 / 5000000000000000000000)

theorem Zeta5Irrational.U_535_8 : Uω (aρ 8) (bρ 8) (39140610900999 / 64000000000000) ≤ -(6813621231441943836873 / 10000000000000000000000)

theorem Zeta5Irrational.U_535_9 : Uω (aρ 9) (bρ 9) (39140610900999 / 64000000000000) ≤ -(190291359982045990177 / 250000000000000000000)

theorem Zeta5Irrational.U_535_10 : Uω (aρ 10) (bρ 10) (39140610900999 / 64000000000000) ≤ -(4336917040251970202751 / 5000000000000000000000)

theorem Zeta5Irrational.U_535_11 : Uω (aρ 11) (bρ 11) (39140610900999 / 64000000000000) ≤ -(5049061054212899413027 / 5000000000000000000000)

theorem Zeta5Irrational.U_535_12 : Uω (aρ 12) (bρ 12) (39140610900999 / 64000000000000) ≤ -(12105946844337847702467 / 10000000000000000000000)

theorem Zeta5Irrational.U_535_13 : Uω (aρ 13) (bρ 13) (39140610900999 / 64000000000000) ≤ -(7886087677459839047893 / 5000000000000000000000)

theorem Zeta5Irrational.U_535_14 : Uω (aρ 14) (bρ 14) (39140610900999 / 64000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_535_15 : Uω (aρ 15) (bρ 15) (39140610900999 / 64000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_535_16 : Uω (aρ 16) (bρ 16) (39140610900999 / 64000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_535 : Uρ (39140610900999 / 64000000000000) ≤ -(8106826625353221444803 / 10000000000000000000000)

theorem Zeta5Irrational.U_536_1 : Uω (aρ 1) (bρ 1) (2450587719121 / 4000000000000) ≤ -(1251385798375307642803 / 2500000000000000000000)

theorem Zeta5Irrational.U_536_2 : Uω (aρ 2) (bρ 2) (2450587719121 / 4000000000000) ≤ -(5045077302141448493163 / 10000000000000000000000)

theorem Zeta5Irrational.U_536_3 : Uω (aρ 3) (bρ 3) (2450587719121 / 4000000000000) ≤ -(640577567897808385041 / 1250000000000000000000)

theorem Zeta5Irrational.U_536_4 : Uω (aρ 4) (bρ 4) (2450587719121 / 4000000000000) ≤ -(164317269602931110393 / 312500000000000000000)

theorem Zeta5Irrational.U_536_5 : Uω (aρ 5) (bρ 5) (2450587719121 / 4000000000000) ≤ -(5465005395609099705269 / 10000000000000000000000)

theorem Zeta5Irrational.U_536_6 : Uω (aρ 6) (bρ 6) (2450587719121 / 4000000000000) ≤ -(1442343826234602812091 / 2500000000000000000000)

theorem Zeta5Irrational.U_536_7 : Uω (aρ 7) (bρ 7) (2450587719121 / 4000000000000) ≤ -(620024083077386747109 / 1000000000000000000000)

theorem Zeta5Irrational.U_536_8 : Uω (aρ 8) (bρ 8) (2450587719121 / 4000000000000) ≤ -(6792187399728591460427 / 10000000000000000000000)

theorem Zeta5Irrational.U_536_9 : Uω (aρ 9) (bρ 9) (2450587719121 / 4000000000000) ≤ -(7588184633861080601369 / 10000000000000000000000)

theorem Zeta5Irrational.U_536_10 : Uω (aρ 10) (bρ 10) (2450587719121 / 4000000000000) ≤ -(1080892956124258428013 / 1250000000000000000000)

theorem Zeta5Irrational.U_536_11 : Uω (aρ 11) (bρ 11) (2450587719121 / 4000000000000) ≤ -(314557910422104071209 / 312500000000000000000)

theorem Zeta5Irrational.U_536_12 : Uω (aρ 12) (bρ 12) (2450587719121 / 4000000000000) ≤ -(6030863735264409501953 / 5000000000000000000000)

theorem Zeta5Irrational.U_536_13 : Uω (aρ 13) (bρ 13) (2450587719121 / 4000000000000) ≤ -(3133142970538085451271 / 2000000000000000000000)

theorem Zeta5Irrational.U_536_14 : Uω (aρ 14) (bρ 14) (2450587719121 / 4000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_536_15 : Uω (aρ 15) (bρ 15) (2450587719121 / 4000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_536_16 : Uω (aρ 16) (bρ 16) (2450587719121 / 4000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_536 : Uρ (2450587719121 / 4000000000000) ≤ -(252550364807948996239 / 312500000000000000000)

theorem Zeta5Irrational.U_537_1 : Uω (aρ 1) (bρ 1) (39278196110873 / 64000000000000) ≤ -(2493913571466764627649 / 5000000000000000000000)

theorem Zeta5Irrational.U_537_2 : Uω (aρ 2) (bρ 2) (39278196110873 / 64000000000000) ≤ -(1005458139663677673063 / 2000000000000000000000)

theorem Zeta5Irrational.U_537_3 : Uω (aρ 3) (bρ 3) (39278196110873 / 64000000000000) ≤ -(5106690698961235973153 / 10000000000000000000000)

theorem Zeta5Irrational.U_537_4 : Uω (aρ 4) (bρ 4) (39278196110873 / 64000000000000) ≤ -(5239978385515379585033 / 10000000000000000000000)

theorem Zeta5Irrational.U_537_5 : Uω (aρ 5) (bρ 5) (39278196110873 / 64000000000000) ≤ -(5446442518364453498131 / 10000000000000000000000)

theorem Zeta5Irrational.U_537_6 : Uω (aρ 6) (bρ 6) (39278196110873 / 64000000000000) ≤ -(5750217286790455522099 / 10000000000000000000000)

theorem Zeta5Irrational.U_537_7 : Uω (aρ 7) (bρ 7) (39278196110873 / 64000000000000) ≤ -(6180189371123662487857 / 10000000000000000000000)

theorem Zeta5Irrational.U_537_8 : Uω (aρ 8) (bρ 8) (39278196110873 / 64000000000000) ≤ -(1692700079319226165529 / 2500000000000000000000)

theorem Zeta5Irrational.U_537_9 : Uω (aρ 9) (bρ 9) (39278196110873 / 64000000000000) ≤ -(3782386067554484225809 / 5000000000000000000000)

theorem Zeta5Irrational.U_537_10 : Uω (aρ 10) (bρ 10) (39278196110873 / 64000000000000) ≤ -(8620530541481646251921 / 10000000000000000000000)

theorem Zeta5Irrational.U_537_11 : Uω (aρ 11) (bρ 11) (39278196110873 / 64000000000000) ≤ -(2508426902235644193011 / 2500000000000000000000)

theorem Zeta5Irrational.U_537_12 : Uω (aρ 12) (bρ 12) (39278196110873 / 64000000000000) ≤ -(1502223847783784689383 / 1250000000000000000000)

theorem Zeta5Irrational.U_537_13 : Uω (aρ 13) (bρ 13) (39278196110873 / 64000000000000) ≤ -(15562622929320063846659 / 10000000000000000000000)

theorem Zeta5Irrational.U_537_14 : Uω (aρ 14) (bρ 14) (39278196110873 / 64000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_537_15 : Uω (aρ 15) (bρ 15) (39278196110873 / 64000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_537_16 : Uω (aρ 16) (bρ 16) (39278196110873 / 64000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_537 : Uρ (39278196110873 / 64000000000000) ≤ -(4028326837852990601667 / 5000000000000000000000)

theorem Zeta5Irrational.U_538_1 : Uω (aρ 1) (bρ 1) (3934698871581 / 6400000000000) ≤ -(4970142422987990689033 / 10000000000000000000000)

theorem Zeta5Irrational.U_538_2 : Uω (aρ 2) (bρ 2) (3934698871581 / 6400000000000) ≤ -(626191959561132738727 / 1250000000000000000000)

theorem Zeta5Irrational.U_538_3 : Uω (aρ 3) (bρ 3) (3934698871581 / 6400000000000) ≤ -(5088792951723855824927 / 10000000000000000000000)

theorem Zeta5Irrational.U_538_4 : Uω (aρ 4) (bρ 4) (3934698871581 / 6400000000000) ≤ -(1305459283471519444757 / 2500000000000000000000)

theorem Zeta5Irrational.U_538_5 : Uω (aρ 5) (bρ 5) (3934698871581 / 6400000000000) ≤ -(339244630606834053439 / 625000000000000000000)

theorem Zeta5Irrational.U_538_6 : Uω (aρ 6) (bρ 6) (3934698871581 / 6400000000000) ≤ -(2865548021714676276341 / 5000000000000000000000)

theorem Zeta5Irrational.U_538_7 : Uω (aρ 7) (bρ 7) (3934698871581 / 6400000000000) ≤ -(24640713584814710663 / 40000000000000000000)

theorem Zeta5Irrational.U_538_8 : Uω (aρ 8) (bρ 8) (3934698871581 / 6400000000000) ≤ -(6749459776710677993977 / 10000000000000000000000)

theorem Zeta5Irrational.U_538_9 : Uω (aρ 9) (bρ 9) (3934698871581 / 6400000000000) ≤ -(3770708306633194469347 / 5000000000000000000000)

theorem Zeta5Irrational.U_538_10 : Uω (aρ 10) (bρ 10) (3934698871581 / 6400000000000) ≤ -(8593994276661595780249 / 10000000000000000000000)

theorem Zeta5Irrational.U_538_11 : Uω (aρ 11) (bρ 11) (3934698871581 / 6400000000000) ≤ -(10001684457041864999147 / 10000000000000000000000)

theorem Zeta5Irrational.U_538_12 : Uω (aρ 12) (bρ 12) (3934698871581 / 6400000000000) ≤ -(5987066129331995198681 / 5000000000000000000000)

theorem Zeta5Irrational.U_538_13 : Uω (aρ 13) (bρ 13) (3934698871581 / 6400000000000) ≤ -(3092521747675457896549 / 2000000000000000000000)

theorem Zeta5Irrational.U_538_14 : Uω (aρ 14) (bρ 14) (3934698871581 / 6400000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_538_15 : Uω (aρ 15) (bρ 15) (3934698871581 / 6400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_538_16 : Uω (aρ 16) (bρ 16) (3934698871581 / 6400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_538 : Uρ (3934698871581 / 6400000000000) ≤ -(1003991872383418357177 / 1250000000000000000000)

theorem Zeta5Irrational.U_539_1 : Uω (aρ 1) (bρ 1) (39415781320747 / 64000000000000) ≤ -(39619911384348771533 / 80000000000000000000)

theorem Zeta5Irrational.U_539_2 : Uω (aρ 2) (bρ 2) (39415781320747 / 64000000000000) ≤ -(4991812124691438887987 / 10000000000000000000000)

theorem Zeta5Irrational.U_539_3 : Uω (aρ 3) (bρ 3) (39415781320747 / 64000000000000) ≤ -(2535463593367915656409 / 5000000000000000000000)

theorem Zeta5Irrational.U_539_4 : Uω (aρ 4) (bρ 4) (39415781320747 / 64000000000000) ≤ -(162616523524473707163 / 312500000000000000000)

theorem Zeta5Irrational.U_539_5 : Uω (aρ 5) (bρ 5) (39415781320747 / 64000000000000) ≤ -(5409419981822095878167 / 10000000000000000000000)

theorem Zeta5Irrational.U_539_6 : Uω (aρ 6) (bρ 6) (39415781320747 / 64000000000000) ≤ -(2856005716701236298161 / 5000000000000000000000)

theorem Zeta5Irrational.U_539_7 : Uω (aρ 7) (bρ 7) (39415781320747 / 64000000000000) ≤ -(614020774142777776231 / 1000000000000000000000)

theorem Zeta5Irrational.U_539_8 : Uω (aρ 8) (bρ 8) (39415781320747 / 64000000000000) ≤ -(6728165572055259940237 / 10000000000000000000000)

theorem Zeta5Irrational.U_539_9 : Uω (aρ 9) (bρ 9) (39415781320747 / 64000000000000) ≤ -(7518117780844264344539 / 10000000000000000000000)

theorem Zeta5Irrational.U_539_10 : Uω (aρ 10) (bρ 10) (39415781320747 / 64000000000000) ≤ -(8567534377982396619123 / 10000000000000000000000)

theorem Zeta5Irrational.U_539_11 : Uω (aρ 11) (bρ 11) (39415781320747 / 64000000000000) ≤ -(1993956523096417586819 / 2000000000000000000000)

theorem Zeta5Irrational.U_539_12 : Uω (aρ 12) (bρ 12) (39415781320747 / 64000000000000) ≤ -(745671718695141265711 / 625000000000000000000)

theorem Zeta5Irrational.U_539_13 : Uω (aρ 13) (bρ 13) (39415781320747 / 64000000000000) ≤ -(7682710624029974679527 / 5000000000000000000000)

theorem Zeta5Irrational.U_539_14 : Uω (aρ 14) (bρ 14) (39415781320747 / 64000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_539_15 : Uω (aρ 15) (bρ 15) (39415781320747 / 64000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_539_16 : Uω (aρ 16) (bρ 16) (39415781320747 / 64000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_539 : Uρ (39415781320747 / 64000000000000) ≤ -(8007440285446487712989 / 10000000000000000000000)

theorem Zeta5Irrational.U_540_1 : Uω (aρ 1) (bρ 1) (9871143481421 / 16000000000000) ≤ -(4934866533064163862467 / 10000000000000000000000)

theorem Zeta5Irrational.U_540_2 : Uω (aρ 2) (bρ 2) (9871143481421 / 16000000000000) ≤ -(497411993155784997629 / 1000000000000000000000)

theorem Zeta5Irrational.U_540_3 : Uω (aρ 3) (bρ 3) (9871143481421 / 16000000000000) ≤ -(631636661234611895621 / 1250000000000000000000)

theorem Zeta5Irrational.U_540_4 : Uω (aρ 4) (bρ 4) (9871143481421 / 16000000000000) ≤ -(648206640404216422783 / 1250000000000000000000)

theorem Zeta5Irrational.U_540_5 : Uω (aρ 5) (bρ 5) (9871143481421 / 16000000000000) ≤ -(5390960067592240995977 / 10000000000000000000000)

theorem Zeta5Irrational.U_540_6 : Uω (aρ 6) (bρ 6) (9871143481421 / 16000000000000) ≤ -(2846481658037417445579 / 5000000000000000000000)

theorem Zeta5Irrational.U_540_7 : Uω (aρ 7) (bρ 7) (9871143481421 / 16000000000000) ≤ -(6120277243219995072763 / 10000000000000000000000)

theorem Zeta5Irrational.U_540_8 : Uω (aρ 8) (bρ 8) (9871143481421 / 16000000000000) ≤ -(670691749872474504841 / 1000000000000000000000)

theorem Zeta5Irrational.U_540_9 : Uω (aρ 9) (bρ 9) (9871143481421 / 16000000000000) ≤ -(7494875352599199835211 / 10000000000000000000000)

theorem Zeta5Irrational.U_540_10 : Uω (aρ 10) (bρ 10) (9871143481421 / 16000000000000) ≤ -(8541150373580887895981 / 10000000000000000000000)

theorem Zeta5Irrational.U_540_11 : Uω (aρ 11) (bρ 11) (9871143481421 / 16000000000000) ≤ -(397520041479983402797 / 400000000000000000000)

theorem Zeta5Irrational.U_540_12 : Uω (aρ 12) (bρ 12) (9871143481421 / 16000000000000) ≤ -(475505288755951282507 / 400000000000000000000)

theorem Zeta5Irrational.U_540_13 : Uω (aρ 13) (bρ 13) (9871143481421 / 16000000000000) ≤ -(7635420998099539770937 / 5000000000000000000000)

theorem Zeta5Irrational.U_540_14 : Uω (aρ 14) (bρ 14) (9871143481421 / 16000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_540_15 : Uω (aρ 15) (bρ 15) (9871143481421 / 16000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_540_16 : Uω (aρ 16) (bρ 16) (9871143481421 / 16000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_540 : Uρ (9871143481421 / 16000000000000) ≤ -(1596631244612458406567 / 2000000000000000000000)

theorem Zeta5Irrational.U_541_1 : Uω (aρ 1) (bρ 1) (39553366530621 / 64000000000000) ≤ -(4917275143594234884783 / 10000000000000000000000)

theorem Zeta5Irrational.U_541_2 : Uω (aρ 2) (bρ 2) (39553366530621 / 64000000000000) ≤ -(77444671661105992217 / 156250000000000000000)

theorem Zeta5Irrational.U_541_3 : Uω (aρ 3) (bρ 3) (39553366530621 / 64000000000000) ≤ -(2517645573818314008889 / 5000000000000000000000)

theorem Zeta5Irrational.U_541_4 : Uω (aρ 4) (bρ 4) (39553366530621 / 64000000000000) ≤ -(2583805063455020443923 / 5000000000000000000000)

theorem Zeta5Irrational.U_541_5 : Uω (aρ 5) (bρ 5) (39553366530621 / 64000000000000) ≤ -(83945847197113369509 / 156250000000000000000)

theorem Zeta5Irrational.U_541_6 : Uω (aρ 6) (bρ 6) (39553366530621 / 64000000000000) ≤ -(354621971976424965729 / 625000000000000000000)

theorem Zeta5Irrational.U_541_7 : Uω (aρ 7) (bρ 7) (39553366530621 / 64000000000000) ≤ -(3050193369503106150261 / 5000000000000000000000)

theorem Zeta5Irrational.U_541_8 : Uω (aρ 8) (bρ 8) (39553366530621 / 64000000000000) ≤ -(3342857676754653328359 / 5000000000000000000000)

theorem Zeta5Irrational.U_541_9 : Uω (aρ 9) (bρ 9) (39553366530621 / 64000000000000) ≤ -(116745141336085632999 / 156250000000000000000)

theorem Zeta5Irrational.U_541_10 : Uω (aρ 10) (bρ 10) (39553366530621 / 64000000000000) ≤ -(8514841796218230196619 / 10000000000000000000000)

theorem Zeta5Irrational.U_541_11 : Uω (aρ 11) (bρ 11) (39553366530621 / 64000000000000) ≤ -(9906338689090923457797 / 10000000000000000000000)

theorem Zeta5Irrational.U_541_12 : Uω (aρ 12) (bρ 12) (39553366530621 / 64000000000000) ≤ -(2368956448966278179891 / 2000000000000000000000)

theorem Zeta5Irrational.U_541_13 : Uω (aρ 13) (bρ 13) (39553366530621 / 64000000000000) ≤ -(15178679457575972544311 / 10000000000000000000000)

theorem Zeta5Irrational.U_541_14 : Uω (aρ 14) (bρ 14) (39553366530621 / 64000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_541_15 : Uω (aρ 15) (bρ 15) (39553366530621 / 64000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_541_16 : Uω (aρ 16) (bρ 16) (39553366530621 / 64000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_541 : Uρ (39553366530621 / 64000000000000) ≤ -(1591814203017836894719 / 2000000000000000000000)

theorem Zeta5Irrational.U_542_1 : Uω (aρ 1) (bρ 1) (19811079567779 / 32000000000000) ≤ -(195988585830199645053 / 400000000000000000000)

theorem Zeta5Irrational.U_542_2 : Uω (aρ 2) (bρ 2) (19811079567779 / 32000000000000) ≤ -(617353647344841031591 / 1250000000000000000000)

theorem Zeta5Irrational.U_542_3 : Uω (aρ 3) (bρ 3) (19811079567779 / 32000000000000) ≤ -(5017520647110118038431 / 10000000000000000000000)

theorem Zeta5Irrational.U_542_4 : Uω (aρ 4) (bρ 4) (19811079567779 / 32000000000000) ≤ -(514959964612481159213 / 1000000000000000000000)

theorem Zeta5Irrational.U_542_5 : Uω (aρ 5) (bρ 5) (19811079567779 / 32000000000000) ≤ -(1070828463037465693711 / 2000000000000000000000)

theorem Zeta5Irrational.U_542_6 : Uω (aρ 6) (bρ 6) (19811079567779 / 32000000000000) ≤ -(565497600102780771467 / 1000000000000000000000)

theorem Zeta5Irrational.U_542_7 : Uω (aρ 7) (bρ 7) (19811079567779 / 32000000000000) ≤ -(6080536067205933051063 / 10000000000000000000000)

theorem Zeta5Irrational.U_542_8 : Uω (aρ 8) (bρ 8) (19811079567779 / 32000000000000) ≤ -(6664558934562687843943 / 10000000000000000000000)

theorem Zeta5Irrational.U_542_9 : Uω (aρ 9) (bρ 9) (19811079567779 / 32000000000000) ≤ -(1862139644687844223167 / 2500000000000000000000)

theorem Zeta5Irrational.U_542_10 : Uω (aρ 10) (bρ 10) (19811079567779 / 32000000000000) ≤ -(8488608183216975225863 / 10000000000000000000000)

theorem Zeta5Irrational.U_542_11 : Uω (aρ 11) (bρ 11) (19811079567779 / 32000000000000) ≤ -(4937397276860661833359 / 5000000000000000000000)

theorem Zeta5Irrational.U_542_12 : Uω (aρ 12) (bρ 12) (19811079567779 / 32000000000000) ≤ -(2950548377821138222619 / 2500000000000000000000)

theorem Zeta5Irrational.U_542_13 : Uω (aρ 13) (bρ 13) (19811079567779 / 32000000000000) ≤ -(15088764605498135512977 / 10000000000000000000000)

theorem Zeta5Irrational.U_542_14 : Uω (aρ 14) (bρ 14) (19811079567779 / 32000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_542_15 : Uω (aρ 15) (bρ 15) (19811079567779 / 32000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_542_16 : Uω (aρ 16) (bρ 16) (19811079567779 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_542 : Uρ (19811079567779 / 32000000000000) ≤ -(7935174218185580261567 / 10000000000000000000000)

theorem Zeta5Irrational.U_543_1 : Uω (aρ 1) (bρ 1) (7938190348099 / 12800000000000) ≤ -(195287397249608713577 / 400000000000000000000)

theorem Zeta5Irrational.U_543_2 : Uω (aρ 2) (bρ 2) (7938190348099 / 12800000000000) ≤ -(492123039929203977663 / 1000000000000000000000)

theorem Zeta5Irrational.U_543_3 : Uω (aρ 3) (bρ 3) (7938190348099 / 12800000000000) ≤ -(4999781675993666482479 / 10000000000000000000000)

theorem Zeta5Irrational.U_543_4 : Uω (aρ 4) (bρ 4) (7938190348099 / 12800000000000) ≤ -(2565810781913314626317 / 5000000000000000000000)

theorem Zeta5Irrational.U_543_5 : Uω (aρ 5) (bρ 5) (7938190348099 / 12800000000000) ≤ -(5335784226300181600677 / 10000000000000000000000)

theorem Zeta5Irrational.U_543_6 : Uω (aρ 6) (bρ 6) (7938190348099 / 12800000000000) ≤ -(2818018263035098048087 / 5000000000000000000000)

theorem Zeta5Irrational.U_543_7 : Uω (aρ 7) (bρ 7) (7938190348099 / 12800000000000) ≤ -(1515181266806033804241 / 2500000000000000000000)

theorem Zeta5Irrational.U_543_8 : Uω (aρ 8) (bρ 8) (7938190348099 / 12800000000000) ≤ -(830431005173728875531 / 1250000000000000000000)

theorem Zeta5Irrational.U_543_9 : Uω (aρ 9) (bρ 9) (7938190348099 / 12800000000000) ≤ -(3712741836837896895691 / 5000000000000000000000)

theorem Zeta5Irrational.U_543_10 : Uω (aρ 10) (bρ 10) (7938190348099 / 12800000000000) ≤ -(2115612269099813192683 / 2500000000000000000000)

theorem Zeta5Irrational.U_543_11 : Uω (aρ 11) (bρ 11) (7938190348099 / 12800000000000) ≤ -(4921683813520243516333 / 5000000000000000000000)

theorem Zeta5Irrational.U_543_12 : Uω (aρ 12) (bρ 12) (7938190348099 / 12800000000000) ≤ -(11759862056280220014139 / 10000000000000000000000)

theorem Zeta5Irrational.U_543_13 : Uω (aρ 13) (bρ 13) (7938190348099 / 12800000000000) ≤ -(7500473685979014998829 / 5000000000000000000000)

theorem Zeta5Irrational.U_543_14 : Uω (aρ 14) (bρ 14) (7938190348099 / 12800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_543_15 : Uω (aρ 15) (bρ 15) (7938190348099 / 12800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_543_16 : Uω (aρ 16) (bρ 16) (7938190348099 / 12800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_543 : Uρ (7938190348099 / 12800000000000) ≤ -(494466032119251637601 / 625000000000000000000)