Certified arcsine potential bounds (U22)

theorem Zeta5Irrational.U_268_1 : Uω (aρ 1) (bρ 1) (1430381373231 / 6400000000000) ≤ -(7638369915361229297179 / 5000000000000000000000)

theorem Zeta5Irrational.U_268_2 : Uω (aρ 2) (bρ 2) (1430381373231 / 6400000000000) ≤ -(7694407190984975856153 / 5000000000000000000000)

theorem Zeta5Irrational.U_268_3 : Uω (aρ 3) (bρ 3) (1430381373231 / 6400000000000) ≤ -(3123634910807985488307 / 2000000000000000000000)

theorem Zeta5Irrational.U_268_4 : Uω (aρ 4) (bρ 4) (1430381373231 / 6400000000000) ≤ -(16015712693712828402873 / 10000000000000000000000)

theorem Zeta5Irrational.U_268_5 : Uω (aρ 5) (bρ 5) (1430381373231 / 6400000000000) ≤ -(16666826535024517328497 / 10000000000000000000000)

theorem Zeta5Irrational.U_268_6 : Uω (aρ 6) (bρ 6) (1430381373231 / 6400000000000) ≤ -(8861319087358917193727 / 5000000000000000000000)

theorem Zeta5Irrational.U_268_7 : Uω (aρ 7) (bρ 7) (1430381373231 / 6400000000000) ≤ -(1951475193735104412929 / 1000000000000000000000)

theorem Zeta5Irrational.U_268_8 : Uω (aρ 8) (bρ 8) (1430381373231 / 6400000000000) ≤ -(23353858451496383736881 / 10000000000000000000000)

