contrapose! hx
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x ∈ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]
⊢ x ≠ 1
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
x : ℂ
hx : x = 1
⊢ x ∉ (fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]]