Kadiri.zeroImagDyadicCumulativeCountByNWithZeroHeightSource_of_positive_bridge

theorem zeroImagDyadicCumulativeCountByNWithZeroHeightSource_of_positive_bridge    (habs : zeroImagDyadicAbsToPositiveCountWithZeroHeightSource)    (hNprime : zeroImagDyadicNPrimeToNSource) :    zeroImagDyadicCumulativeCountByNWithZeroHeightSource := by  rcases habs with ⟨A, D, hA_nonneg, hD_nonneg, habs⟩  rcases hNprime with ⟨B, hB_nonneg, hNprime⟩  refine ⟨A * B, D, mul_nonneg hA_nonneg hB_nonneg, hD_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| + D := by    have habskT :        (Nat.card {rho : NontrivialZeros // |(rho : ℂ).im| < T} : ℝ) ≤          A * (Nat.card {rho : NontrivialZeros //            0 < (rho : ℂ).im ∧ (rho : ℂ).im < T} : ℝ) + D := by      dsimp [T]      exact habsk    have hmul :=      mul_le_mul_of_nonneg_left hpositive_abs hA_nonneg    calc      (Nat.card {rho : NontrivialZeros // |(rho : ℂ).im| < T} : ℝ)          ≤ A * (Nat.card {rho : NontrivialZeros //            0 < (rho : ℂ).im ∧ (rho : ℂ).im < T} : ℝ) + D := habskT      _ ≤ A * |riemannZeta.N' 0 T| + D := add_le_add_left hmul D  have hstep2 :      A * |riemannZeta.N' 0 T| + D ≤        A * (B * |riemannZeta.N T|) + D := by    have hNprimeT : |riemannZeta.N' 0 T| ≤ B * |riemannZeta.N T| := by      dsimp [T]      exact hNprime k    have hmul :=      mul_le_mul_of_nonneg_left hNprimeT hA_nonneg    exact add_le_add_left hmul D  calc    (Nat.card {rho : NontrivialZeros //        |(rho : ℂ).im| < (2 : ℝ) ^ (k + 1)} : ℝ)        ≤ A * |riemannZeta.N' 0 T| + D := by          dsimp [T] at hstep1          exact hstep1    _ ≤ A * (B * |riemannZeta.N T|) + D := hstep2    _ = A * B * |riemannZeta.N ((2 : ℝ) ^ (k + 1))| + D := by          dsimp [T]          ring