The integrals of the piece tables

∑_i ∫_{t_i}^{t_{i+1}} (a_i x + b_i)/x³ dx equals (5.18) for the inner table and 127751/96000 + 9/640 for the outer table.

theorem Zeta5Irrational.integral_lin_div_cube (A B : ℝ) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ (x : ℝ) in a..b, (A * x + B) / x ^ 3 = A * (1 / a - 1 / b) + B / 2 * (1 / a ^ 2 - 1 / b ^ 2)

theorem Zeta5Irrational.tIn_pos (i : ℕ) (hi : i ≤ 125) : 0 < tIn i

theorem Zeta5Irrational.tOut_pos (i : ℕ) (hi : i ≤ 13) : 0 < tOut i

theorem Zeta5Irrational.inner_integrals : ∑ i ∈ Finset.range 125, ∫ (x : ℝ) in tIn i..tIn (i + 1), gIn i x / x ^ 3 = 322437603634266857629 / 7535670527041937280000

theorem Zeta5Irrational.outer_integrals : ∑ i ∈ Finset.range 13, ∫ (x : ℝ) in tOut i..tOut (i + 1), gOut i x / x ^ 3 = 129101 / 96000