ComputationsChoiceExponent.ζ_neg_iff_aux₀

lemma ζ_neg_iff_aux₀ (ht : t ∈ Ioo 0 1) (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₁ : 0 < p₁) (hq₁ : 0 < q₁)    (hp₀p₁ : p₀ ≠ p₁) (hq₀q₁ : q₀ ≠ q₁) :    (ζ p₀ q₀ p₁ q₁ t.toReal) < 0 ↔      q₀⁻¹.toReal < q₁⁻¹.toReal ∧ p₁⁻¹.toReal < p₀⁻¹.toReal ∨      q₁⁻¹.toReal < q₀⁻¹.toReal ∧ p₀⁻¹.toReal < p₁⁻¹.toReal := by  unfold ζ  rw [div_neg_iff, ← Left.neg_pos_iff, ← Left.neg_pos_iff, neg_mul_eq_mul_neg, neg_mul_eq_mul_neg]  rw [mul_pos_iff_of_pos_left, mul_pos_iff_of_pos_left,      mul_pos_iff_of_pos_left, mul_pos_iff_of_pos_left, neg_sub, neg_sub]  · simp only [sub_pos]  · exact preservation_positivity_inv_toReal ht hq₀ hq₁ hq₀q₁  · exact preservation_positivity_inv_toReal ht hp₀ hp₁ hp₀p₁  · exact preservation_positivity_inv_toReal ht hq₀ hq₁ hq₀q₁  · exact preservation_positivity_inv_toReal ht hp₀ hp₁ hp₀p₁