Kadiri.zeroImagDyadicCumulativeCountBoundSource_of_count_by_N_and_backlund_growth

theorem zeroImagDyadicCumulativeCountBoundSource_of_count_by_N_and_backlund_growth    (hRvM : riemannZeta.Riemann_vonMangoldt_bound 0.137 0.443 6.1)    (hcountN : zeroImagDyadicCumulativeCountByNSource)    (hgrowth : zetaCountingDyadicMajorantGrowthSource) :    zeroImagDyadicCumulativeCountBoundSource := by  rcases hcountN with ⟨A, hA_nonneg, hcountN⟩  rcases hgrowth with ⟨C, hC_nonneg, hgrowth⟩  refine ⟨A * C, mul_nonneg hA_nonneg hC_nonneg, ?_⟩  intro k  have hN := zetaCountingDyadic_abs_N_le_backlund_majorant hRvM k  have hto_majorant :      A * |riemannZeta.N ((2 : ℝ) ^ (k + 1))| ≤        A * zetaCountingDyadicMajorant 0.137 0.443 6.1 k := by    exact mul_le_mul_of_nonneg_left hN hA_nonneg  have hto_growth :      A * zetaCountingDyadicMajorant 0.137 0.443 6.1 k ≤        A * (C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)) := by    exact mul_le_mul_of_nonneg_left (hgrowth k) hA_nonneg  calc    (Nat.card {rho : NontrivialZeros //        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ)        ≤ A * |riemannZeta.N ((2 : ℝ) ^ (k + 1))| := hcountN k    _ ≤ A * zetaCountingDyadicMajorant 0.137 0.443 6.1 k := hto_majorant    _ ≤ A * (C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)) := hto_growth    _ = A * C * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := by ring