∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {n : ℕ},
  2 ≤ n →
    ∀ {x : ℝ},
      1 < x →
        ∀ (y : ℝ),
          0 ≤
            3 * (-Complex.log (1 - 1 ↑n * ↑n ^ (-↑x))).re +
                4 * (-Complex.log (1 - χ ↑n * ↑n ^ (-(↑x + Complex.I * ↑y)))).re +
              (-Complex.log (1 - χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * Complex.I * ↑y)))).re