theorem complex_trigonometric_function_definitions (z : ℂ) : Complex.cos z = (Complex.exp (Complex.I * z) + Complex.exp (-(Complex.I * z))) / 2 ∧ Complex.sin z = (Complex.exp (Complex.I * z) - Complex.exp (-(Complex.I * z))) / (2 * Complex.I)

Definition 4.7.1 (Trigonometric functions): for each z : ℂ, cos z = (exp (i z) + exp (-i z)) / 2 and sin z = (exp (i z) - exp (-i z)) / (2i).

theorem helperForProposition_4_7_1_abs_even_series_summable (x : ℝ) : Summable fun (n : ℕ) => |(-1) ^ n * x ^ (2 * n) / ↑(2 * n).factorial|

Helper for Proposition 4.7.1: the absolute-value even cosine-series coefficients are summable over ℝ.

theorem helperForProposition_4_7_1_abs_odd_series_summable (x : ℝ) : Summable fun (n : ℕ) => |(-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1).factorial|

Helper for Proposition 4.7.1: the absolute-value odd sine-series coefficients are summable over ℝ.

theorem helperForProposition_4_7_1_signed_series_summable (x : ℝ) : (Summable fun (n : ℕ) => (-1) ^ n * x ^ (2 * n) / ↑(2 * n).factorial) ∧ Summable fun (n : ℕ) => (-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1).factorial

Helper for Proposition 4.7.1: the signed cosine and sine coefficient series are summable over ℝ.

theorem helperForProposition_4_7_1_assemble_let_bound_goal (x : ℝ) : have a := fun (n : ℕ) => (-1) ^ n * x ^ (2 * n) / ↑(2 * n).factorial; have b := fun (n : ℕ) => (-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1).factorial; (Summable fun (n : ℕ) => |a n|) ∧ (Summable fun (n : ℕ) => |b n|) ∧ Summable a ∧ Summable b

Helper for Proposition 4.7.1: assemble the final conjunction for the let-bound series definitions.

theorem real_trigonometric_series_absolutely_convergent (x : ℝ) : have a := fun (n : ℕ) => (-1) ^ n * x ^ (2 * n) / ↑(2 * n).factorial; have b := fun (n : ℕ) => (-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1).factorial; (Summable fun (n : ℕ) => |a n|) ∧ (Summable fun (n : ℕ) => |b n|) ∧ Summable a ∧ Summable b

Proposition 4.7.1 (Reality and absolute convergence on ℝ): for every x : ℝ, the series ∑' n, (-1)^n * x^(2n) / (2n)! and ∑' n, (-1)^n * x^(2n+1) / (2n+1)! converge absolutely. Consequently, defining cos(x) and sin(x) by these series gives real-valued quantities for each real input.

theorem helperForProposition_4_7_2_eventually_ne_value_at_x0 (f : ℝ → ℝ) (x₀ : ℝ) (hf_diff : DifferentiableAt ℝ f x₀) (hf_deriv_ne_zero : deriv f x₀ ≠ 0) : ∀ᶠ (y : ℝ) in nhdsWithin x₀ {x₀}ᶜ, f y ≠ f x₀

Helper for Proposition 4.7.2: a nonzero derivative at x₀ forces nearby punctured points to have function value different from f x₀.

theorem helperForProposition_4_7_2_eventually_ne_zero (f : ℝ → ℝ) (x₀ : ℝ) (hf_zero : f x₀ = 0) (h_ne_value_at_x0 : ∀ᶠ (y : ℝ) in nhdsWithin x₀ {x₀}ᶜ, f y ≠ f x₀) : ∀ᶠ (y : ℝ) in nhdsWithin x₀ {x₀}ᶜ, f y ≠ 0

Helper for Proposition 4.7.2: rewriting local inequality against f x₀ as local inequality against 0 when f x₀ = 0.

theorem helperForProposition_4_7_2_radius_from_eventually_punctured (x₀ : ℝ) {P : ℝ → Prop} (hP : ∀ᶠ (y : ℝ) in nhdsWithin x₀ {x₀}ᶜ, P y) : ∃ c > 0, ∀ (y : ℝ), 0 < |y - x₀| ∧ |y - x₀| < c → P y

