[Merged by Bors] - feat(100-theorems-list/16_abel_ruffini): The Abel-Ruffini Theorem

[tb65536]

It's done!

---

• depends on: [Merged by Bors] - feat(field_theory/abel_ruffini): Version of solvable_by_rad.is_solvable #7509
• depends on: [Merged by Bors] - feat(analysis/calculus/local_extr): A polynomial's roots are bounded by its derivative #7571
• depends on: [Merged by Bors] - feat(data/int/basic): sign raised to an odd power #7559

[benjamindavidson]

I put together the following restructure of real_roots_Phi_ge_aux to minimize the amount of work you have to do in its proof (this also involved making a slight alteration to the statement and proof of real_roots_Phi_ge_aux'):

lemma real_roots_Phi_ge_aux' (hab : b < a) : (a : ℝ) ^ 2 - a ^ 5 + b ≤ 0 :=
begin
  rw_mod_cast [sub_add_eq_add_sub, sub_nonpos],
  refine ((nat.add_le_add_iff_le_right 1 _ _).mp _).trans (nat.pow_le_pow_of_le_right
    (nat.one_le_of_lt hab) (bit1_le_bit1.mpr one_le_two)),
  rw add_assoc,
  apply (add_le_add (le_refl (a ^ 2)) (nat.succ_le_iff.mpr hab)).trans,
  suffices : ∀ c : ℤ, 0 ≤ c → c ^ 2 + c ≤ c ^ 3 + 1,
  { exact_mod_cast this a (int.coe_nat_nonneg a) },
  intros c hc,
  rw [←sub_nonneg, show c ^ 3 + 1 - (c ^ 2 + c) = (c - 1) ^ 2 * (c + 1), by ring],
  exact mul_nonneg (pow_two_nonneg _) (add_nonneg hc zero_le_one),
end

lemma real_roots_Phi_ge_aux (hab : b < a) :
  ∃ x y : ℝ, x ≠ y ∧ aeval x (Φ ℚ a b) = 0 ∧ aeval y (Φ ℚ a b) = 0 :=
begin
  let f := λ x : ℝ, aeval x (Φ ℚ a b),
  have hf : f = λ x, x ^ 5 - a * x + b, { simp [f, Φ] },
  have hc : ∀ s : set ℝ, continuous_on f s := λ s, (Φ ℚ a b).continuous_on_aeval,
  have ha : (1 : ℝ) ≤ a := nat.one_le_cast.mpr (nat.one_le_of_lt hab),
  have hle : (0 : ℝ) ≤ 1, { exact_mod_cast zero_le_one' },
  have hf0 : 0 ≤ f 0, { norm_num [hf] },
  by_cases hb : (1 : ℝ) - a + b < 0,
  { have hf1 : f 1 < 0, { norm_num [hf, hb] },
    have hfa : 0 ≤ f a,
    { simp_rw [hf, ← sq],
      refine add_nonneg (sub_nonneg.mpr (pow_le_pow ha _)) _; norm_num },
    obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (set.mem_Ioc.mpr ⟨hf1, hf0⟩),
    obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (set.mem_Ioc.mpr ⟨hf1, hfa⟩),
    exact ⟨x, y, (hx1.trans hy1).ne, hx2, hy2⟩ },
  { have hb' : (1 : ℝ) - a + b = 0,
    { refine le_antisymm _ (not_lt.mp hb),
      rw [sub_add_eq_add_sub, sub_nonpos, add_comm],
      exact_mod_cast nat.succ_le_iff.mpr hab },
    have hf1 : f 1 = 0, { norm_num [hf, hb'] },
    have hfa : f (-a) ≤ 0, { norm_num [hf, ← sq, real_roots_Phi_ge_aux' a b hab] },
    have ha' := neg_nonpos.mpr (hle.trans ha),
    obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Icc ha' (hc _) (set.mem_Icc.mpr ⟨hfa, hf0⟩),
    exact ⟨x, 1, (hx1.trans_lt zero_lt_one).ne, hx2, hf1⟩ },
end

[tb65536]

@benjamindavidson Thanks! I managed to further golf the new version of real_roots_Phi_ge_aux'.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests