Brahmagupta-Fibonacci identity
Prove the Brahmagupta-Fibonacci identity \[ (a^2 + b^2)(c^2 + d^2) = (ac - bd)^2 + (ad + bc)^2 \]
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 := sorry
1. Proof in natural language
The proof follows from the following chain of equalities: \begin{align} (a^2 + b^2)(c^2 + d^2) &= a^2(c^2 + d^2) + b^2(c^2 + d^2) \newline &= (a^2c^2 + a^2d^2) + (b^2c^2 + b^2d^2) \newline &= ((ac)^2 + (bd)^2) + ((ad)^2 + (bc)^2) \newline &= ((ac)^2 - 2acbd + (bd)^2) + ((ad)^2 + 2adbc + (bc)^2) \newline &= (ac - bd)^2 + (ad + bc)^2 \end{align}
2. Proofs with Lean4
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (a b c d : ℝ) -- Proof 1 -- ======= example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 := calc (a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2) := right_distrib (a^2) (b^2) (c^2 + d^2) _ = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2) := congr_arg₂ (. + .) (left_distrib (a^2) (c^2) (d^2)) rfl _ = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2) := congr_arg₂ (. + .) rfl (left_distrib (b^2) (c^2) (d^2)) _ = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2) := by ring _ = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2) := by ring _ = (a*c - b*d)^2 + (a*d + b*c)^2 := by ring -- Proof 2 -- ======= example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 := by ring -- Used lemmas -- =========== -- variable (f : ℝ → ℝ → ℝ) -- variable (x x' y y' : ℝ) -- #check (congr_arg₂ f : x = x' → y = y' → f x y = f x' y') -- #check (left_distrib a b c : a * (b + c) = a * b + a * c) -- #check (right_distrib a b c: (a + b) * c = a * c + b * c)
You can interact with the previous proofs at Lean 4 Web.
3. Proofs with Isabelle/HOL
theory "Brahmagupta-Fibonacci_identity" imports Main HOL.Real begin (* Proof 1 *) lemma fixes a b c d :: real shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" proof - have "(a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)" by (simp only: distrib_right) also have "… = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)" by (simp only: distrib_left) also have "… = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)" by (simp only: distrib_left) also have "… = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)" by algebra also have "… = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)" by algebra also have "… = (a*c - b*d)^2 + (a*d + b*c)^2" by algebra finally show "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" . qed (* Proof 2 *) lemma fixes a b c d :: real shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" by algebra end
Note: The code for the previous proofs can be found in the Calculemus repository on GitHub.