Helper for Proposition 4.7.2: an eventual punctured-neighborhood property yields a positive radius with the textbook 0 < |y - x₀| < c form.

theorem isolated_zero_of_differentiableAt_deriv_ne_zero (f : ℝ → ℝ) (x₀ : ℝ) (hf_diff : DifferentiableAt ℝ f x₀) (hf_zero : f x₀ = 0) (hf_deriv_ne_zero : deriv f x₀ ≠ 0) : ∃ c > 0, ∀ (y : ℝ), 0 < |y - x₀| ∧ |y - x₀| < c → f y ≠ 0

Proposition 4.7.2: If f : ℝ → ℝ is differentiable at x₀, with f x₀ = 0 and f' x₀ ≠ 0, then there exists c > 0 such that for every y : ℝ, 0 < |y - x₀| < c implies f y ≠ 0.

theorem exists_pos_radius_sine_ne_zero_right_of_zero : ∃ c > 0, ∀ (x : ℝ), 0 < x ∧ x < c → Real.sin x ≠ 0

Proposition 4.7.3: There exists a real number c > 0 such that for every real x with 0 < x < c, one has sin x ≠ 0.

theorem helperForTheorem_4_7_1_sine_mem_Icc (x : ℝ) : Real.sin x ∈ Set.Icc (-1) 1

Helper for Theorem 4.7.1: every real sine value lies in [-1, 1].

theorem helperForTheorem_4_7_1_cosine_mem_Icc (x : ℝ) : Real.cos x ∈ Set.Icc (-1) 1

Helper for Theorem 4.7.1: every real cosine value lies in [-1, 1].

theorem real_sine_cosine_pythagorean_identity_and_bounds (x : ℝ) : Real.sin x ^ 2 + Real.cos x ^ 2 = 1 ∧ Real.sin x ∈ Set.Icc (-1) 1 ∧ Real.cos x ∈ Set.Icc (-1) 1

Theorem 4.7.1: For every real number x, one has sin(x)^2 + cos(x)^2 = 1; in particular sin(x), cos(x) ∈ [-1, 1].

theorem helperForTheorem_4_7_2_sin_deriv_pointwise (x : ℝ) : deriv Real.sin x = Real.cos x

Helper for Theorem 4.7.2: pointwise derivative formula for Real.sin.

theorem helperForTheorem_4_7_2_cos_deriv_pointwise (x : ℝ) : deriv Real.cos x = -Real.sin x

Helper for Theorem 4.7.2: pointwise derivative formula for Real.cos.

theorem real_sine_cosine_derivative_formulas (x : ℝ) : deriv Real.sin x = Real.cos x ∧ deriv Real.cos x = -Real.sin x

Theorem 4.7.2: For every real number x, (Real.sin)'(x) = Real.cos x and (Real.cos)'(x) = -Real.sin x.

theorem real_sine_odd_and_cosine_even (x : ℝ) : Real.sin (-x) = -Real.sin x ∧ Real.cos (-x) = Real.cos x

Theorem 4.7.3: For every real number x, sin(-x) = -sin(x) and cos(-x) = cos(x).

theorem real_sine_cosine_addition_formulas (x y : ℝ) : Real.cos (x + y) = Real.cos x * Real.cos y - Real.sin x * Real.sin y ∧ Real.sin (x + y) = Real.sin x * Real.cos y + Real.cos x * Real.sin y

Theorem 4.7.4: For all real numbers x, y, cos(x + y) = cos(x)cos(y) - sin(x)sin(y) and sin(x + y) = sin(x)cos(y) + cos(x)sin(y).

theorem real_sine_and_cosine_at_zero : Real.sin 0 = 0 ∧ Real.cos 0 = 1

Theorem 4.7.5: We have sin(0) = 0 and cos(0) = 1.

theorem exists_positive_real_with_sine_zero : ∃ (x : ℝ), 0 < x ∧ Real.sin x = 0

Lemma 4.7.1: There exists a real number x > 0 such that sin x = 0.

noncomputable def firstPositiveSineZero : ℝ

Definition 4.7.2: Define π to be inf {x ∈ (0, ∞) : Real.sin x = 0}.

Equations

• firstPositiveSineZero = sInf {x : ℝ | x ∈ Set.Ioi 0 ∧ Real.sin x = 0}

