Certified arcsine potential bounds (U33)

theorem Zeta5Irrational.U_400_1 : Uω (aρ 1) (bρ 1) (12864925888431 / 32000000000000) ≤ -(9274145591088656349597 / 10000000000000000000000)

theorem Zeta5Irrational.U_400_2 : Uω (aρ 2) (bρ 2) (12864925888431 / 32000000000000) ≤ -(145859318811119573189 / 156250000000000000000)

theorem Zeta5Irrational.U_400_3 : Uω (aρ 3) (bρ 3) (12864925888431 / 32000000000000) ≤ -(9458033394948477753999 / 10000000000000000000000)

theorem Zeta5Irrational.U_400_4 : Uω (aρ 4) (bρ 4) (12864925888431 / 32000000000000) ≤ -(4833229095758892645243 / 5000000000000000000000)

theorem Zeta5Irrational.U_400_5 : Uω (aρ 5) (bρ 5) (12864925888431 / 32000000000000) ≤ -(9994254414217391606101 / 10000000000000000000000)

theorem Zeta5Irrational.U_400_6 : Uω (aρ 6) (bρ 6) (12864925888431 / 32000000000000) ≤ -(10488546692852194258217 / 10000000000000000000000)

theorem Zeta5Irrational.U_400_7 : Uω (aρ 7) (bρ 7) (12864925888431 / 32000000000000) ≤ -(2804114770301443257797 / 2500000000000000000000)

theorem Zeta5Irrational.U_400_8 : Uω (aρ 8) (bρ 8) (12864925888431 / 32000000000000) ≤ -(12284230347491191553647 / 10000000000000000000000)

theorem Zeta5Irrational.U_400_9 : Uω (aρ 9) (bρ 9) (12864925888431 / 32000000000000) ≤ -(6949648283068307006159 / 5000000000000000000000)

