Kadiri.zeroImagDyadicCumulativeCountBoundSource_of_count_by_N_with_zero_height_and_backlund_growth

theorem zeroImagDyadicCumulativeCountBoundSource_of_count_by_N_with_zero_height_and_backlund_growth    (hRvM : riemannZeta.Riemann_vonMangoldt_bound 0.137 0.443 6.1)    (hcountN : zeroImagDyadicCumulativeCountByNWithZeroHeightSource)    (hgrowth : zetaCountingDyadicMajorantGrowthSource) :    zeroImagDyadicCumulativeCountBoundSource := by  rcases hcountN with ⟨A, D, hA_nonneg, hD_nonneg, hcountN⟩  rcases hgrowth with ⟨C, hC_nonneg, hgrowth⟩  refine ⟨A * C + D, add_nonneg (mul_nonneg hA_nonneg hC_nonneg) hD_nonneg, ?_⟩  intro k  let G : ℝ := ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)  have hN := zetaCountingDyadic_abs_N_le_backlund_majorant hRvM k  have hto_majorant :      A * |riemannZeta.N ((2 : ℝ) ^ (k + 1))| + D ≤        A * zetaCountingDyadicMajorant 0.137 0.443 6.1 k + D := by    exact add_le_add_left (mul_le_mul_of_nonneg_left hN hA_nonneg) D  have hto_growth :      A * zetaCountingDyadicMajorant 0.137 0.443 6.1 k + D ≤        A * (C * G) + D := by    have hgrowthk :        zetaCountingDyadicMajorant 0.137 0.443 6.1 k ≤ C * G := by      dsimp [G]      calc        zetaCountingDyadicMajorant 0.137 0.443 6.1 k            ≤ C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := hgrowth k        _ = C * (((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)) := by ring    exact add_le_add_left (mul_le_mul_of_nonneg_left hgrowthk hA_nonneg) D  have hk_one : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by    exact_mod_cast Nat.succ_le_succ (Nat.zero_le k)  have hpow_one : (1 : ℝ) ≤ (2 : ℝ) ^ k :=    one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)  have hG_one : (1 : ℝ) ≤ G := by    dsimp [G]    calc      (1 : ℝ) = 1 * 1 := by ring      _ ≤ ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) :=          mul_le_mul hk_one hpow_one (by norm_num) (le_trans (by norm_num) hk_one)  have hD_absorb : D ≤ D * G := by    calc      D = D * 1 := by ring      _ ≤ D * G := mul_le_mul_of_nonneg_left hG_one hD_nonneg  calc    (Nat.card {rho : NontrivialZeros //        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ)        ≤ A * |riemannZeta.N ((2 : ℝ) ^ (k + 1))| + D := hcountN k    _ ≤ A * zetaCountingDyadicMajorant 0.137 0.443 6.1 k + D := hto_majorant    _ ≤ A * (C * G) + D := hto_growth    _ ≤ A * (C * G) + D * G := add_le_add_right hD_absorb (A * (C * G))    _ = (A * C + D) * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := by          dsimp [G]          ring