noncomputable def tangentFunction : ↑(Set.Ioo (-(firstPositiveSineZero / 2)) (firstPositiveSineZero / 2)) → ℝ

Definition 4.7.3: The tangent function is the map tan : (-π/2, π/2) → ℝ defined by tan(x) = sin x / cos x.

Equations

• tangentFunction x = Real.sin ↑x / Real.cos ↑x

noncomputable def scaledCosineSeriesFunction : ℝ → ℝ

Definition 4.7.4: Define f : ℝ → ℝ by f(x) = ∑' n = 1..∞, 4^{-n} * cos(32^n * π * x). Equivalently (reindexing by n : ℕ), f(x) = ∑' n, (1 / 4^(n+1)) * cos(32^(n+1) * π * x).

Equations

• scaledCosineSeriesFunction x = ∑' (n : ℕ), 1 / 4 ^ (n + 1) * Real.cos (32 ^ (n + 1) * firstPositiveSineZero * x)

theorem helperForProposition_4_7_8_pi_le_of_positive_sine_zero (t : ℝ) (ht_pos : 0 < t) (ht_sin : Real.sin t = 0) : Real.pi ≤ t

Helper for Proposition 4.7.8: every positive real zero of Real.sin is at least π.

theorem helperForProposition_4_7_8_firstPositiveSineZero_eq_pi : firstPositiveSineZero = Real.pi

Helper for Proposition 4.7.8: the infimum defining firstPositiveSineZero equals π.

theorem helperForProposition_4_7_8_differentiableOn_tan_Ioo : DifferentiableOn ℝ Real.tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))

Helper for Proposition 4.7.8: Real.tan is differentiable on (-π/2, π/2).

theorem helperForProposition_4_7_8_deriv_tan_eq_one_add_tan_sq_on_Ioo (x : ℝ) : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) → deriv Real.tan x = 1 + Real.tan x ^ 2

Helper for Proposition 4.7.8: the derivative formula tan' = 1 + tan^2 on (-π/2, π/2).

theorem helperForProposition_4_7_8_bijective_tan_subtype : Function.Bijective fun (x : ↑(Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))) => Real.tan ↑x

Helper for Proposition 4.7.8: Real.tan is bijective from (-π/2, π/2) to ℝ.

theorem tangent_differentiableOn_deriv_strictMono_limits_and_bijective : DifferentiableOn ℝ (fun (x : ℝ) => Real.sin x / Real.cos x) (Set.Ioo (-(firstPositiveSineZero / 2)) (firstPositiveSineZero / 2)) ∧ (∀ x ∈ Set.Ioo (-(firstPositiveSineZero / 2)) (firstPositiveSineZero / 2), deriv (fun (y : ℝ) => Real.sin y / Real.cos y) x = 1 + (Real.sin x / Real.cos x) ^ 2) ∧ StrictMonoOn (fun (x : ℝ) => Real.sin x / Real.cos x) (Set.Ioo (-(firstPositiveSineZero / 2)) (firstPositiveSineZero / 2)) ∧ Filter.Tendsto (fun (x : ℝ) => Real.sin x / Real.cos x) (nhdsWithin (firstPositiveSineZero / 2) (Set.Iio (firstPositiveSineZero / 2))) Filter.atTop ∧ Filter.Tendsto (fun (x : ℝ) => Real.sin x / Real.cos x) (nhdsWithin (-(firstPositiveSineZero / 2)) (Set.Ioi (-(firstPositiveSineZero / 2)))) Filter.atBot ∧ Function.Bijective fun (x : ↑(Set.Ioo (-(firstPositiveSineZero / 2)) (firstPositiveSineZero / 2))) => Real.sin ↑x / Real.cos ↑x

Proposition 4.7.8: Define tan : (-π/2, π/2) → ℝ by tan(x) = sin x / cos x. Then tan is differentiable on (-π/2, π/2) and (d/dx) tan(x) = 1 + tan(x)^2 for x ∈ (-π/2, π/2). In particular, tan is strictly increasing on (-π/2, π/2), lim_{x→(π/2)^-} tan(x) = +∞, lim_{x→(-π/2)^+} tan(x) = -∞, and hence tan is a bijection from (-π/2, π/2) onto ℝ.

