Certified arcsine potential bounds (U31)

theorem Zeta5Irrational.U_376_1 : Uω (aρ 1) (bρ 1) (23971791621423 / 64000000000000) ≤ -(9993867007066015957191 / 10000000000000000000000)

theorem Zeta5Irrational.U_376_2 : Uω (aρ 2) (bρ 2) (23971791621423 / 64000000000000) ≤ -(10059320806281235657447 / 10000000000000000000000)

theorem Zeta5Irrational.U_376_3 : Uω (aρ 3) (bρ 3) (23971791621423 / 64000000000000) ≤ -(2038361309453471391991 / 2000000000000000000000)

theorem Zeta5Irrational.U_376_4 : Uω (aρ 4) (bρ 4) (23971791621423 / 64000000000000) ≤ -(5208342325874971915933 / 5000000000000000000000)

theorem Zeta5Irrational.U_376_5 : Uω (aρ 5) (bρ 5) (23971791621423 / 64000000000000) ≤ -(2692890035511764538969 / 2500000000000000000000)

theorem Zeta5Irrational.U_376_6 : Uω (aρ 6) (bρ 6) (23971791621423 / 64000000000000) ≤ -(11309727313063090127271 / 10000000000000000000000)

theorem Zeta5Irrational.U_376_7 : Uω (aρ 7) (bρ 7) (23971791621423 / 64000000000000) ≤ -(12109924977090579279271 / 10000000000000000000000)

theorem Zeta5Irrational.U_376_8 : Uω (aρ 8) (bρ 8) (23971791621423 / 64000000000000) ≤ -(13304483040210431015309 / 10000000000000000000000)

theorem Zeta5Irrational.U_376_9 : Uω (aρ 9) (bρ 9) (23971791621423 / 64000000000000) ≤ -(15180537896117200035529 / 10000000000000000000000)

