MAT3253 Complex Variables

1.3. Cardano equation🔗

Equation from Philip Ording's book "99 variations on a proof"

Show that the cubic equation x^3-6x^2+11x-6=2x-2 has solutions 1 and 4.

The following is yet another proof that

1 and 4 are solutions, and
there is no other solution.

section Cardano

/-- Prove that 1 and 4 satisfy Cardano's equation
-/
theorem cardano1 {x:ℝ}: x=1 ∨ x=4
    → x^3-6*x^2+11*x-6=2*x-2 := byx:ℝ⊢ x = 1 ∨ x = 4 → x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2
  intro hx:ℝh:x = 1 ∨ x = 4⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2
  obtain h1|h4 := hinlx:ℝh1:x = 1⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2inrx:ℝh4:x = 4⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2
  ·inlx:ℝh1:x = 1⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2 -- assume x=1
    rw [h1]inlx:ℝh1:x = 1⊢ 1 ^ 3 - 6 * 1 ^ 2 + 11 * 1 - 6 = 2 * 1 - 2 ; ringAll goals completed! 🐙
  ·inrx:ℝh4:x = 4⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2 -- assume x=4
    rw [h4]inrx:ℝh4:x = 4⊢ 4 ^ 3 - 6 * 4 ^ 2 + 11 * 4 - 6 = 2 * 4 - 2 ; ringAll goals completed! 🐙

/-- Prove that if x satisfies the equation,
    then x is either 1 or 4
-/
theorem cardano2 {x:ℝ}: x^3-6*x^2+11*x-6=2*x-2
    → x=1 ∨ x=4 := byx:ℝ⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2 → x = 1 ∨ x = 4
  intro hx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2⊢ x = 1 ∨ x = 4

  -- factorize the polynomial
  have h1 : (x-4)*((x-1)*(x-1)) = 0 :=
    calc
      (x-4)*((x-1)*(x-1))
      = (x^3-6*x^2+11*x-6) - (2*x-2) := byx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2⊢ (x - 4) * ((x - 1) * (x - 1)) = x ^ 3 - 6 * x ^ 2 + 11 * x - 6 - (2 * x - 2) ringAll goals completed! 🐙
    _ = (2*x-2) - (2*x-2) := byx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 - (2 * x - 2) = 2 * x - 2 - (2 * x - 2) rw [h]All goals completed! 🐙
    _ = 0 := byx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2⊢ 2 * x - 2 - (2 * x - 2) = 0 ringAll goals completed! 🐙

  -- deduce x=4 ∨ x=1 from hypothesis h1
  obtain ha | hb := eq_zero_or_eq_zero_of_mul_eq_zero h1inlx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2h1:(x - 4) * ((x - 1) * (x - 1)) = 0ha:x - 4 = 0⊢ x = 1 ∨ x = 4inrx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2h1:(x - 4) * ((x - 1) * (x - 1)) = 0hb:(x - 1) * (x - 1) = 0⊢ x = 1 ∨ x = 4
  ·inlx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2h1:(x - 4) * ((x - 1) * (x - 1)) = 0ha:x - 4 = 0⊢ x = 1 ∨ x = 4 exact Or.inr (sub_eq_zero.mp ha)All goals completed! 🐙
  ·inrx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2h1:(x - 4) * ((x - 1) * (x - 1)) = 0hb:(x - 1) * (x - 1) = 0⊢ x = 1 ∨ x = 4 have h3 : x-1=0 ∨ x-1=0 :=
      eq_zero_or_eq_zero_of_mul_eq_zero hbinrx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2h1:(x - 4) * ((x - 1) * (x - 1)) = 0hb:(x - 1) * (x - 1) = 0h3:x - 1 = 0 ∨ x - 1 = 0⊢ x = 1 ∨ x = 4
    obtain h4 | h4 := h3inr.inlx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2h1:(x - 4) * ((x - 1) * (x - 1)) = 0hb:(x - 1) * (x - 1) = 0h4:x - 1 = 0⊢ x = 1 ∨ x = 4inr.inrx:ℝh:x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2h1:(x - 4) * ((x - 1) * (x - 1)) = 0hb:(x - 1) * (x - 1) = 0h4:x - 1 = 0⊢ x = 1 ∨ x = 4
    repeat exact Or.inl (sub_eq_zero.mp h4)All goals completed! 🐙

Combining thw above two, we obtain

/-- The solutions of Cardano's equation are
    precisely 1 and 4
-/
theorem cardano {x:ℝ}:
    x^3-6*x^2+11*x-6=2*x-2 ↔ x=1 ∨ x=4 := byx:ℝ⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2 ↔ x = 1 ∨ x = 4
  constructormpx:ℝ⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2 → x = 1 ∨ x = 4mprx:ℝ⊢ x = 1 ∨ x = 4 → x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2
  ·mpx:ℝ⊢ x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2 → x = 1 ∨ x = 4 exact cardano2All goals completed! 🐙
  ·mprx:ℝ⊢ x = 1 ∨ x = 4 → x ^ 3 - 6 * x ^ 2 + 11 * x - 6 = 2 * x - 2 exact cardano1All goals completed! 🐙

end Cardano