BKLNW.Pp''_nonneg

lemma Pp''_nonneg {A₁ A₂ E : ℝ} (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E)    {m : ℕ} (hm : m ≤ 3) {y : ℝ} (hy20 : 20 ≤ y) : 0 ≤ Pp'' m A₁ A₂ E y := by  unfold Pp''  have t1 : (0 : ℝ) ≤ A₁ * pTdd m (1 / 2) y := mul_nonneg hA1 (pTdd_nonneg (by norm_num) hm hy20)  have t2 : (0 : ℝ) ≤ A₂ * pTdd m (2 / 3) y := mul_nonneg hA2 (pTdd_nonneg (by norm_num) hm hy20)  have t3 : (0 : ℝ) ≤ E * (((m + 2 : ℕ) : ℝ) * (((m + 1 : ℕ) : ℝ) * y ^ m)) := by    apply mul_nonneg hE    exact mul_nonneg (by positivity) (mul_nonneg (by positivity) (pow_nonneg (by linarith) m))  linarith [t1, t2, t3]