theorem helperForProposition_4_7_9_differentiable_arctan_global : Differentiable ℝ Real.arctan

Helper for Proposition 4.7.9: Real.arctan is differentiable on all real numbers.

theorem helperForProposition_4_7_9_deriv_arctan_pointwise (x : ℝ) : deriv Real.arctan x = 1 / (1 + x ^ 2)

Helper for Proposition 4.7.9: pointwise derivative formula for Real.arctan.

theorem helperForProposition_4_7_9_deriv_arctan_pointwise_alt (x : ℝ) : deriv Real.arctan x = 1 / (1 + x ^ 2)

Helper for Proposition 4.7.9: alternate pointwise derivative formula from Real.deriv_arctan.

theorem arctan_differentiable_and_deriv : Differentiable ℝ Real.arctan ∧ ∀ (x : ℝ), deriv Real.arctan x = 1 / (1 + x ^ 2)

Proposition 4.7.9: Let tan⁻¹ : ℝ → (-π/2, π/2) be the inverse of tan : (-π/2, π/2) → ℝ. Then Real.arctan is differentiable on ℝ and for every x : ℝ, (d/dx) arctan(x) = 1 / (1 + x^2).

theorem arctan_eq_tsum_powerSeries_of_abs_lt_one {x : ℝ} (hx : |x| < 1) : Real.arctan x = ∑' (n : ℕ), (-1) ^ n * x ^ (2 * n + 1) / (2 * ↑n + 1)

Proposition 4.7.10: For every real number x with |x| < 1, the arctangent function has the power series expansion arctan x = ∑' n, (-1)^n * x^(2n+1) / (2n+1).

theorem helperForProposition_4_7_4_positiveSineZeroSet_nonempty_bddBelow : {t : ℝ | t ∈ Set.Ioi 0 ∧ Real.sin t = 0}.Nonempty ∧ BddBelow {t : ℝ | t ∈ Set.Ioi 0 ∧ Real.sin t = 0}

Helper for Proposition 4.7.4: the positive-zero set used in the definition of firstPositiveSineZero is nonempty and bounded below.

theorem helperForProposition_4_7_4_pi_le_of_positive_sine_zero (t : ℝ) (ht_pos : 0 < t) (ht_sin : Real.sin t = 0) : Real.pi ≤ t

Helper for Proposition 4.7.4: every positive real zero of Real.sin is at least π.

theorem helperForProposition_4_7_4_firstPositiveSineZero_eq_pi : firstPositiveSineZero = Real.pi

Helper for Proposition 4.7.4: the definition of firstPositiveSineZero agrees with the standard constant Real.pi.

theorem helperForProposition_4_7_4_exists_angle_in_Ioc_neg_pi_pi (x y : ℝ) (hxy : x ^ 2 + y ^ 2 = 1) : ∃ θ ∈ Set.Ioc (-Real.pi) Real.pi, Real.sin θ = x ∧ Real.cos θ = y

Helper for Proposition 4.7.4: existence of an angle in (-π, π] with prescribed sin and cos coordinates on the unit circle.

theorem helperForProposition_4_7_4_angle_unique_in_Ioc_neg_pi_pi (x y θ₁ θ₂ : ℝ) (hθ₁ : θ₁ ∈ Set.Ioc (-Real.pi) Real.pi) (hθ₂ : θ₂ ∈ Set.Ioc (-Real.pi) Real.pi) (hsin₁ : Real.sin θ₁ = x) (hcos₁ : Real.cos θ₁ = y) (hsin₂ : Real.sin θ₂ = x) (hcos₂ : Real.cos θ₂ = y) : θ₁ = θ₂

Helper for Proposition 4.7.4: uniqueness of the angle in (-π, π] with fixed sin and cos values.

theorem existsUnique_angle_in_Ioc_neg_pi_pi_of_sq_add_sq_eq_one (x y : ℝ) (hxy : x ^ 2 + y ^ 2 = 1) : ∃! θ : ℝ, θ ∈ Set.Ioc (-firstPositiveSineZero) firstPositiveSineZero ∧ Real.sin θ = x ∧ Real.cos θ = y

