V36: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_433 : 3774887277605171324213 / 10000000000000000000000 - 6 * (3 / 40) * -(479593316593176151771 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3386063355216127 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2976340953035626311821 / 10000000000000000000000)) - 6 * (11029859851979670127 / 100000000000000000000))) ≤ Vfield (917234003643 / 2000000000000)

theorem Zeta5Irrational.V_434 : 377942582123225227881 / 1000000000000000000000 - 6 * (3 / 40) * -(7659240193694681880157 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6777013735855563 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2978015798672107485851 / 10000000000000000000000)) - 6 * (1102197030739536467523 / 10000000000000000000000))) ≤ Vfield (1837116607039 / 4000000000000)

theorem Zeta5Irrational.V_435 : 18919811529779573573 / 50000000000000000000 - 6 * (3 / 40) * -(1529001521484943568809 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6781897239696277 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2979688678173779422881 / 10000000000000000000000)) - 6 * (34419055214933789157 / 312500000000000000000))) ≤ Vfield (229970650849 / 500000000000)

theorem Zeta5Irrational.V_436 : 3788496733643348428943 / 10000000000000000000000 - 6 * (3 / 40) * -(1907698812254968296973 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6786777229556381 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2981359595926635812237 / 10000000000000000000000)) - 6 * (44024967503350408363 / 400000000000000000000))) ≤ Vfield (368482761309 / 800000000000)

theorem Zeta5Irrational.V_437 : 3793029106159204379151 / 10000000000000000000000 - 6 * (3 / 40) * -(7616603061064595854687 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6791653713010549 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2983028556301359654301 / 10000000000000000000000)) - 6 * (549920143428996453391 / 5000000000000000000000))) ≤ Vfield (922531203149 / 2000000000000)

theorem Zeta5Irrational.V_438 : 1898779712682799641597 / 5000000000000000000000 - 6 * (3 / 40) * -(7602430986387443157753 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1699131674401571 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2984695563653398434181 / 10000000000000000000000)) - 6 * (549529029365633383129 / 5000000000000000000000))) ≤ Vfield (1847711006051 / 4000000000000)

theorem Zeta5Irrational.V_439 : 3802087693122120209983 / 10000000000000000000000 - 6 * (3 / 40) * -(758827896805969992371 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (425087261929003 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2986360622323037088307 / 10000000000000000000000)) - 6 * (1098277497263947141799 / 10000000000000000000000))) ≤ Vfield (462589901451 / 1000000000000)

theorem Zeta5Irrational.V_440 : 3806613911285829159271 / 10000000000000000000000 - 6 * (3 / 40) * -(946768368674250799957 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3403131100138701 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (597604747327094440931 / 2000000000000000000000)) - 6 * (274374649136471787029 / 2500000000000000000000))) ≤ Vfield (1853008205557 / 4000000000000)

theorem Zeta5Irrational.V_441 : 1905569040855633815593 / 5000000000000000000000 - 6 * (3 / 40) * -(75600348739429958419 / 100000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6811124733313139 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (298968491090088576719 / 1000000000000000000000)) - 6 * (68545084418514996731 / 625000000000000000000))) ≤ Vfield (185565680531 / 400000000000)

theorem Zeta5Irrational.V_442 : 23847876289065382409 / 62500000000000000000 - 6 * (3 / 40) * -(7545942685497941771449 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3407991898705709 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2991344149414517301659 / 10000000000000000000000)) - 6 * (1095945753863272201041 / 10000000000000000000000))) ≤ Vfield (1858305405063 / 4000000000000)

theorem Zeta5Irrational.V_443 : 382018028675292399023 / 1000000000000000000000 - 6 * (3 / 40) * -(3765935164043707208489 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3410419699992949 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (598600291291347412667 / 2000000000000000000000)) - 6 * (136896475028022353711 / 1250000000000000000000))) ≤ Vfield (116309625301 / 250000000000)

theorem Zeta5Irrational.V_444 : 3824698325065663360863 / 10000000000000000000000 - 6 * (3 / 40) * -(1879454436493986812577 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1365138309684773 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2994656836293116231503 / 10000000000000000000000)) - 6 * (68399967749056262157 / 625000000000000000000))) ≤ Vfield (1863602604569 / 4000000000000)