theorem Zeta5Irrational.U_400_10 : Uω (aρ 10) (bρ 10) (12864925888431 / 32000000000000) ≤ -(16686293334959350296841 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_400 : Uρ (12864925888431 / 32000000000000) ≤ -(6646107995395590288459 / 5000000000000000000000)

theorem Zeta5Irrational.U_401_1 : Uω (aρ 1) (bρ 1) (1294864303869 / 3200000000000) ≤ -(2302056756254861910491 / 2500000000000000000000)

theorem Zeta5Irrational.U_401_2 : Uω (aρ 2) (bρ 2) (1294864303869 / 3200000000000) ≤ -(1853734599609437634619 / 2000000000000000000000)

theorem Zeta5Irrational.U_401_3 : Uω (aρ 3) (bρ 3) (1294864303869 / 3200000000000) ≤ -(4695439966694920649199 / 5000000000000000000000)

theorem Zeta5Irrational.U_401_4 : Uω (aρ 4) (bρ 4) (1294864303869 / 3200000000000) ≤ -(9597862507636789230839 / 10000000000000000000000)

theorem Zeta5Irrational.U_401_5 : Uω (aρ 5) (bρ 5) (1294864303869 / 3200000000000) ≤ -(1240411754096010472283 / 1250000000000000000000)

theorem Zeta5Irrational.U_401_6 : Uω (aρ 6) (bρ 6) (1294864303869 / 3200000000000) ≤ -(1301722415710541881821 / 1250000000000000000000)

theorem Zeta5Irrational.U_401_7 : Uω (aρ 7) (bρ 7) (1294864303869 / 3200000000000) ≤ -(5567744317910864751661 / 5000000000000000000000)

theorem Zeta5Irrational.U_401_8 : Uω (aρ 8) (bρ 8) (1294864303869 / 3200000000000) ≤ -(12192603200744992393569 / 10000000000000000000000)

theorem Zeta5Irrational.U_401_9 : Uω (aρ 9) (bρ 9) (1294864303869 / 3200000000000) ≤ -(13786735457843431653397 / 10000000000000000000000)

theorem Zeta5Irrational.U_401_10 : Uω (aρ 10) (bρ 10) (1294864303869 / 3200000000000) ≤ -(16512559890281452104139 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_401 : Uρ (1294864303869 / 3200000000000) ≤ -(13232137085469873442083 / 10000000000000000000000)

theorem Zeta5Irrational.U_402_1 : Uω (aρ 1) (bρ 1) (13032360188949 / 32000000000000) ≤ -(2285685037350096200439 / 2500000000000000000000)

theorem Zeta5Irrational.U_402_2 : Uω (aρ 2) (bρ 2) (13032360188949 / 32000000000000) ≤ -(4601393316889063213119 / 5000000000000000000000)

theorem Zeta5Irrational.U_402_3 : Uω (aρ 3) (bρ 3) (13032360188949 / 32000000000000) ≤ -(4662087319745159335967 / 5000000000000000000000)

theorem Zeta5Irrational.U_402_4 : Uω (aρ 4) (bρ 4) (13032360188949 / 32000000000000) ≤ -(1191216852877995912977 / 1250000000000000000000)

theorem Zeta5Irrational.U_402_5 : Uω (aρ 5) (bρ 5) (13032360188949 / 32000000000000) ≤ -(9852835570745593329249 / 10000000000000000000000)

theorem Zeta5Irrational.U_402_6 : Uω (aρ 6) (bρ 6) (13032360188949 / 32000000000000) ≤ -(10339572280256983547971 / 10000000000000000000000)

theorem Zeta5Irrational.U_402_7 : Uω (aρ 7) (bρ 7) (13032360188949 / 32000000000000) ≤ -(690949015699183907021 / 625000000000000000000)

theorem Zeta5Irrational.U_402_8 : Uω (aρ 8) (bρ 8) (13032360188949 / 32000000000000) ≤ -(12101857029900682044303 / 10000000000000000000000)

theorem Zeta5Irrational.U_402_9 : Uω (aρ 9) (bρ 9) (13032360188949 / 32000000000000) ≤ -(6837808690690216867231 / 5000000000000000000000)

theorem Zeta5Irrational.U_402_10 : Uω (aρ 10) (bρ 10) (13032360188949 / 32000000000000) ≤ -(2042910051658331651807 / 1250000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_402 : Uρ (13032360188949 / 32000000000000) ≤ -(13172843436669313561171 / 10000000000000000000000)

theorem Zeta5Irrational.U_403_1 : Uω (aρ 1) (bρ 1) (1639509667401 / 4000000000000) ≤ -(9077679346739136303621 / 10000000000000000000000)

theorem Zeta5Irrational.U_403_2 : Uω (aρ 2) (bρ 2) (1639509667401 / 4000000000000) ≤ -(2284332897053214077443 / 2500000000000000000000)

theorem Zeta5Irrational.U_403_3 : Uω (aρ 3) (bρ 3) (1639509667401 / 4000000000000) ≤ -(4628955784060132778483 / 5000000000000000000000)

theorem Zeta5Irrational.U_403_4 : Uω (aρ 4) (bρ 4) (1639509667401 / 4000000000000) ≤ -(9462068786104314284357 / 10000000000000000000000)

theorem Zeta5Irrational.U_403_5 : Uω (aρ 5) (bρ 5) (1639509667401 / 4000000000000) ≤ -(4891435975477487785923 / 5000000000000000000000)

theorem Zeta5Irrational.U_403_6 : Uω (aρ 6) (bρ 6) (1639509667401 / 4000000000000) ≤ -(10265917141164475357851 / 10000000000000000000000)

theorem Zeta5Irrational.U_403_7 : Uω (aρ 7) (bρ 7) (1639509667401 / 4000000000000) ≤ -(1371941851203687294137 / 1250000000000000000000)

theorem Zeta5Irrational.U_403_8 : Uω (aρ 8) (bρ 8) (1639509667401 / 4000000000000) ≤ -(12011974165207489099981 / 10000000000000000000000)

theorem Zeta5Irrational.U_403_9 : Uω (aρ 9) (bρ 9) (1639509667401 / 4000000000000) ≤ -(1695737679398358110773 / 1250000000000000000000)

theorem Zeta5Irrational.U_403_10 : Uω (aρ 10) (bρ 10) (1639509667401 / 4000000000000) ≤ -(647126960665450513509 / 400000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_403 : Uρ (1639509667401 / 4000000000000) ≤ -(3278575728550199324133 / 2500000000000000000000)

theorem Zeta5Irrational.U_404_1 : Uω (aρ 1) (bρ 1) (6641755819863 / 16000000000000) ≤ -(8948814032234249353119 / 10000000000000000000000)

theorem Zeta5Irrational.U_404_2 : Uω (aρ 2) (bρ 2) (6641755819863 / 16000000000000) ≤ -(1125961639650166118421 / 1250000000000000000000)

theorem Zeta5Irrational.U_404_3 : Uω (aρ 3) (bρ 3) (6641755819863 / 16000000000000) ≤ -(456334444861630339123 / 500000000000000000000)

theorem Zeta5Irrational.U_404_4 : Uω (aρ 4) (bρ 4) (6641755819863 / 16000000000000) ≤ -(9328096888636753907783 / 10000000000000000000000)

theorem Zeta5Irrational.U_404_5 : Uω (aρ 5) (bρ 5) (6641755819863 / 16000000000000) ≤ -(2411100417759986548877 / 2500000000000000000000)

theorem Zeta5Irrational.U_404_6 : Uω (aρ 6) (bρ 6) (6641755819863 / 16000000000000) ≤ -(5060114932047977894949 / 5000000000000000000000)

theorem Zeta5Irrational.U_404_7 : Uω (aρ 7) (bρ 7) (6641755819863 / 16000000000000) ≤ -(10818157684744796127839 / 10000000000000000000000)

theorem Zeta5Irrational.U_404_8 : Uω (aρ 8) (bρ 8) (6641755819863 / 16000000000000) ≤ -(5917365200118181528387 / 5000000000000000000000)

theorem Zeta5Irrational.U_404_9 : Uω (aρ 9) (bρ 9) (6641755819863 / 16000000000000) ≤ -(3337630368056965153349 / 2500000000000000000000)

theorem Zeta5Irrational.U_404_10 : Uω (aρ 10) (bρ 10) (6641755819863 / 16000000000000) ≤ -(15859495990828664169851 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_404 : Uρ (6641755819863 / 16000000000000) ≤ -(3249841497956135963179 / 2500000000000000000000)

theorem Zeta5Irrational.U_405_1 : Uω (aρ 1) (bρ 1) (3362736485061 / 8000000000000) ≤ -(2205397067664007022223 / 2500000000000000000000)

theorem Zeta5Irrational.U_405_2 : Uω (aρ 2) (bρ 2) (3362736485061 / 8000000000000) ≤ -(4439856992194217320277 / 5000000000000000000000)

theorem Zeta5Irrational.U_405_3 : Uω (aρ 3) (bρ 3) (3362736485061 / 8000000000000) ≤ -(2249291664094980362187 / 2500000000000000000000)

theorem Zeta5Irrational.U_405_4 : Uω (aρ 4) (bρ 4) (3362736485061 / 8000000000000) ≤ -(143685914272745119657 / 156250000000000000000)

theorem Zeta5Irrational.U_405_5 : Uω (aρ 5) (bρ 5) (3362736485061 / 8000000000000) ≤ -(4753914742488689626759 / 5000000000000000000000)

theorem Zeta5Irrational.U_405_6 : Uω (aρ 6) (bρ 6) (3362736485061 / 8000000000000) ≤ -(2494163466899750630607 / 2500000000000000000000)

theorem Zeta5Irrational.U_405_7 : Uω (aρ 7) (bρ 7) (3362736485061 / 8000000000000) ≤ -(2665818446664646446537 / 2500000000000000000000)

theorem Zeta5Irrational.U_405_8 : Uω (aρ 8) (bρ 8) (3362736485061 / 8000000000000) ≤ -(11660741129451976871839 / 10000000000000000000000)

theorem Zeta5Irrational.U_405_9 : Uω (aρ 9) (bρ 9) (3362736485061 / 8000000000000) ≤ -(13140303395378854275257 / 10000000000000000000000)

theorem Zeta5Irrational.U_405_10 : Uω (aρ 10) (bρ 10) (3362736485061 / 8000000000000) ≤ -(1555478437684198579321 / 1000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_405 : Uρ (3362736485061 / 8000000000000) ≤ -(12887117814147303746673 / 10000000000000000000000)

theorem Zeta5Irrational.U_406_1 : Uω (aρ 1) (bρ 1) (6809190120381 / 16000000000000) ≤ -(8695960864778360946079 / 10000000000000000000000)

theorem Zeta5Irrational.U_406_2 : Uω (aρ 2) (bρ 2) (6809190120381 / 16000000000000) ≤ -(4376676121341284168073 / 5000000000000000000000)

theorem Zeta5Irrational.U_406_3 : Uω (aρ 3) (bρ 3) (6809190120381 / 16000000000000) ≤ -(2217325329992838613491 / 2500000000000000000000)

theorem Zeta5Irrational.U_406_4 : Uω (aρ 4) (bρ 4) (6809190120381 / 16000000000000) ≤ -(9065427257069945571199 / 10000000000000000000000)

theorem Zeta5Irrational.U_406_5 : Uω (aρ 5) (bρ 5) (6809190120381 / 16000000000000) ≤ -(4686551939544443826109 / 5000000000000000000000)

theorem Zeta5Irrational.U_406_6 : Uω (aρ 6) (bρ 6) (6809190120381 / 16000000000000) ≤ -(9835128300274148067791 / 10000000000000000000000)

theorem Zeta5Irrational.U_406_7 : Uω (aρ 7) (bρ 7) (6809190120381 / 16000000000000) ≤ -(5132228374587151913 / 4882812500000000000)

theorem Zeta5Irrational.U_406_8 : Uω (aρ 8) (bρ 8) (6809190120381 / 16000000000000) ≤ -(11489883318043325304749 / 10000000000000000000000)

theorem Zeta5Irrational.U_406_9 : Uω (aρ 9) (bρ 9) (6809190120381 / 16000000000000) ≤ -(404218113034351628443 / 312500000000000000000)

theorem Zeta5Irrational.U_406_10 : Uω (aρ 10) (bρ 10) (6809190120381 / 16000000000000) ≤ -(7631299881357333164523 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_406 : Uρ (6809190120381 / 16000000000000) ≤ -(399293109801970771631 / 312500000000000000000)

theorem Zeta5Irrational.U_407_1 : Uω (aρ 1) (bρ 1) (86161340883 / 200000000000) ≤ -(342875686036299859671 / 400000000000000000000)

theorem Zeta5Irrational.U_407_2 : Uω (aρ 2) (bρ 2) (86161340883 / 200000000000) ≤ -(1725713503188980663307 / 2000000000000000000000)

theorem Zeta5Irrational.U_407_3 : Uω (aρ 3) (bρ 3) (86161340883 / 200000000000) ≤ -(8743051013203827149901 / 10000000000000000000000)

theorem Zeta5Irrational.U_407_4 : Uω (aρ 4) (bρ 4) (86161340883 / 200000000000) ≤ -(2234159628991301625199 / 2500000000000000000000)

theorem Zeta5Irrational.U_407_5 : Uω (aρ 5) (bρ 5) (86161340883 / 200000000000) ≤ -(1848035083146948254919 / 2000000000000000000000)

theorem Zeta5Irrational.U_407_6 : Uω (aρ 6) (bρ 6) (86161340883 / 200000000000) ≤ -(1939118985162720111611 / 2000000000000000000000)

theorem Zeta5Irrational.U_407_7 : Uω (aρ 7) (bρ 7) (86161340883 / 200000000000) ≤ -(10360671859386552173789 / 10000000000000000000000)

theorem Zeta5Irrational.U_407_8 : Uω (aρ 8) (bρ 8) (86161340883 / 200000000000) ≤ -(2264408210820016486429 / 2000000000000000000000)

theorem Zeta5Irrational.U_407_9 : Uω (aρ 9) (bρ 9) (86161340883 / 200000000000) ≤ -(12734304324888259626497 / 10000000000000000000000)

theorem Zeta5Irrational.U_407_10 : Uω (aρ 10) (bρ 10) (86161340883 / 200000000000) ≤ -(3745433928253882754121 / 2500000000000000000000)

theorem Zeta5Irrational.U_407_11 : Uω (aρ 11) (bρ 11) (86161340883 / 200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_407_12 : Uω (aρ 12) (bρ 12) (86161340883 / 200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_407_13 : Uω (aρ 13) (bρ 13) (86161340883 / 200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_407_14 : Uω (aρ 14) (bρ 14) (86161340883 / 200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_407_15 : Uω (aρ 15) (bρ 15) (86161340883 / 200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_407_16 : Uω (aρ 16) (bρ 16) (86161340883 / 200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_407 : Uρ (86161340883 / 200000000000) ≤ -(791874724932342320321 / 625000000000000000000)

theorem Zeta5Irrational.U_408_1 : Uω (aρ 1) (bρ 1) (54181913021 / 125000000000) ≤ -(1701934117171983693411 / 2000000000000000000000)

theorem Zeta5Irrational.U_408_2 : Uω (aρ 2) (bρ 2) (54181913021 / 125000000000) ≤ -(535374392089433119633 / 625000000000000000000)

theorem Zeta5Irrational.U_408_3 : Uω (aρ 3) (bρ 3) (54181913021 / 125000000000) ≤ -(867974593018045612053 / 1000000000000000000000)

theorem Zeta5Irrational.U_408_4 : Uω (aρ 4) (bρ 4) (54181913021 / 125000000000) ≤ -(8872073375269568597809 / 10000000000000000000000)

theorem Zeta5Irrational.U_408_5 : Uω (aρ 5) (bρ 5) (54181913021 / 125000000000) ≤ -(917355697984571850539 / 1000000000000000000000)

theorem Zeta5Irrational.U_408_6 : Uω (aρ 6) (bρ 6) (54181913021 / 125000000000) ≤ -(1925140956285161018611 / 2000000000000000000000)

theorem Zeta5Irrational.U_408_7 : Uω (aρ 7) (bρ 7) (54181913021 / 125000000000) ≤ -(10285543461370157781439 / 10000000000000000000000)

theorem Zeta5Irrational.U_408_8 : Uω (aρ 8) (bρ 8) (54181913021 / 125000000000) ≤ -(112381938674848357789 / 100000000000000000000)

theorem Zeta5Irrational.U_408_9 : Uω (aρ 9) (bρ 9) (54181913021 / 125000000000) ≤ -(12634421825163466454341 / 10000000000000000000000)

theorem Zeta5Irrational.U_408_10 : Uω (aρ 10) (bρ 10) (54181913021 / 125000000000) ≤ -(7421773000218264526129 / 5000000000000000000000)

theorem Zeta5Irrational.U_408_11 : Uω (aρ 11) (bρ 11) (54181913021 / 125000000000) ≤ -(10359853335001487342957 / 5000000000000000000000)

theorem Zeta5Irrational.U_408_12 : Uω (aρ 12) (bρ 12) (54181913021 / 125000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_408_13 : Uω (aρ 13) (bρ 13) (54181913021 / 125000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_408_14 : Uω (aρ 14) (bρ 14) (54181913021 / 125000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_408_15 : Uω (aρ 15) (bρ 15) (54181913021 / 125000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_408_16 : Uω (aρ 16) (bρ 16) (54181913021 / 125000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_408 : Uρ (54181913021 / 125000000000) ≤ -(12492873305617532369633 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_1 : Uω (aρ 1) (bρ 1) (436103903921 / 1000000000000) ≤ -(8447833787109033449899 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_2 : Uω (aρ 2) (bρ 2) (436103903921 / 1000000000000) ≤ -(531487639599329723427 / 625000000000000000000)

theorem Zeta5Irrational.U_409_3 : Uω (aρ 3) (bρ 3) (436103903921 / 1000000000000) ≤ -(4308419623487413080987 / 5000000000000000000000)

theorem Zeta5Irrational.U_409_4 : Uω (aρ 4) (bρ 4) (436103903921 / 1000000000000) ≤ -(352316917537988224177 / 400000000000000000000)

theorem Zeta5Irrational.U_409_5 : Uω (aρ 5) (bρ 5) (436103903921 / 1000000000000) ≤ -(9107380873511893660103 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_6 : Uω (aρ 6) (bρ 6) (436103903921 / 1000000000000) ≤ -(9556303782198983042833 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_7 : Uω (aρ 7) (bρ 7) (436103903921 / 1000000000000) ≤ -(10210986681307664216749 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_8 : Uω (aρ 8) (bρ 8) (436103903921 / 1000000000000) ≤ -(11155077685116505444933 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_9 : Uω (aρ 9) (bρ 9) (436103903921 / 1000000000000) ≤ -(12535644509160010633761 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_10 : Uω (aρ 10) (bρ 10) (436103903921 / 1000000000000) ≤ -(14707874772608179319249 / 10000000000000000000000)

theorem Zeta5Irrational.U_409_11 : Uω (aρ 11) (bρ 11) (436103903921 / 1000000000000) ≤ -(10036489124495165724449 / 5000000000000000000000)

theorem Zeta5Irrational.U_409_12 : Uω (aρ 12) (bρ 12) (436103903921 / 1000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_409_13 : Uω (aρ 13) (bρ 13) (436103903921 / 1000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_409_14 : Uω (aρ 14) (bρ 14) (436103903921 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_409_15 : Uω (aρ 15) (bρ 15) (436103903921 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_409_16 : Uω (aρ 16) (bρ 16) (436103903921 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_409 : Uρ (436103903921 / 1000000000000) ≤ -(6194447236115731929341 / 5000000000000000000000)

theorem Zeta5Irrational.U_410_1 : Uω (aρ 1) (bρ 1) (219376251837 / 500000000000) ≤ -(2096594256290114153041 / 2500000000000000000000)

theorem Zeta5Irrational.U_410_2 : Uω (aρ 2) (bρ 2) (219376251837 / 500000000000) ≤ -(1055249823054743877783 / 1250000000000000000000)

theorem Zeta5Irrational.U_410_3 : Uω (aρ 3) (bρ 3) (219376251837 / 500000000000) ≤ -(4277162989177892952323 / 5000000000000000000000)

theorem Zeta5Irrational.U_410_4 : Uω (aρ 4) (bρ 4) (219376251837 / 500000000000) ≤ -(4372090952870243498743 / 5000000000000000000000)

theorem Zeta5Irrational.U_410_5 : Uω (aρ 5) (bρ 5) (219376251837 / 500000000000) ≤ -(904164124252520286273 / 1000000000000000000000)

theorem Zeta5Irrational.U_410_6 : Uω (aρ 6) (bρ 6) (219376251837 / 500000000000) ≤ -(9487385073304664494243 / 10000000000000000000000)

theorem Zeta5Irrational.U_410_7 : Uω (aρ 7) (bρ 7) (219376251837 / 500000000000) ≤ -(5068496359337917405659 / 5000000000000000000000)

theorem Zeta5Irrational.U_410_8 : Uω (aρ 8) (bρ 8) (219376251837 / 500000000000) ≤ -(11072679310070797156689 / 10000000000000000000000)

theorem Zeta5Irrational.U_410_9 : Uω (aρ 9) (bρ 9) (219376251837 / 500000000000) ≤ -(6218972905446657801553 / 5000000000000000000000)

theorem Zeta5Irrational.U_410_10 : Uω (aρ 10) (bρ 10) (219376251837 / 500000000000) ≤ -(14574612834924164906609 / 10000000000000000000000)

theorem Zeta5Irrational.U_410_11 : Uω (aρ 11) (bρ 11) (219376251837 / 500000000000) ≤ -(611820281831991679449 / 312500000000000000000)

theorem Zeta5Irrational.U_410_12 : Uω (aρ 12) (bρ 12) (219376251837 / 500000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_410_13 : Uω (aρ 13) (bρ 13) (219376251837 / 500000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_410_14 : Uω (aρ 14) (bρ 14) (219376251837 / 500000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_410_15 : Uω (aρ 15) (bρ 15) (219376251837 / 500000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_410_16 : Uω (aρ 16) (bρ 16) (219376251837 / 500000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_410 : Uρ (219376251837 / 500000000000) ≤ -(12297444852051932068801 / 10000000000000000000000)

theorem Zeta5Irrational.U_411_1 : Uω (aρ 1) (bρ 1) (880153607101 / 2000000000000) ≤ -(8355789703777010327123 / 10000000000000000000000)

theorem Zeta5Irrational.U_411_2 : Uω (aρ 2) (bρ 2) (880153607101 / 2000000000000) ≤ -(1682247885388241367499 / 2000000000000000000000)

theorem Zeta5Irrational.U_411_3 : Uω (aρ 3) (bρ 3) (880153607101 / 2000000000000) ≤ -(4261607671066074145483 / 5000000000000000000000)

theorem Zeta5Irrational.U_411_4 : Uω (aρ 4) (bρ 4) (880153607101 / 2000000000000) ≤ -(2178115821864365629041 / 2500000000000000000000)

theorem Zeta5Irrational.U_411_5 : Uω (aρ 5) (bρ 5) (880153607101 / 2000000000000) ≤ -(9008933307601673657931 / 10000000000000000000000)

theorem Zeta5Irrational.U_411_6 : Uω (aρ 6) (bρ 6) (880153607101 / 2000000000000) ≤ -(4726552237572163998887 / 5000000000000000000000)

theorem Zeta5Irrational.U_411_7 : Uω (aρ 7) (bρ 7) (880153607101 / 2000000000000) ≤ -(404008164002188548969 / 400000000000000000000)

theorem Zeta5Irrational.U_411_8 : Uω (aρ 8) (bρ 8) (880153607101 / 2000000000000) ≤ -(5515872638589955285107 / 5000000000000000000000)

theorem Zeta5Irrational.U_411_9 : Uω (aρ 9) (bρ 9) (880153607101 / 2000000000000) ≤ -(12389492920326356581651 / 10000000000000000000000)

theorem Zeta5Irrational.U_411_10 : Uω (aρ 10) (bρ 10) (880153607101 / 2000000000000) ≤ -(56675208404681107481 / 39062500000000000000)

theorem Zeta5Irrational.U_411_11 : Uω (aρ 11) (bρ 11) (880153607101 / 2000000000000) ≤ -(968136623931926557471 / 500000000000000000000)

theorem Zeta5Irrational.U_411_12 : Uω (aρ 12) (bρ 12) (880153607101 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_411_13 : Uω (aρ 13) (bρ 13) (880153607101 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_411_14 : Uω (aρ 14) (bρ 14) (880153607101 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_411_15 : Uω (aρ 15) (bρ 15) (880153607101 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_411_16 : Uω (aρ 16) (bρ 16) (880153607101 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_411 : Uρ (880153607101 / 2000000000000) ≤ -(6127214758723858306379 / 5000000000000000000000)