Kadiri.zeroImagDyadicCumulativeCountByNSource_of_positive_bridge

theorem zeroImagDyadicCumulativeCountByNSource_of_positive_bridge    (habs : zeroImagDyadicAbsToPositiveCountSource)    (hNprime : zeroImagDyadicNPrimeToNSource) :    zeroImagDyadicCumulativeCountByNSource := by  rcases habs with ⟨A, hA_nonneg, habs⟩  rcases hNprime with ⟨B, hB_nonneg, hNprime⟩  refine ⟨A * B, mul_nonneg hA_nonneg hB_nonneg, ?_⟩  intro k  let T : ℝ := (2 : ℝ) ^ (k + 1)  have hpositive :=    positive_height_nontrivial_zero_count_le_NPrime T  have hpositive_nonneg :      0 ≤ (Nat.card {rho : NontrivialZeros //        0 < (rho : ℂ).im ∧ (rho : ℂ).im < T} : ℝ) := by    exact_mod_cast Nat.zero_le      (Nat.card {rho : NontrivialZeros // 0 < (rho : ℂ).im ∧ (rho : ℂ).im < T})  have hNprime_nonneg : 0 ≤ riemannZeta.N' 0 T :=    hpositive_nonneg.trans hpositive  have hpositive_abs :      (Nat.card {rho : NontrivialZeros //        0 < (rho : ℂ).im ∧ (rho : ℂ).im < T} : ℝ) ≤        |riemannZeta.N' 0 T| := by    rw [abs_of_nonneg hNprime_nonneg]    exact hpositive  have habsk := habs k  have hstep1 :      (Nat.card {rho : NontrivialZeros // |(rho : ℂ).im| < T} : ℝ) ≤        A * |riemannZeta.N' 0 T| := by    exact habsk.trans (mul_le_mul_of_nonneg_left hpositive_abs hA_nonneg)  have hstep2 :      A * |riemannZeta.N' 0 T| ≤        A * (B * |riemannZeta.N T|) := by    dsimp [T]    exact mul_le_mul_of_nonneg_left (hNprime k) hA_nonneg  calc    (Nat.card {rho : NontrivialZeros //        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ)        ≤ A * |riemannZeta.N' 0 T| := by          dsimp [T] at hstep1          exact hstep1    _ ≤ A * (B * |riemannZeta.N T|) := hstep2    _ = A * B * |riemannZeta.N ((2 : ℝ) ^ (k + 1))| := by          dsimp [T]          ring