∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) [inst_1 : NormedSpace ℂ E] (z : ℂ),
  DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
    BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
      z ∈ Complex.HadamardThreeLines.verticalStrip 0 1 → ‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip f z‖