von Staudt–Clausen consequences used by the proof notes, Lemma 3: v_p(B'_k) ≥ -1 always, v_p(B'_k) ≥ 0 unless k > 0 and (p - 1) ∣ k, and the resulting bounds on the local moments locMoment s e = e B'_{e-1} + 2 s B'_e for v_p(s) ≥ 1.

theorem Zeta32.PrimeEdge.VG_one_div_prime {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℕ} (hq : Nat.Prime q) (hqp : q ≠ p) : Zeta5Irrational.VG p (1 / ↑q) 0

theorem Zeta32.PrimeEdge.VG_one_div_self {p : ℕ} [hp : Fact (Nat.Prime p)] : Zeta5Irrational.VG p (1 / ↑p) (-1)

theorem Zeta32.PrimeEdge.bernoulli_even_eq (m : ℕ) : ∃ (T : ℤ), bernoulli (2 * m) = ↑T - ∑ q ∈ Finset.range (2 * m + 2) with Nat.Prime q ∧ q - 1 ∣ 2 * m, 1 / ↑q

von Staudt–Clausen, even index: B_{2m} = T - ∑_{q prime, (q-1) ∣ 2m} 1/q.

theorem Zeta32.PrimeEdge.VG_bernoulli_even {p : ℕ} [Fact (Nat.Prime p)] (m : ℕ) : Zeta5Irrational.VG p (bernoulli (2 * m)) (-1)

theorem Zeta32.PrimeEdge.VG_bernoulli_even_of_not_dvd {p : ℕ} [Fact (Nat.Prime p)] (m : ℕ) (hm : ¬p - 1 ∣ 2 * m) : Zeta5Irrational.VG p (bernoulli (2 * m)) 0

theorem Zeta32.PrimeEdge.VG_half {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) : Zeta5Irrational.VG p (1 / 2) 0

theorem Zeta32.PrimeEdge.VG_bernoulli' {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) (k : ℕ) : Zeta5Irrational.VG p (bernoulli' k) (-1)

v_p(B'_k) ≥ -1.

theorem Zeta32.PrimeEdge.VG_bernoulli'_zero {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {k : ℕ} (hk : k = 0 ∨ ¬p - 1 ∣ k) : Zeta5Irrational.VG p (bernoulli' k) 0

v_p(B'_k) ≥ 0 for k = 0 or (p - 1) ∤ k.

theorem Zeta32.PrimeEdge.VG_bernoulli'_small {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {k : ℕ} (hk : k + 2 ≤ p) : Zeta5Irrational.VG p (bernoulli' k) 0

B'_k is p-integral for k ≤ p - 2.

theorem Zeta32.PrimeEdge.VG_two_mul {p : ℕ} [Fact (Nat.Prime p)] {s r : ℚ} (h : Zeta5Irrational.VG p s r) : Zeta5Irrational.VG p (2 * s) r

theorem Zeta32.PrimeEdge.VG_locMoment {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) (e : ℕ) : Zeta5Irrational.VG p (locMoment s e) (-1)

v_p(locMoment s e) ≥ -1 when v_p(s) ≥ 1.

theorem Zeta32.PrimeEdge.VG_locMoment_zero {p : ℕ} [hp : Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {e : ℕ} (he : e + 2 ≤ 2 * p) : Zeta5Irrational.VG p (locMoment s e) 0

v_p(locMoment s e) ≥ 0 for e ≤ 2p - 2 (the only possible p in a denominator of B'_{e-1} in that range is at e = p, where the factor e cancels it).

theorem Zeta32.PrimeEdge.VG_locMoment_sub {p : ℕ} [Fact (Nat.Prime p)] (hp3 : 3 ≤ p) {s : ℚ} (hs : Zeta5Irrational.VG p s 1) {e : ℕ} (he : e + 2 ≤ p) : Zeta5Irrational.VG p (locMoment s e - locMoment 0 e) 1

locMoment s e - locMoment 0 e = 2 s B'_e has v_p ≥ 1 for e ≤ p - 2.