Small primes: products over the poles ±1, …, ±K

• ∏_{s ∈ PlK K} (m - s) = (K!)² C(m-1, K) C(m+K, K) for m > K;
• the residue denominators ∏_{s ≠ r} (r - s) at r = ±j, and v_p((K!)² / ∏_{s ≠ r} (r - s)) ≥ -log_p (2K).

theorem Zeta5Irrational.prod_Icc_sub_mul_factorial (a c : ℕ) : c < a → (∏ i ∈ Finset.Icc 1 c, (↑a - ↑i)) * ↑(a - 1 - c).factorial = ↑(a - 1).factorial

theorem Zeta5Irrational.prod_Icc_add_mul_factorial (a c : ℕ) : (∏ i ∈ Finset.Icc 1 c, (↑a + ↑i)) * ↑a.factorial = ↑(a + c).factorial

theorem Zeta5Irrational.prod_Ioc_sub (j t : ℕ) : ∏ i ∈ Finset.Ioc j (j + t), (↑j - ↑i) = (-1) ^ t * ↑t.factorial

theorem Zeta5Irrational.prod_Icc_sub_eq_choose {m K : ℕ} (h : K < m) : ∏ j ∈ Finset.Icc 1 K, (↑m - ↑j) = ↑K.factorial * ↑((m - 1).choose K)

∏_{j ≤ K} (m - j) = K! C(m-1, K) for m > K.

theorem Zeta5Irrational.prod_Icc_add_eq_choose (m K : ℕ) : ∏ j ∈ Finset.Icc 1 K, (↑m + ↑j) = ↑K.factorial * ↑((m + K).choose K)

∏_{j ≤ K} (m + j) = K! C(m+K, K).

theorem Zeta5Irrational.prod_PlK_sub {m K : ℕ} (h : K < m) : ∏ s ∈ PlK K, (↑m - ↑s) = ↑K.factorial ^ 2 * ↑((m - 1).choose K) * ↑((m + K).choose K)

The pole product at a point m > K.

theorem Zeta5Irrational.prod_Icc_ite_sub {j K : ℕ} (hj1 : 1 ≤ j) (hjK : j ≤ K) : (∏ i ∈ Finset.Icc 1 K, if i = j then 1 else ↑j - ↑i) = (-1) ^ (K - j) * ↑(j - 1).factorial * ↑(K - j).factorial

The product ∏_{i ≤ K, i ≠ j} (j - i).

theorem Zeta5Irrational.prod_erase_PlK {j K : ℕ} (hj1 : 1 ≤ j) (hjK : j ≤ K) (ε : ℤ) (hε : ε = 1 ∨ ε = -1) : ∃ (σ : ℚ), (σ = 1 ∨ σ = -1) ∧ ∏ s ∈ (PlK K).erase (ε * ↑j), (↑(ε * ↑j) - ↑s) = σ * ↑(j - 1).factorial * ↑(K - j).factorial * ↑(K + j).factorial / ↑j.factorial

Residue denominator at r = ±j, up to sign.