Theorem: RuesRealToReal (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
x : ℝ
⊢ (Rues n ↑x).im = 0
Tactic:
rw [Rues]
State after:
n : ℕ+
x : ℝ
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0

State before:
n : ℕ+
x : ℝ
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Tactic:
let h₀ := ContinuousLinearMap.map_tsum Complex.imCLM (RuesSummable n x)
State after:
n : ℕ+
x : ℝ
h₀ : imCLM (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial) =
  ∑' (z : ℕ), imCLM (↑x ^ (↑n * z) / ↑(↑n * z).factorial) :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0

State before:
n : ℕ+
x : ℝ
h₀ : imCLM (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial) =
  ∑' (z : ℕ), imCLM (↑x ^ (↑n * z) / ↑(↑n * z).factorial) :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Tactic:
simp only [imCLM_apply] at h₀
State after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0

State before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (∑' (k : ℕ), ↑x ^ (↑n * k) / ↑(↑n * k).factorial).im = 0
Tactic:
rw [h₀]
State after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0

State before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Tactic:
suffices h₁ : ∑' (z : ℕ), (x ^ (n * z) : ℂ).im / ↑(Nat.factorial (n * z)) = ∑' (z : ℕ), 0
State after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0

case h₁
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0

State before:
case h₁
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0
Tactic:
congr
State after:
case h₁.e_f
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (fun z => (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial) = fun z => 0

State before:
case h₁.e_f
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
⊢ (fun z => (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial) = fun z => 0
Tactic:
ext1 k
State after:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ (↑x ^ (↑n * k)).im / ↑(↑n * k).factorial = 0

State before:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ (↑x ^ (↑n * k)).im / ↑(↑n * k).factorial = 0
Tactic:
norm_cast at *
State after:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ 0 / ↑(↑n * k).factorial = 0

State before:
case h₁.e_f.h
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
k : ℕ
⊢ 0 / ↑(↑n * k).factorial = 0
Tactic:
simp only [zero_div]
State after:
no goals

State before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = ∑' (z : ℕ), 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Tactic:
rw [tsum_zero] at h₁
State after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0

State before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = 0
Tactic:
rw [←h₁]
State after:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial

State before:
n : ℕ+
x : ℝ
h₀ : (∑' (z : ℕ), ↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im :=
  ContinuousLinearMap.map_tsum imCLM (RuesSummable n ↑x)
h₁ : ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial = 0
⊢ ∑' (z : ℕ), (↑x ^ (↑n * z) / ↑(↑n * z).factorial).im = ∑' (z : ℕ), (↑x ^ (↑n * z)).im / ↑(↑n * z).factorial
Tactic:
simp only [div_natCast_im]
State after:
no goals