theorem Zeta5Irrational.U_268_9 : Uω (aρ 9) (bρ 9) (1430381373231 / 6400000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_268_10 : Uω (aρ 10) (bρ 10) (1430381373231 / 6400000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_268_11 : Uω (aρ 11) (bρ 11) (1430381373231 / 6400000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_268_12 : Uω (aρ 12) (bρ 12) (1430381373231 / 6400000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_268_13 : Uω (aρ 13) (bρ 13) (1430381373231 / 6400000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_268 : Uρ (1430381373231 / 6400000000000) ≤ -(18700808222836457915203 / 10000000000000000000000)

theorem Zeta5Irrational.U_269_1 : Uω (aρ 1) (bρ 1) (14337933849397 / 64000000000000) ≤ -(7626102786438175269679 / 5000000000000000000000)

theorem Zeta5Irrational.U_269_2 : Uω (aρ 2) (bρ 2) (14337933849397 / 64000000000000) ≤ -(7681999553831932135529 / 5000000000000000000000)

theorem Zeta5Irrational.U_269_3 : Uω (aρ 3) (bρ 3) (14337933849397 / 64000000000000) ≤ -(7796384408299785382657 / 5000000000000000000000)

theorem Zeta5Irrational.U_269_4 : Uω (aρ 4) (bρ 4) (14337933849397 / 64000000000000) ≤ -(7994615924007200057329 / 5000000000000000000000)

theorem Zeta5Irrational.U_269_5 : Uω (aρ 5) (bρ 5) (14337933849397 / 64000000000000) ≤ -(16638428417119872482403 / 10000000000000000000000)

theorem Zeta5Irrational.U_269_6 : Uω (aρ 6) (bρ 6) (14337933849397 / 64000000000000) ≤ -(3538128136498892697533 / 2000000000000000000000)

theorem Zeta5Irrational.U_269_7 : Uω (aρ 7) (bρ 7) (14337933849397 / 64000000000000) ≤ -(4868684798127873941503 / 2500000000000000000000)

theorem Zeta5Irrational.U_269_8 : Uω (aρ 8) (bρ 8) (14337933849397 / 64000000000000) ≤ -(23278948388726262110201 / 10000000000000000000000)

theorem Zeta5Irrational.U_269_9 : Uω (aρ 9) (bρ 9) (14337933849397 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_269_10 : Uω (aρ 10) (bρ 10) (14337933849397 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_269_11 : Uω (aρ 11) (bρ 11) (14337933849397 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_269_12 : Uω (aρ 12) (bρ 12) (14337933849397 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_269_13 : Uω (aρ 13) (bρ 13) (14337933849397 / 64000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_269 : Uρ (14337933849397 / 64000000000000) ≤ -(3736537088496720148241 / 2000000000000000000000)

theorem Zeta5Irrational.U_270_1 : Uω (aρ 1) (bρ 1) (3593013491621 / 16000000000000) ≤ -(15227731364814907513837 / 10000000000000000000000)

theorem Zeta5Irrational.U_270_2 : Uω (aρ 2) (bρ 2) (3593013491621 / 16000000000000) ≤ -(7669622644416340882011 / 5000000000000000000000)

theorem Zeta5Irrational.U_270_3 : Uω (aρ 3) (bρ 3) (3593013491621 / 16000000000000) ≤ -(15567427568303136711517 / 10000000000000000000000)

theorem Zeta5Irrational.U_270_4 : Uω (aρ 4) (bρ 4) (3593013491621 / 16000000000000) ≤ -(7981410650442638429787 / 5000000000000000000000)

theorem Zeta5Irrational.U_270_5 : Uω (aρ 5) (bρ 5) (3593013491621 / 16000000000000) ≤ -(16610111915455838225121 / 10000000000000000000000)

theorem Zeta5Irrational.U_270_6 : Uω (aρ 6) (bρ 6) (3593013491621 / 16000000000000) ≤ -(17658749634887927061711 / 10000000000000000000000)

theorem Zeta5Irrational.U_270_7 : Uω (aρ 7) (bρ 7) (3593013491621 / 16000000000000) ≤ -(9717453763183694041361 / 5000000000000000000000)

theorem Zeta5Irrational.U_270_8 : Uω (aρ 8) (bρ 8) (3593013491621 / 16000000000000) ≤ -(5801248140116723696391 / 2500000000000000000000)

theorem Zeta5Irrational.U_270_9 : Uω (aρ 9) (bρ 9) (3593013491621 / 16000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_270_10 : Uω (aρ 10) (bρ 10) (3593013491621 / 16000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_270_11 : Uω (aρ 11) (bρ 11) (3593013491621 / 16000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_270_12 : Uω (aρ 12) (bρ 12) (3593013491621 / 16000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_270_13 : Uω (aρ 13) (bρ 13) (3593013491621 / 16000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_270 : Uρ (3593013491621 / 16000000000000) ≤ -(2333085713962513780869 / 1250000000000000000000)

theorem Zeta5Irrational.U_271_1 : Uω (aρ 1) (bρ 1) (14406174083571 / 64000000000000) ≤ -(7601658456640705685281 / 5000000000000000000000)

theorem Zeta5Irrational.U_271_2 : Uω (aρ 2) (bρ 2) (14406174083571 / 64000000000000) ≤ -(15314552621698947647151 / 10000000000000000000000)

theorem Zeta5Irrational.U_271_3 : Uω (aρ 3) (bρ 3) (14406174083571 / 64000000000000) ≤ -(7771075241021788038101 / 5000000000000000000000)

theorem Zeta5Irrational.U_271_4 : Uω (aρ 4) (bρ 4) (14406174083571 / 64000000000000) ≤ -(15936480678178473697243 / 10000000000000000000000)

theorem Zeta5Irrational.U_271_5 : Uω (aρ 5) (bρ 5) (14406174083571 / 64000000000000) ≤ -(103636728471640727917 / 62500000000000000000)

theorem Zeta5Irrational.U_271_6 : Uω (aρ 6) (bρ 6) (14406174083571 / 64000000000000) ≤ -(17626964297738276232173 / 10000000000000000000000)

theorem Zeta5Irrational.U_271_7 : Uω (aρ 7) (bρ 7) (14406174083571 / 64000000000000) ≤ -(9697627563002555907191 / 5000000000000000000000)

theorem Zeta5Irrational.U_271_8 : Uω (aρ 8) (bρ 8) (14406174083571 / 64000000000000) ≤ -(23131959300184916443993 / 10000000000000000000000)

theorem Zeta5Irrational.U_271_9 : Uω (aρ 9) (bρ 9) (14406174083571 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_271_10 : Uω (aρ 10) (bρ 10) (14406174083571 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_271_11 : Uω (aρ 11) (bρ 11) (14406174083571 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_271_12 : Uω (aρ 12) (bρ 12) (14406174083571 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_271_13 : Uω (aρ 13) (bρ 13) (14406174083571 / 64000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_271 : Uρ (14406174083571 / 64000000000000) ≤ -(18646805938925348800429 / 10000000000000000000000)

theorem Zeta5Irrational.U_272_1 : Uω (aρ 1) (bρ 1) (7220147100329 / 32000000000000) ≤ -(15178961927162266424097 / 10000000000000000000000)

theorem Zeta5Irrational.U_272_2 : Uω (aρ 2) (bρ 2) (7220147100329 / 32000000000000) ≤ -(1528992080473304163929 / 1000000000000000000000)

theorem Zeta5Irrational.U_272_3 : Uω (aρ 3) (bρ 3) (7220147100329 / 32000000000000) ≤ -(3879234308300097326093 / 2500000000000000000000)

theorem Zeta5Irrational.U_272_4 : Uω (aρ 4) (bρ 4) (7220147100329 / 32000000000000) ≤ -(15910209608740880248149 / 10000000000000000000000)

theorem Zeta5Irrational.U_272_5 : Uω (aρ 5) (bρ 5) (7220147100329 / 32000000000000) ≤ -(16553721866754159805869 / 10000000000000000000000)

theorem Zeta5Irrational.U_272_6 : Uω (aρ 6) (bρ 6) (7220147100329 / 32000000000000) ≤ -(54985262327256662747 / 31250000000000000000)

theorem Zeta5Irrational.U_272_7 : Uω (aρ 7) (bρ 7) (7220147100329 / 32000000000000) ≤ -(19355780207743348837579 / 10000000000000000000000)

theorem Zeta5Irrational.U_272_8 : Uω (aρ 8) (bρ 8) (7220147100329 / 32000000000000) ≤ -(23059818675209941582027 / 10000000000000000000000)

theorem Zeta5Irrational.U_272_9 : Uω (aρ 9) (bρ 9) (7220147100329 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_272_10 : Uω (aρ 10) (bρ 10) (7220147100329 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_272_11 : Uω (aρ 11) (bρ 11) (7220147100329 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_272_12 : Uω (aρ 12) (bρ 12) (7220147100329 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_272_13 : Uω (aρ 13) (bρ 13) (7220147100329 / 32000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_272 : Uρ (7220147100329 / 32000000000000) ≤ -(9314521594811334388811 / 5000000000000000000000)

theorem Zeta5Irrational.U_273_1 : Uω (aρ 1) (bρ 1) (2894882863549 / 12800000000000) ≤ -(15154666117466165170289 / 10000000000000000000000)

theorem Zeta5Irrational.U_273_2 : Uω (aρ 2) (bρ 2) (2894882863549 / 12800000000000) ≤ -(3816337384657765063509 / 2500000000000000000000)

theorem Zeta5Irrational.U_273_3 : Uω (aρ 3) (bρ 3) (2894882863549 / 12800000000000) ≤ -(7745893749807219680829 / 5000000000000000000000)

theorem Zeta5Irrational.U_273_4 : Uω (aρ 4) (bρ 4) (2894882863549 / 12800000000000) ≤ -(15884007724381241620549 / 10000000000000000000000)

theorem Zeta5Irrational.U_273_5 : Uω (aρ 5) (bρ 5) (2894882863549 / 12800000000000) ≤ -(4131411845769879803169 / 2500000000000000000000)

theorem Zeta5Irrational.U_273_6 : Uω (aρ 6) (bρ 6) (2894882863549 / 12800000000000) ≤ -(4390926964309566989123 / 2500000000000000000000)

theorem Zeta5Irrational.U_273_7 : Uω (aρ 7) (bρ 7) (2894882863549 / 12800000000000) ≤ -(9658240508237714690711 / 5000000000000000000000)

theorem Zeta5Irrational.U_273_8 : Uω (aρ 8) (bρ 8) (2894882863549 / 12800000000000) ≤ -(22988542356000148652769 / 10000000000000000000000)

theorem Zeta5Irrational.U_273_9 : Uω (aρ 9) (bρ 9) (2894882863549 / 12800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_273_10 : Uω (aρ 10) (bρ 10) (2894882863549 / 12800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_273_11 : Uω (aρ 11) (bρ 11) (2894882863549 / 12800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_273_12 : Uω (aρ 12) (bρ 12) (2894882863549 / 12800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_273_13 : Uω (aρ 13) (bρ 13) (2894882863549 / 12800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_273 : Uρ (2894882863549 / 12800000000000) ≤ -(9305697337325464503709 / 5000000000000000000000)

theorem Zeta5Irrational.U_274_1 : Uω (aρ 1) (bρ 1) (906783402177 / 4000000000000) ≤ -(15130429197303497441467 / 10000000000000000000000)

theorem Zeta5Irrational.U_274_2 : Uω (aρ 2) (bρ 2) (906783402177 / 4000000000000) ≤ -(15240838526292947970749 / 10000000000000000000000)

theorem Zeta5Irrational.U_274_3 : Uω (aρ 3) (bρ 3) (906783402177 / 4000000000000) ≤ -(3866675240390775093581 / 2500000000000000000000)

theorem Zeta5Irrational.U_274_4 : Uω (aρ 4) (bρ 4) (906783402177 / 4000000000000) ≤ -(15857874659838571656279 / 10000000000000000000000)

theorem Zeta5Irrational.U_274_5 : Uω (aρ 5) (bρ 5) (906783402177 / 4000000000000) ≤ -(6444395563387845643 / 3906250000000000000)

theorem Zeta5Irrational.U_274_6 : Uω (aρ 6) (bρ 6) (906783402177 / 4000000000000) ≤ -(17532235324295299403419 / 10000000000000000000000)

theorem Zeta5Irrational.U_274_7 : Uω (aρ 7) (bρ 7) (906783402177 / 4000000000000) ≤ -(4819338956257651832129 / 2500000000000000000000)

theorem Zeta5Irrational.U_274_8 : Uω (aρ 8) (bρ 8) (906783402177 / 4000000000000) ≤ -(11459051748918678550413 / 5000000000000000000000)

theorem Zeta5Irrational.U_274_9 : Uω (aρ 9) (bρ 9) (906783402177 / 4000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_274_10 : Uω (aρ 10) (bρ 10) (906783402177 / 4000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_274_11 : Uω (aρ 11) (bρ 11) (906783402177 / 4000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_274_12 : Uω (aρ 12) (bρ 12) (906783402177 / 4000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_274_13 : Uω (aρ 13) (bρ 13) (906783402177 / 4000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_274 : Uρ (906783402177 / 4000000000000) ≤ -(9296928869868299308561 / 5000000000000000000000)

theorem Zeta5Irrational.U_275_1 : Uω (aρ 1) (bρ 1) (14542654551919 / 64000000000000) ≤ -(15106250881866031193979 / 10000000000000000000000)

theorem Zeta5Irrational.U_275_2 : Uω (aρ 2) (bρ 2) (14542654551919 / 64000000000000) ≤ -(15216387472800909762541 / 10000000000000000000000)

theorem Zeta5Irrational.U_275_3 : Uω (aρ 3) (bρ 3) (14542654551919 / 64000000000000) ≤ -(15441677301735706487299 / 10000000000000000000000)

theorem Zeta5Irrational.U_275_4 : Uω (aρ 4) (bρ 4) (14542654551919 / 64000000000000) ≤ -(633272402110040347591 / 400000000000000000000)

theorem Zeta5Irrational.U_275_5 : Uω (aρ 5) (bρ 5) (14542654551919 / 64000000000000) ≤ -(8234868593102955975117 / 5000000000000000000000)

theorem Zeta5Irrational.U_275_6 : Uω (aρ 6) (bρ 6) (14542654551919 / 64000000000000) ≤ -(17500865642401456087003 / 10000000000000000000000)

theorem Zeta5Irrational.U_275_7 : Uω (aρ 7) (bρ 7) (14542654551919 / 64000000000000) ≤ -(384768058671075131277 / 200000000000000000000)

theorem Zeta5Irrational.U_275_8 : Uω (aρ 8) (bρ 8) (14542654551919 / 64000000000000) ≤ -(22848476633536171818119 / 10000000000000000000000)

theorem Zeta5Irrational.U_275_9 : Uω (aρ 9) (bρ 9) (14542654551919 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_275_10 : Uω (aρ 10) (bρ 10) (14542654551919 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_275_11 : Uω (aρ 11) (bρ 11) (14542654551919 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_275_12 : Uω (aρ 12) (bρ 12) (14542654551919 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_275_13 : Uω (aρ 13) (bρ 13) (14542654551919 / 64000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_275 : Uρ (14542654551919 / 64000000000000) ≤ -(290256716498770197431 / 156250000000000000000)

theorem Zeta5Irrational.U_276_1 : Uω (aρ 1) (bρ 1) (7288387334503 / 32000000000000) ≤ -(1508213088840681581873 / 1000000000000000000000)

theorem Zeta5Irrational.U_276_2 : Uω (aρ 2) (bρ 2) (7288387334503 / 32000000000000) ≤ -(15191996085398068846649 / 10000000000000000000000)

theorem Zeta5Irrational.U_276_3 : Uω (aρ 3) (bρ 3) (7288387334503 / 32000000000000) ≤ -(3854179051302327034767 / 2500000000000000000000)

theorem Zeta5Irrational.U_276_4 : Uω (aρ 4) (bρ 4) (7288387334503 / 32000000000000) ≤ -(1975726692953131972251 / 1250000000000000000000)

theorem Zeta5Irrational.U_276_5 : Uω (aρ 5) (bρ 5) (7288387334503 / 32000000000000) ≤ -(328838011214802240827 / 200000000000000000000)

theorem Zeta5Irrational.U_276_6 : Uω (aρ 6) (bρ 6) (7288387334503 / 32000000000000) ≤ -(17469598115456413670451 / 10000000000000000000000)

theorem Zeta5Irrational.U_276_7 : Uω (aρ 7) (bρ 7) (7288387334503 / 32000000000000) ≤ -(3839924133780546951883 / 2000000000000000000000)

theorem Zeta5Irrational.U_276_8 : Uω (aρ 8) (bρ 8) (7288387334503 / 32000000000000) ≤ -(2277963757593818057009 / 1000000000000000000000)

theorem Zeta5Irrational.U_276_9 : Uω (aρ 9) (bρ 9) (7288387334503 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_276_10 : Uω (aρ 10) (bρ 10) (7288387334503 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_276_11 : Uω (aρ 11) (bρ 11) (7288387334503 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_276_12 : Uω (aρ 12) (bρ 12) (7288387334503 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_276_13 : Uω (aρ 13) (bρ 13) (7288387334503 / 32000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_276 : Uρ (7288387334503 / 32000000000000) ≤ -(4639777152719005169681 / 2500000000000000000000)

theorem Zeta5Irrational.U_277_1 : Uω (aρ 1) (bρ 1) (732250745159 / 3200000000000) ≤ -(15034064746622953868251 / 10000000000000000000000)

theorem Zeta5Irrational.U_277_2 : Uω (aρ 2) (bρ 2) (732250745159 / 3200000000000) ≤ -(3028678229702195023461 / 2000000000000000000000)

theorem Zeta5Irrational.U_277_3 : Uω (aρ 3) (bρ 3) (732250745159 / 3200000000000) ≤ -(384174511354075211361 / 250000000000000000000)

theorem Zeta5Irrational.U_277_4 : Uω (aρ 4) (bρ 4) (732250745159 / 3200000000000) ≤ -(7877011697722102677853 / 5000000000000000000000)

theorem Zeta5Irrational.U_277_5 : Uω (aρ 5) (bρ 5) (732250745159 / 3200000000000) ≤ -(4096615501181864826651 / 2500000000000000000000)

theorem Zeta5Irrational.U_277_6 : Uω (aρ 6) (bρ 6) (732250745159 / 3200000000000) ≤ -(870368338916667326583 / 500000000000000000000)

theorem Zeta5Irrational.U_277_7 : Uω (aρ 7) (bρ 7) (732250745159 / 3200000000000) ≤ -(9561280728788798957347 / 5000000000000000000000)

theorem Zeta5Irrational.U_277_8 : Uω (aρ 8) (bρ 8) (732250745159 / 3200000000000) ≤ -(11322116003695119553231 / 5000000000000000000000)

theorem Zeta5Irrational.U_277_9 : Uω (aρ 9) (bρ 9) (732250745159 / 3200000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_277_10 : Uω (aρ 10) (bρ 10) (732250745159 / 3200000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_277_11 : Uω (aρ 11) (bρ 11) (732250745159 / 3200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_277_12 : Uω (aρ 12) (bρ 12) (732250745159 / 3200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_277_13 : Uω (aρ 13) (bρ 13) (732250745159 / 3200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_277_14 : Uω (aρ 14) (bρ 14) (732250745159 / 3200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_277_15 : Uω (aρ 15) (bρ 15) (732250745159 / 3200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_277_16 : Uω (aρ 16) (bρ 16) (732250745159 / 3200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_277 : Uρ (732250745159 / 3200000000000) ≤ -(4631194231033519735309 / 2500000000000000000000)

theorem Zeta5Irrational.U_278_1 : Uω (aρ 1) (bρ 1) (7356627568677 / 32000000000000) ≤ -(14986228550453869444753 / 10000000000000000000000)

theorem Zeta5Irrational.U_278_2 : Uω (aρ 2) (bρ 2) (7356627568677 / 32000000000000) ≤ -(7547510708000491888651 / 5000000000000000000000)

theorem Zeta5Irrational.U_278_3 : Uω (aρ 3) (bρ 3) (7356627568677 / 32000000000000) ≤ -(7658745617946492467501 / 5000000000000000000000)

theorem Zeta5Irrational.U_278_4 : Uω (aρ 4) (bρ 4) (7356627568677 / 32000000000000) ≤ -(3140500279114518294383 / 2000000000000000000000)

theorem Zeta5Irrational.U_278_5 : Uω (aρ 5) (bρ 5) (7356627568677 / 32000000000000) ≤ -(16331333419163968740737 / 10000000000000000000000)

theorem Zeta5Irrational.U_278_6 : Uω (aρ 6) (bρ 6) (7356627568677 / 32000000000000) ≤ -(17345535887965030851513 / 10000000000000000000000)

theorem Zeta5Irrational.U_278_7 : Uω (aρ 7) (bρ 7) (7356627568677 / 32000000000000) ≤ -(761846612733371790459 / 400000000000000000000)

theorem Zeta5Irrational.U_278_8 : Uω (aρ 8) (bρ 8) (7356627568677 / 32000000000000) ≤ -(4502343141899525609949 / 2000000000000000000000)

theorem Zeta5Irrational.U_278_9 : Uω (aρ 9) (bρ 9) (7356627568677 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_278_10 : Uω (aρ 10) (bρ 10) (7356627568677 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_278_11 : Uω (aρ 11) (bρ 11) (7356627568677 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_278_12 : Uω (aρ 12) (bρ 12) (7356627568677 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_278_13 : Uω (aρ 13) (bρ 13) (7356627568677 / 32000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_278 : Uρ (7356627568677 / 32000000000000) ≤ -(2311355678676694845457 / 1250000000000000000000)

theorem Zeta5Irrational.U_279_1 : Uω (aρ 1) (bρ 1) (1847686921441 / 8000000000000) ≤ -(746931005506826067739 / 500000000000000000000)

theorem Zeta5Irrational.U_279_2 : Uω (aρ 2) (bρ 2) (1847686921441 / 8000000000000) ≤ -(150468846214901381899 / 100000000000000000000)

theorem Zeta5Irrational.U_279_3 : Uω (aρ 3) (bρ 3) (1847686921441 / 8000000000000) ≤ -(7634123057285258519997 / 5000000000000000000000)

theorem Zeta5Irrational.U_279_4 : Uω (aρ 4) (bρ 4) (1847686921441 / 8000000000000) ≤ -(3130248953656063937241 / 2000000000000000000000)

theorem Zeta5Irrational.U_279_5 : Uω (aρ 5) (bρ 5) (1847686921441 / 8000000000000) ≤ -(16276511309893494333811 / 10000000000000000000000)

theorem Zeta5Irrational.U_279_6 : Uω (aρ 6) (bρ 6) (1847686921441 / 8000000000000) ≤ -(17284100131055428922333 / 10000000000000000000000)

theorem Zeta5Irrational.U_279_7 : Uω (aρ 7) (bρ 7) (1847686921441 / 8000000000000) ≤ -(9485209885025233626713 / 5000000000000000000000)

theorem Zeta5Irrational.U_279_8 : Uω (aρ 8) (bρ 8) (1847686921441 / 8000000000000) ≤ -(11190966569279896228593 / 5000000000000000000000)

theorem Zeta5Irrational.U_279_9 : Uω (aρ 9) (bρ 9) (1847686921441 / 8000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_279_10 : Uω (aρ 10) (bρ 10) (1847686921441 / 8000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_279_11 : Uω (aρ 11) (bρ 11) (1847686921441 / 8000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_279_12 : Uω (aρ 12) (bρ 12) (1847686921441 / 8000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_279_13 : Uω (aρ 13) (bρ 13) (1847686921441 / 8000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_279_14 : Uω (aρ 14) (bρ 14) (1847686921441 / 8000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_279_15 : Uω (aρ 15) (bρ 15) (1847686921441 / 8000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_279_16 : Uω (aρ 16) (bρ 16) (1847686921441 / 8000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_279 : Uρ (1847686921441 / 8000000000000) ≤ -(1153581143868500307221 / 625000000000000000000)