Proposition 4.7.4: If x, y : ℝ satisfy x^2 + y^2 = 1, then there exists a unique θ ∈ (-π, π] such that sin θ = x and cos θ = y.

theorem helperForProposition_4_7_5_norm_exp_I_mul_real (x : ℝ) : ‖Complex.exp (Complex.I * ↑x)‖ = 1

Helper for Proposition 4.7.5: the norm of exp(i x) is 1 for real x.

theorem helperForProposition_4_7_5_radius_eq_of_scaled_exp_eq (r s θ α : ℝ) (hr : 0 < r) (hs : 0 < s) (hEq : ↑r * Complex.exp (Complex.I * ↑θ) = ↑s * Complex.exp (Complex.I * ↑α)) : r = s

Helper for Proposition 4.7.5: equality of scaled polar exponentials with positive radii forces equality of radii.

theorem helperForProposition_4_7_5_exp_eq_of_radius_eq (r s θ α : ℝ) (hr : 0 < r) (hrs : r = s) (hEq : ↑r * Complex.exp (Complex.I * ↑θ) = ↑s * Complex.exp (Complex.I * ↑α)) : Complex.exp (Complex.I * ↑θ) = Complex.exp (Complex.I * ↑α)

Helper for Proposition 4.7.5: after identifying radii, one can cancel the nonzero real scalar and deduce equality of the exponential factors.

theorem helperForProposition_4_7_5_angle_shift_of_exp_I_eq (θ α : ℝ) (hExpEq : Complex.exp (Complex.I * ↑θ) = Complex.exp (Complex.I * ↑α)) : ∃ (k : ℤ), θ = α + 2 * Real.pi * ↑k

Helper for Proposition 4.7.5: equality of exp(iθ) and exp(iα) forces an integer 2π angle shift between θ and α.

theorem complex_polar_exp_eq_iff (r s θ α : ℝ) (hr : 0 < r) (hs : 0 < s) (hEq : ↑r * Complex.exp (Complex.I * ↑θ) = ↑s * Complex.exp (Complex.I * ↑α)) : r = s ∧ ∃ (k : ℤ), θ = α + 2 * Real.pi * ↑k

Proposition 4.7.5: if r, s > 0 and θ, α : ℝ satisfy (r : ℂ) * exp(iθ) = (s : ℂ) * exp(iα), then r = s and θ = α + 2πk for some k : ℤ.

theorem helperForProposition_4_7_6_exists_polar_witness (z : ℂ) (hz : z ≠ 0) : ∃ (p : ℝ × ℝ), 0 < p.1 ∧ p.2 ∈ Set.Ioc (-firstPositiveSineZero) firstPositiveSineZero ∧ z = ↑p.1 * Complex.exp (Complex.I * ↑p.2)

Helper for Proposition 4.7.6: the canonical witness (‖z‖, arg z) satisfies the required positivity, interval, and reconstruction properties.

theorem helperForProposition_4_7_6_int_shift_zero_of_interval_bounds {θ α : ℝ} {k : ℤ} (hθ : θ ∈ Set.Ioc (-firstPositiveSineZero) firstPositiveSineZero) (hα : α ∈ Set.Ioc (-firstPositiveSineZero) firstPositiveSineZero) (hEq : θ = α + 2 * Real.pi * ↑k) : k = 0

Helper for Proposition 4.7.6: if two angles lie in (-π, π] and differ by an integer multiple of 2π, then the integer shift is zero.

theorem helperForProposition_4_7_6_radius_angle_unique {z : ℂ} {r s θ α : ℝ} (hr : 0 < r) (hs : 0 < s) (hθ : θ ∈ Set.Ioc (-firstPositiveSineZero) firstPositiveSineZero) (hα : α ∈ Set.Ioc (-firstPositiveSineZero) firstPositiveSineZero) (hEqR : z = ↑r * Complex.exp (Complex.I * ↑θ)) (hEqS : z = ↑s * Complex.exp (Complex.I * ↑α)) : r = s ∧ θ = α

Helper for Proposition 4.7.6: two admissible polar representations of the same nonzero complex number have identical radius and angle.