theorem Zeta5Irrational.U_376_10 : Uω (aρ 10) (bρ 10) (23971791621423 / 64000000000000) ≤ -(18892689722321229897263 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_376 : Uρ (23971791621423 / 64000000000000) ≤ -(6991230191038809068327 / 5000000000000000000000)

theorem Zeta5Irrational.U_377_1 : Uω (aρ 1) (bρ 1) (9605460078621 / 25600000000000) ≤ -(9976114805201331339663 / 10000000000000000000000)

theorem Zeta5Irrational.U_377_2 : Uω (aρ 2) (bρ 2) (9605460078621 / 25600000000000) ≤ -(2510362732834259353731 / 2500000000000000000000)

theorem Zeta5Irrational.U_377_3 : Uω (aρ 3) (bρ 3) (9605460078621 / 25600000000000) ≤ -(10173694864971688524833 / 10000000000000000000000)

theorem Zeta5Irrational.U_377_4 : Uω (aρ 4) (bρ 4) (9605460078621 / 25600000000000) ≤ -(5199075537472519501479 / 5000000000000000000000)

theorem Zeta5Irrational.U_377_5 : Uω (aρ 5) (bρ 5) (9605460078621 / 25600000000000) ≤ -(10752329842358406152703 / 10000000000000000000000)

theorem Zeta5Irrational.U_377_6 : Uω (aρ 6) (bρ 6) (9605460078621 / 25600000000000) ≤ -(11289361654615094735919 / 10000000000000000000000)

theorem Zeta5Irrational.U_377_7 : Uω (aρ 7) (bρ 7) (9605460078621 / 25600000000000) ≤ -(12087670011636276249273 / 10000000000000000000000)

theorem Zeta5Irrational.U_377_8 : Uω (aρ 8) (bρ 8) (9605460078621 / 25600000000000) ≤ -(13278851339418135968547 / 10000000000000000000000)

theorem Zeta5Irrational.U_377_9 : Uω (aρ 9) (bρ 9) (9605460078621 / 25600000000000) ≤ -(3029529911736138818707 / 2000000000000000000000)

theorem Zeta5Irrational.U_377_10 : Uω (aρ 10) (bρ 10) (9605460078621 / 25600000000000) ≤ -(18828606670727822522699 / 10000000000000000000000)

theorem Zeta5Irrational.U_377_11 : Uω (aρ 11) (bρ 11) (9605460078621 / 25600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_377_12 : Uω (aρ 12) (bρ 12) (9605460078621 / 25600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_377_13 : Uω (aρ 13) (bρ 13) (9605460078621 / 25600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_377_14 : Uω (aρ 14) (bρ 14) (9605460078621 / 25600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_377_15 : Uω (aρ 15) (bρ 15) (9605460078621 / 25600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_377_16 : Uω (aρ 16) (bρ 16) (9605460078621 / 25600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_377 : Uρ (9605460078621 / 25600000000000) ≤ -(2792884219465679483077 / 2000000000000000000000)

theorem Zeta5Irrational.U_378_1 : Uω (aρ 1) (bρ 1) (12027754385841 / 32000000000000) ≤ -(9958394062313398461891 / 10000000000000000000000)

theorem Zeta5Irrational.U_378_2 : Uω (aρ 2) (bρ 2) (12027754385841 / 32000000000000) ≤ -(10023612937712580116809 / 10000000000000000000000)

theorem Zeta5Irrational.U_378_3 : Uω (aρ 3) (bρ 3) (12027754385841 / 32000000000000) ≤ -(10155615945187571679447 / 10000000000000000000000)

theorem Zeta5Irrational.U_378_4 : Uω (aρ 4) (bρ 4) (12027754385841 / 32000000000000) ≤ -(518982592080921205731 / 500000000000000000000)

theorem Zeta5Irrational.U_378_5 : Uω (aρ 5) (bρ 5) (12027754385841 / 32000000000000) ≤ -(10733136621036858840227 / 10000000000000000000000)

theorem Zeta5Irrational.U_378_6 : Uω (aρ 6) (bρ 6) (12027754385841 / 32000000000000) ≤ -(11269037875509371656561 / 10000000000000000000000)

theorem Zeta5Irrational.U_378_7 : Uω (aρ 7) (bρ 7) (12027754385841 / 32000000000000) ≤ -(2413093184052817137671 / 2000000000000000000000)

theorem Zeta5Irrational.U_378_8 : Uω (aρ 8) (bρ 8) (12027754385841 / 32000000000000) ≤ -(13253290037235338137851 / 10000000000000000000000)

theorem Zeta5Irrational.U_378_9 : Uω (aρ 9) (bρ 9) (12027754385841 / 32000000000000) ≤ -(7557445616019576398087 / 5000000000000000000000)

theorem Zeta5Irrational.U_378_10 : Uω (aρ 10) (bρ 10) (12027754385841 / 32000000000000) ≤ -(18765319741641310131049 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_378 : Uρ (12027754385841 / 32000000000000) ≤ -(13946482418286257096903 / 10000000000000000000000)

theorem Zeta5Irrational.U_379_1 : Uω (aρ 1) (bρ 1) (48194734693623 / 128000000000000) ≤ -(9940704667098828597671 / 10000000000000000000000)

theorem Zeta5Irrational.U_379_2 : Uω (aρ 2) (bρ 2) (48194734693623 / 128000000000000) ≤ -(2501451677958700695517 / 2500000000000000000000)

theorem Zeta5Irrational.U_379_3 : Uω (aρ 3) (bρ 3) (48194734693623 / 128000000000000) ≤ -(5068784834766586812851 / 5000000000000000000000)

theorem Zeta5Irrational.U_379_4 : Uω (aρ 4) (bρ 4) (48194734693623 / 128000000000000) ≤ -(414447472980535392993 / 400000000000000000000)

theorem Zeta5Irrational.U_379_5 : Uω (aρ 5) (bρ 5) (48194734693623 / 128000000000000) ≤ -(10713980334728234077113 / 10000000000000000000000)

theorem Zeta5Irrational.U_379_6 : Uω (aρ 6) (bρ 6) (48194734693623 / 128000000000000) ≤ -(11248755801878956064031 / 10000000000000000000000)

theorem Zeta5Irrational.U_379_7 : Uω (aρ 7) (bρ 7) (48194734693623 / 128000000000000) ≤ -(602165623219844768649 / 500000000000000000000)

theorem Zeta5Irrational.U_379_8 : Uω (aρ 8) (bρ 8) (48194734693623 / 128000000000000) ≤ -(6613899361208653044927 / 5000000000000000000000)

theorem Zeta5Irrational.U_379_9 : Uω (aρ 9) (bρ 9) (48194734693623 / 128000000000000) ≤ -(3770565433462939589999 / 2500000000000000000000)

theorem Zeta5Irrational.U_379_10 : Uω (aρ 10) (bρ 10) (48194734693623 / 128000000000000) ≤ -(3740560484983560820433 / 2000000000000000000000)

theorem Zeta5Irrational.U_379_11 : Uω (aρ 11) (bρ 11) (48194734693623 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_379_12 : Uω (aρ 12) (bρ 12) (48194734693623 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_379_13 : Uω (aρ 13) (bρ 13) (48194734693623 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_379_14 : Uω (aρ 14) (bρ 14) (48194734693623 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_379_15 : Uω (aρ 15) (bρ 15) (48194734693623 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_379_16 : Uω (aρ 16) (bρ 16) (48194734693623 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_379 : Uρ (48194734693623 / 128000000000000) ≤ -(13928641877448414677921 / 10000000000000000000000)

theorem Zeta5Irrational.U_380_1 : Uω (aρ 1) (bρ 1) (24139225921941 / 64000000000000) ≤ -(4961523254421947127759 / 5000000000000000000000)

theorem Zeta5Irrational.U_380_2 : Uω (aρ 2) (bρ 2) (24139225921941 / 64000000000000) ≤ -(1248504017592068370069 / 1250000000000000000000)

theorem Zeta5Irrational.U_380_3 : Uω (aρ 3) (bρ 3) (24139225921941 / 64000000000000) ≤ -(10119555920267487374541 / 10000000000000000000000)

theorem Zeta5Irrational.U_380_4 : Uω (aρ 4) (bρ 4) (24139225921941 / 64000000000000) ≤ -(10342755897080370757173 / 10000000000000000000000)

theorem Zeta5Irrational.U_380_5 : Uω (aρ 5) (bρ 5) (24139225921941 / 64000000000000) ≤ -(10694860840911806552079 / 10000000000000000000000)

theorem Zeta5Irrational.U_380_6 : Uω (aρ 6) (bρ 6) (24139225921941 / 64000000000000) ≤ -(5614257630474681781133 / 5000000000000000000000)

theorem Zeta5Irrational.U_380_7 : Uω (aρ 7) (bρ 7) (24139225921941 / 64000000000000) ≤ -(3005302351793728355003 / 2500000000000000000000)

theorem Zeta5Irrational.U_380_8 : Uω (aρ 8) (bρ 8) (24139225921941 / 64000000000000) ≤ -(6601188493753449905703 / 5000000000000000000000)

theorem Zeta5Irrational.U_380_9 : Uω (aρ 9) (bρ 9) (24139225921941 / 64000000000000) ≤ -(601990395975625400427 / 400000000000000000000)

theorem Zeta5Irrational.U_380_10 : Uω (aρ 10) (bρ 10) (24139225921941 / 64000000000000) ≤ -(4660257416487714340737 / 2500000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_380 : Uρ (24139225921941 / 64000000000000) ≤ -(6955448566996252704807 / 5000000000000000000000)

theorem Zeta5Irrational.U_381_1 : Uω (aρ 1) (bρ 1) (48362168994141 / 128000000000000) ≤ -(9905419477420379522699 / 10000000000000000000000)

theorem Zeta5Irrational.U_381_2 : Uω (aρ 2) (bρ 2) (48362168994141 / 128000000000000) ≤ -(997028911205224600551 / 1000000000000000000000)

theorem Zeta5Irrational.U_381_3 : Uω (aρ 3) (bρ 3) (48362168994141 / 128000000000000) ≤ -(10101574580285721318899 / 10000000000000000000000)

theorem Zeta5Irrational.U_381_4 : Uω (aρ 4) (bρ 4) (48362168994141 / 128000000000000) ≤ -(10324358933471767397939 / 10000000000000000000000)

theorem Zeta5Irrational.U_381_5 : Uω (aρ 5) (bρ 5) (48362168994141 / 128000000000000) ≤ -(2135155599578764903971 / 2000000000000000000000)

theorem Zeta5Irrational.U_381_6 : Uω (aρ 6) (bρ 6) (48362168994141 / 128000000000000) ≤ -(2802079020257341762367 / 2500000000000000000000)

theorem Zeta5Irrational.U_381_7 : Uω (aρ 7) (bρ 7) (48362168994141 / 128000000000000) ≤ -(11999156513438851452341 / 10000000000000000000000)

theorem Zeta5Irrational.U_381_8 : Uω (aρ 8) (bρ 8) (48362168994141 / 128000000000000) ≤ -(329425610719656756109 / 250000000000000000000)

theorem Zeta5Irrational.U_381_9 : Uω (aρ 9) (bρ 9) (48362168994141 / 128000000000000) ≤ -(15017384581172952189737 / 10000000000000000000000)

theorem Zeta5Irrational.U_381_10 : Uω (aρ 10) (bρ 10) (48362168994141 / 128000000000000) ≤ -(18579977755783579673383 / 10000000000000000000000)

theorem Zeta5Irrational.U_381_11 : Uω (aρ 11) (bρ 11) (48362168994141 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_381_12 : Uω (aρ 12) (bρ 12) (48362168994141 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_381_13 : Uω (aρ 13) (bρ 13) (48362168994141 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_381_14 : Uω (aρ 14) (bρ 14) (48362168994141 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_381_15 : Uω (aρ 15) (bρ 15) (48362168994141 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_381_16 : Uω (aρ 16) (bρ 16) (48362168994141 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_381 : Uρ (48362168994141 / 128000000000000) ≤ -(2778649192868835725683 / 2000000000000000000000)

theorem Zeta5Irrational.U_382_1 : Uω (aρ 1) (bρ 1) (121114715361 / 320000000000) ≤ -(395512938531258084853 / 400000000000000000000)

theorem Zeta5Irrational.U_382_2 : Uω (aρ 2) (bρ 2) (121114715361 / 320000000000) ≤ -(398103100560546859391 / 400000000000000000000)

theorem Zeta5Irrational.U_382_3 : Uω (aρ 3) (bρ 3) (121114715361 / 320000000000) ≤ -(2520906383278679509249 / 2500000000000000000000)

theorem Zeta5Irrational.U_382_4 : Uω (aρ 4) (bρ 4) (121114715361 / 320000000000) ≤ -(25764989521341751801 / 25000000000000000000)

theorem Zeta5Irrational.U_382_5 : Uω (aρ 5) (bρ 5) (121114715361 / 320000000000) ≤ -(10656731664801098998343 / 10000000000000000000000)

theorem Zeta5Irrational.U_382_6 : Uω (aρ 6) (bρ 6) (121114715361 / 320000000000) ≤ -(11188158091501860923951 / 10000000000000000000000)

theorem Zeta5Irrational.U_382_7 : Uω (aρ 7) (bρ 7) (121114715361 / 320000000000) ≤ -(5988576774856659351441 / 5000000000000000000000)

theorem Zeta5Irrational.U_382_8 : Uω (aρ 8) (bρ 8) (121114715361 / 320000000000) ≤ -(13151740646229372841851 / 10000000000000000000000)

theorem Zeta5Irrational.U_382_9 : Uω (aρ 9) (bρ 9) (121114715361 / 320000000000) ≤ -(14985134648602909743777 / 10000000000000000000000)

theorem Zeta5Irrational.U_382_10 : Uω (aρ 10) (bρ 10) (121114715361 / 320000000000) ≤ -(72342282154980825373 / 39062500000000000000)

theorem Zeta5Irrational.U_382_11 : Uω (aρ 11) (bρ 11) (121114715361 / 320000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_382_12 : Uω (aρ 12) (bρ 12) (121114715361 / 320000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_382_13 : Uω (aρ 13) (bρ 13) (121114715361 / 320000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_382_14 : Uω (aρ 14) (bρ 14) (121114715361 / 320000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_382_15 : Uω (aρ 15) (bρ 15) (121114715361 / 320000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_382_16 : Uω (aρ 16) (bρ 16) (121114715361 / 320000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_382 : Uρ (121114715361 / 320000000000) ≤ -(2775137250727846017459 / 2000000000000000000000)

theorem Zeta5Irrational.U_383_1 : Uω (aρ 1) (bρ 1) (48529603294659 / 128000000000000) ≤ -(38555696708818691983 / 39062500000000000000)

theorem Zeta5Irrational.U_383_2 : Uω (aρ 2) (bρ 2) (48529603294659 / 128000000000000) ≤ -(993489723544569558129 / 1000000000000000000000)

theorem Zeta5Irrational.U_383_3 : Uω (aρ 3) (bρ 3) (48529603294659 / 128000000000000) ≤ -(2516427165727103197089 / 2500000000000000000000)

theorem Zeta5Irrational.U_383_4 : Uω (aρ 4) (bρ 4) (48529603294659 / 128000000000000) ≤ -(10287666397815893786367 / 10000000000000000000000)

theorem Zeta5Irrational.U_383_5 : Uω (aρ 5) (bρ 5) (48529603294659 / 128000000000000) ≤ -(5318860850787325044227 / 5000000000000000000000)

theorem Zeta5Irrational.U_383_6 : Uω (aρ 6) (bρ 6) (48529603294659 / 128000000000000) ≤ -(11168041122814828369441 / 10000000000000000000000)

theorem Zeta5Irrational.U_383_7 : Uω (aρ 7) (bρ 7) (48529603294659 / 128000000000000) ≤ -(11955200284190424110453 / 10000000000000000000000)

theorem Zeta5Irrational.U_383_8 : Uω (aρ 8) (bρ 8) (48529603294659 / 128000000000000) ≤ -(3281631310863808718577 / 2500000000000000000000)

theorem Zeta5Irrational.U_383_9 : Uω (aρ 9) (bρ 9) (48529603294659 / 128000000000000) ≤ -(934563061726455595199 / 625000000000000000000)

theorem Zeta5Irrational.U_383_10 : Uω (aρ 10) (bρ 10) (48529603294659 / 128000000000000) ≤ -(9229973893465110443607 / 5000000000000000000000)

theorem Zeta5Irrational.U_383_11 : Uω (aρ 11) (bρ 11) (48529603294659 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_383_12 : Uω (aρ 12) (bρ 12) (48529603294659 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_383_13 : Uω (aρ 13) (bρ 13) (48529603294659 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_383_14 : Uω (aρ 14) (bρ 14) (48529603294659 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_383_15 : Uω (aρ 15) (bρ 15) (48529603294659 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_383_16 : Uω (aρ 16) (bρ 16) (48529603294659 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_383 : Uρ (48529603294659 / 128000000000000) ≤ -(13858215987978432094499 / 10000000000000000000000)

theorem Zeta5Irrational.U_384_1 : Uω (aρ 1) (bρ 1) (24306660222459 / 64000000000000) ≤ -(9852724051552499823691 / 10000000000000000000000)

theorem Zeta5Irrational.U_384_2 : Uω (aρ 2) (bρ 2) (24306660222459 / 64000000000000) ≤ -(9917248165762109789853 / 10000000000000000000000)

theorem Zeta5Irrational.U_384_3 : Uω (aρ 3) (bρ 3) (24306660222459 / 64000000000000) ≤ -(5023911927221671117419 / 5000000000000000000000)

theorem Zeta5Irrational.U_384_4 : Uω (aρ 4) (bρ 4) (24306660222459 / 64000000000000) ≤ -(10269370577536574744851 / 10000000000000000000000)

theorem Zeta5Irrational.U_384_5 : Uω (aρ 5) (bρ 5) (24306660222459 / 64000000000000) ≤ -(2654686992240856056823 / 2500000000000000000000)

theorem Zeta5Irrational.U_384_6 : Uω (aρ 6) (bρ 6) (24306660222459 / 64000000000000) ≤ -(11147965006472399763539 / 10000000000000000000000)

theorem Zeta5Irrational.U_384_7 : Uω (aρ 7) (bρ 7) (24306660222459 / 64000000000000) ≤ -(5966648243356786807413 / 5000000000000000000000)

theorem Zeta5Irrational.U_384_8 : Uω (aρ 8) (bρ 8) (24306660222459 / 64000000000000) ≤ -(1310137782768200082229 / 1000000000000000000000)

theorem Zeta5Irrational.U_384_9 : Uω (aρ 9) (bρ 9) (24306660222459 / 64000000000000) ≤ -(14921006500376229850049 / 10000000000000000000000)

theorem Zeta5Irrational.U_384_10 : Uω (aρ 10) (bρ 10) (24306660222459 / 64000000000000) ≤ -(18400928188958520139997 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_384 : Uρ (24306660222459 / 64000000000000) ≤ -(3460208311846665330791 / 2500000000000000000000)

theorem Zeta5Irrational.U_385_1 : Uω (aρ 1) (bρ 1) (48697037595177 / 128000000000000) ≤ -(9835220437739158478671 / 10000000000000000000000)

theorem Zeta5Irrational.U_385_2 : Uω (aρ 2) (bρ 2) (48697037595177 / 128000000000000) ≤ -(4949815097480732821211 / 5000000000000000000000)

theorem Zeta5Irrational.U_385_3 : Uω (aρ 3) (bρ 3) (48697037595177 / 128000000000000) ≤ -(5014985496557094599463 / 5000000000000000000000)

theorem Zeta5Irrational.U_385_4 : Uω (aρ 4) (bρ 4) (48697037595177 / 128000000000000) ≤ -(5125554112303715040283 / 5000000000000000000000)

theorem Zeta5Irrational.U_385_5 : Uω (aρ 5) (bρ 5) (48697037595177 / 128000000000000) ≤ -(2119962065703611401969 / 2000000000000000000000)

theorem Zeta5Irrational.U_385_6 : Uω (aρ 6) (bρ 6) (48697037595177 / 128000000000000) ≤ -(445117183001040530557 / 400000000000000000000)

theorem Zeta5Irrational.U_385_7 : Uω (aρ 7) (bρ 7) (48697037595177 / 128000000000000) ≤ -(1488930241095184756289 / 1250000000000000000000)

theorem Zeta5Irrational.U_385_8 : Uω (aρ 8) (bρ 8) (48697037595177 / 128000000000000) ≤ -(6538149004840853801523 / 5000000000000000000000)

theorem Zeta5Irrational.U_385_9 : Uω (aρ 9) (bρ 9) (48697037595177 / 128000000000000) ≤ -(14889126104872971111557 / 10000000000000000000000)

theorem Zeta5Irrational.U_385_10 : Uω (aρ 10) (bρ 10) (48697037595177 / 128000000000000) ≤ -(18342546204662378687801 / 10000000000000000000000)

theorem Zeta5Irrational.U_385_11 : Uω (aρ 11) (bρ 11) (48697037595177 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_385_12 : Uω (aρ 12) (bρ 12) (48697037595177 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_385_13 : Uω (aρ 13) (bρ 13) (48697037595177 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_385_14 : Uω (aρ 14) (bρ 14) (48697037595177 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_385_15 : Uω (aρ 15) (bρ 15) (48697037595177 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_385_16 : Uω (aρ 16) (bρ 16) (48697037595177 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_385 : Uρ (48697037595177 / 128000000000000) ≤ -(13823536199399352962991 / 10000000000000000000000)

theorem Zeta5Irrational.U_386_1 : Uω (aρ 1) (bρ 1) (12195188686359 / 32000000000000) ≤ -(9817747408755780516049 / 10000000000000000000000)

theorem Zeta5Irrational.U_386_2 : Uω (aρ 2) (bρ 2) (12195188686359 / 32000000000000) ≤ -(4941021606811480716549 / 5000000000000000000000)

theorem Zeta5Irrational.U_386_3 : Uω (aρ 3) (bρ 3) (12195188686359 / 32000000000000) ≤ -(625759372808085277601 / 625000000000000000000)

theorem Zeta5Irrational.U_386_4 : Uω (aρ 4) (bρ 4) (12195188686359 / 32000000000000) ≤ -(10232879216613597053591 / 10000000000000000000000)

theorem Zeta5Irrational.U_386_5 : Uω (aρ 5) (bρ 5) (12195188686359 / 32000000000000) ≤ -(10580908642584709892287 / 10000000000000000000000)

theorem Zeta5Irrational.U_386_6 : Uω (aρ 6) (bρ 6) (12195188686359 / 32000000000000) ≤ -(11107934662065662635813 / 10000000000000000000000)

theorem Zeta5Irrational.U_386_7 : Uω (aρ 7) (bρ 7) (12195188686359 / 32000000000000) ≤ -(2377927276686470457359 / 2000000000000000000000)

theorem Zeta5Irrational.U_386_8 : Uω (aρ 8) (bρ 8) (12195188686359 / 32000000000000) ≤ -(13051285403735799505811 / 10000000000000000000000)

theorem Zeta5Irrational.U_386_9 : Uω (aρ 9) (bρ 9) (12195188686359 / 32000000000000) ≤ -(7428683367336118564909 / 5000000000000000000000)

theorem Zeta5Irrational.U_386_10 : Uω (aρ 10) (bρ 10) (12195188686359 / 32000000000000) ≤ -(18284783532368180351299 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_386 : Uρ (12195188686359 / 32000000000000) ≤ -(6903161546604532718271 / 5000000000000000000000)

theorem Zeta5Irrational.U_387_1 : Uω (aρ 1) (bρ 1) (9772894379139 / 25600000000000) ≤ -(9800304857901901130603 / 10000000000000000000000)

theorem Zeta5Irrational.U_387_2 : Uω (aρ 2) (bρ 2) (9772894379139 / 25600000000000) ≤ -(4932243556451181186989 / 5000000000000000000000)

theorem Zeta5Irrational.U_387_3 : Uω (aρ 3) (bρ 3) (9772894379139 / 25600000000000) ≤ -(499718032825331389293 / 500000000000000000000)

theorem Zeta5Irrational.U_387_4 : Uω (aρ 4) (bρ 4) (9772894379139 / 25600000000000) ≤ -(10214683431811717131443 / 10000000000000000000000)

theorem Zeta5Irrational.U_387_5 : Uω (aρ 5) (bρ 5) (9772894379139 / 25600000000000) ≤ -(10562042774298962654907 / 10000000000000000000000)

theorem Zeta5Irrational.U_387_6 : Uω (aρ 6) (bρ 6) (9772894379139 / 25600000000000) ≤ -(11087980102211234289417 / 10000000000000000000000)

theorem Zeta5Irrational.U_387_7 : Uω (aρ 7) (bρ 7) (9772894379139 / 25600000000000) ≤ -(11867879625428304621113 / 10000000000000000000000)

theorem Zeta5Irrational.U_387_8 : Uω (aρ 8) (bρ 8) (9772894379139 / 25600000000000) ≤ -(3256584906897836630917 / 2500000000000000000000)

theorem Zeta5Irrational.U_387_9 : Uω (aρ 9) (bρ 9) (9772894379139 / 25600000000000) ≤ -(593029093542680300733 / 400000000000000000000)

theorem Zeta5Irrational.U_387_10 : Uω (aρ 10) (bρ 10) (9772894379139 / 25600000000000) ≤ -(18227622739612179984223 / 10000000000000000000000)

theorem Zeta5Irrational.U_387_11 : Uω (aρ 11) (bρ 11) (9772894379139 / 25600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_387_12 : Uω (aρ 12) (bρ 12) (9772894379139 / 25600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_387_13 : Uω (aρ 13) (bρ 13) (9772894379139 / 25600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_387_14 : Uω (aρ 14) (bρ 14) (9772894379139 / 25600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_387_15 : Uω (aρ 15) (bρ 15) (9772894379139 / 25600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_387_16 : Uω (aρ 16) (bρ 16) (9772894379139 / 25600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_387 : Uρ (9772894379139 / 25600000000000) ≤ -(13789192254313298509481 / 10000000000000000000000)