apply (Real.rpow_le_rpow_iff (z := 4) (by norm_num) ?_ (by norm_num)).mp
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖
σ t : ℝ
σ_gt : 1 < σ
⊢ 1 ^ 4 ≤ (‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖) ^ 4

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 ≤ ‖ζ ↑σ‖ ^ (3 / 4) * ‖ζ (↑σ + 2 * ↑t * I)‖ ^ (1 / 4) * ‖ζ (↑σ + ↑t * I)‖

σ t : ℝ
σ_gt : 1 < σ
⊢ 0 < ‖ζ (↑σ + ↑t * I)‖