theorem complex_existsUnique_polar_coordinates_Ioc (z : ℂ) (hz : z ≠ 0) : ∃! p : ℝ × ℝ, 0 < p.1 ∧ p.2 ∈ Set.Ioc (-firstPositiveSineZero) firstPositiveSineZero ∧ z = ↑p.1 * Complex.exp (Complex.I * ↑p.2)

Proposition 4.7.6: for every nonzero complex number z, there exists a unique pair (r, θ) with r > 0 and θ ∈ (-π, π] (where π is firstPositiveSineZero) such that z = r * exp(iθ).

theorem helperForTheorem_4_7_6_exp_I_mul_ofReal (x : ℝ) : Complex.exp (Complex.I * ↑x) = ↑(Real.cos x) + Complex.I * ↑(Real.sin x)

Helper for Theorem 4.7.6: Euler's formula in the exp(i x) direction for real x.

theorem helperForTheorem_4_7_6_exp_neg_I_mul_ofReal (x : ℝ) : Complex.exp (-Complex.I * ↑x) = ↑(Real.cos x) - Complex.I * ↑(Real.sin x)

Helper for Theorem 4.7.6: Euler's formula in the exp(-i x) direction for real x.

theorem helperForTheorem_4_7_6_re_im_of_exp_I_mul (x : ℝ) : Real.cos x = (Complex.exp (Complex.I * ↑x)).re ∧ Real.sin x = (Complex.exp (Complex.I * ↑x)).im

Helper for Theorem 4.7.6: real and imaginary parts of exp(i x) for real x.

theorem real_euler_formula_and_real_imag_parts (x : ℝ) : Complex.exp (Complex.I * ↑x) = ↑(Real.cos x) + Complex.I * ↑(Real.sin x) ∧ Complex.exp (-Complex.I * ↑x) = ↑(Real.cos x) - Complex.I * ↑(Real.sin x) ∧ Real.cos x = (Complex.exp (Complex.I * ↑x)).re ∧ Real.sin x = (Complex.exp (Complex.I * ↑x)).im

Theorem 4.7.6: for every real number x, exp(ix) = cos(x) + i sin(x) and exp(-ix) = cos(x) - i sin(x). In particular, cos(x) = Re(exp(ix)) and sin(x) = Im(exp(ix)).

theorem helperForProposition_4_7_7_base_as_exp (θ : ℝ) : ↑(Real.cos θ) + Complex.I * ↑(Real.sin θ) = Complex.exp (Complex.I * ↑θ)

Helper for Proposition 4.7.7: rewrite cos θ + i sin θ as exp(iθ).

theorem helperForProposition_4_7_7_exp_int_argument_rewrite (θ : ℝ) (n : ℤ) : ↑n * (Complex.I * ↑θ) = Complex.I * ↑(↑n * θ)

Helper for Proposition 4.7.7: normalize the scaled exponential argument for integer powers.

theorem helperForProposition_4_7_7_power_as_exp_scaled (θ : ℝ) (n : ℤ) : (↑(Real.cos θ) + Complex.I * ↑(Real.sin θ)) ^ n = Complex.exp (Complex.I * ↑(↑n * θ))

Helper for Proposition 4.7.7: convert (cos θ + i sin θ)^n to one exponential at argument (n : ℝ) * θ.

theorem helperForProposition_4_7_7_re_im_from_power (θ : ℝ) (n : ℤ) : Real.cos (↑n * θ) = ((↑(Real.cos θ) + Complex.I * ↑(Real.sin θ)) ^ n).re ∧ Real.sin (↑n * θ) = ((↑(Real.cos θ) + Complex.I * ↑(Real.sin θ)) ^ n).im

Helper for Proposition 4.7.7: identify cos(nθ) and sin(nθ) as the real and imaginary parts of (cos θ + i sin θ)^n.

theorem de_moivre_identities_integer_powers (θ : ℝ) (n : ℤ) : Real.cos (↑n * θ) = ((↑(Real.cos θ) + Complex.I * ↑(Real.sin θ)) ^ n).re ∧ Real.sin (↑n * θ) = ((↑(Real.cos θ) + Complex.I * ↑(Real.sin θ)) ^ n).im ∧ (↑(Real.cos θ) + Complex.I * ↑(Real.sin θ)) ^ n = ↑(Real.cos (↑n * θ)) + Complex.I * ↑(Real.sin (↑n * θ))

