feat(Archive/Imo): IMO 1963 Q5 (#18789)

proves the equality `cos (π / 7) - cos (2 * π / 7) + cos (3 * π / 7) = 1 / 2`.

Author: Rida-Hamadani

Archive.lean

@@ -12,6 +12,7 @@ import Archive.Imo.Imo1960Q2
 import Archive.Imo.Imo1961Q3
 import Archive.Imo.Imo1962Q1
 import Archive.Imo.Imo1962Q4
+import Archive.Imo.Imo1963Q5
 import Archive.Imo.Imo1964Q1
 import Archive.Imo.Imo1969Q1
 import Archive.Imo.Imo1972Q5

Archive/Imo/Imo1963Q5.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Rida Hamadani. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rida Hamadani
+-/
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
+
+/-!
+# IMO 1963 Q5
+
+Prove that `cos (π / 7) - cos (2 * π / 7) + cos (3 * π / 7) = 1 / 2`.
+
+The main idea of the proof is to multiply both sides by `2 * sin (π / 7)`, then the result follows
+through basic algebraic manipulations with the use of some trigonometric identities.
+
+-/
+
+open Real
+
+lemma two_sin_pi_div_seven_ne_zero : 2 * sin (π / 7) ≠ 0 := by
+  apply mul_ne_zero two_ne_zero (Real.sin_pos_of_pos_of_lt_pi _ _).ne' <;> linarith [pi_pos]
+
+lemma sin_pi_mul_neg_div (a b : ℝ) : sin (π * (- a / b)) = - sin (π * (a / b)) := by
+  ring_nf
+  exact sin_neg _
+
+theorem imo1963_q5 : cos (π / 7) - cos (2 * π / 7) + cos (3 * π / 7) = 1 / 2 := by
+  rw [← mul_right_inj' two_sin_pi_div_seven_ne_zero, mul_add, mul_sub, ← sin_two_mul,
+    two_mul_sin_mul_cos, two_mul_sin_mul_cos]
+  ring_nf
+  rw [← sin_pi_sub (π * (3 / 7)), sin_pi_mul_neg_div 2 7, sin_pi_mul_neg_div 1 7]
+  ring_nf

Mathlib/Data/Complex/Exponential.lean

@@ -759,6 +759,18 @@ nonrec theorem cos_sub_cos : cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x -
 nonrec theorem cos_add_cos : cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) :=
   ofReal_injective <| by simp [cos_add_cos]
 
+theorem two_mul_sin_mul_sin (x y : ℝ) : 2 * sin x * sin y = cos (x - y) - cos (x + y) := by
+  simp [cos_add, cos_sub]
+  ring
+
+theorem two_mul_cos_mul_cos (x y : ℝ) : 2 * cos x * cos y = cos (x - y) + cos (x + y) := by
+  simp [cos_add, cos_sub]
+  ring
+
+theorem two_mul_sin_mul_cos (x y : ℝ) : 2 * sin x * cos y = sin (x - y) + sin (x + y) := by
+  simp [sin_add, sin_sub]
+  ring
+
 nonrec theorem tan_eq_sin_div_cos : tan x = sin x / cos x :=
   ofReal_injective <| by simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin,
     ofReal_cos]
@@ -1487,3 +1499,5 @@ theorem abs_exp_eq_iff_re_eq {x y : ℂ} : abs (exp x) = abs (exp y) ↔ x.re =
   rw [abs_exp, abs_exp, Real.exp_eq_exp]
 
 end Complex
+
+set_option linter.style.longFile 1700