Proposition 4.7.7 (de Moivre identities): for every θ : ℝ and n : ℤ, cos(nθ) and sin(nθ) are the real and imaginary parts of (cos θ + i sin θ)^n; equivalently, (cos θ + i sin θ)^n = cos(nθ) + i sin(nθ).

theorem helperForTheorem_4_7_7_positiveSineZeroSet_nonempty_bddBelow : {x : ℝ | x ∈ Set.Ioi 0 ∧ Real.sin x = 0}.Nonempty ∧ BddBelow {x : ℝ | x ∈ Set.Ioi 0 ∧ Real.sin x = 0}

Helper for Theorem 4.7.7: the positive sine-zero set is nonempty and bounded below.

theorem helperForTheorem_4_7_7_pi_is_lower_bound_of_positive_sine_zeros (y : ℝ) (hy_pos : 0 < y) (hy_sin : Real.sin y = 0) : Real.pi ≤ y

Helper for Theorem 4.7.7: every positive real zero of sine is at least π.

theorem helperForTheorem_4_7_7_firstPositiveSineZero_eq_pi : firstPositiveSineZero = Real.pi

Helper for Theorem 4.7.7: the definition of firstPositiveSineZero agrees with Real.pi.

theorem helperForTheorem_4_7_7_transport_antiperiodic_periodic (hpi : firstPositiveSineZero = Real.pi) : (∀ (x : ℝ), Real.cos (x + firstPositiveSineZero) = -Real.cos x ∧ Real.sin (x + firstPositiveSineZero) = -Real.sin x) ∧ (∀ (x : ℝ), Real.cos (x + 2 * firstPositiveSineZero) = Real.cos x ∧ Real.sin (x + 2 * firstPositiveSineZero) = Real.sin x) ∧ Function.Periodic Real.cos (2 * firstPositiveSineZero) ∧ Function.Periodic Real.sin (2 * firstPositiveSineZero)

Helper for Theorem 4.7.7: transport π-identities to firstPositiveSineZero.

theorem real_sine_cosine_pi_antiperiodicity_and_two_pi_periodicity : (∀ (x : ℝ), Real.cos (x + firstPositiveSineZero) = -Real.cos x ∧ Real.sin (x + firstPositiveSineZero) = -Real.sin x) ∧ (∀ (x : ℝ), Real.cos (x + 2 * firstPositiveSineZero) = Real.cos x ∧ Real.sin (x + 2 * firstPositiveSineZero) = Real.sin x) ∧ Function.Periodic Real.cos (2 * firstPositiveSineZero) ∧ Function.Periodic Real.sin (2 * firstPositiveSineZero)

Theorem 4.7.7: For every real number x (with π from Definition 4.7.2), cos (x + π) = -cos x and sin (x + π) = -sin x. In particular, cos (x + 2π) = cos x and sin (x + 2π) = sin x, so sin and cos are periodic with period 2π.

theorem helperForTheorem_4_7_8_firstPositiveSineZero_ne_zero : firstPositiveSineZero ≠ 0

Helper for Theorem 4.7.8: firstPositiveSineZero is nonzero.

theorem helperForTheorem_4_7_8_div_eq_int_iff_mul_eq_int_pi (x : ℝ) (n : ℤ) : x / firstPositiveSineZero = ↑n ↔ x = ↑n * Real.pi

Helper for Theorem 4.7.8: divide-by-firstPositiveSineZero form equals integer-multiple-of-π form.

theorem helperForTheorem_4_7_8_exists_div_eq_int_iff_exists_mul_eq_int_pi (x : ℝ) : (∃ (n : ℤ), x / firstPositiveSineZero = ↑n) ↔ ∃ (n : ℤ), x = ↑n * Real.pi

Helper for Theorem 4.7.8: the integer-existence formulations using division by firstPositiveSineZero and multiplication by π are equivalent.

theorem real_sine_eq_zero_iff_div_firstPositiveSineZero_integer (x : ℝ) : Real.sin x = 0 ↔ ∃ (n : ℤ), x / firstPositiveSineZero = ↑n

Theorem 4.7.8: For every real number x (with π given by Definition 4.7.2), Real.sin x = 0 if and only if x / π is an integer.