[GOAL]
f : ℂ[X]
hf : 0 < degree f
⊢ ∃ z, IsRoot f z
[PROOFSTEP]
contrapose! hf
[GOAL]
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
⊢ degree f ≤ 0
[PROOFSTEP]
have : Metric.Bounded (Set.range (eval · f)⁻¹)
[GOAL]
case this
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
⊢ Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
[PROOFSTEP]
obtain ⟨z₀, h₀⟩ := f.exists_forall_norm_le
[GOAL]
case this.intro
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
z₀ : ℂ
h₀ : ∀ (y : ℂ), ‖eval z₀ f‖ ≤ ‖eval y f‖
⊢ Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
[PROOFSTEP]
simp only [Pi.inv_apply, bounded_iff_forall_norm_le, Set.forall_range_iff, norm_inv]
[GOAL]
case this.intro
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
z₀ : ℂ
h₀ : ∀ (y : ℂ), ‖eval z₀ f‖ ≤ ‖eval y f‖
⊢ ∃ C, ∀ (i : ℂ), ‖eval i f‖⁻¹ ≤ C
[PROOFSTEP]
exact ⟨‖eval z₀ f‖⁻¹, fun z => inv_le_inv_of_le (norm_pos_iff.2 <| hf z₀) (h₀ z)⟩
[GOAL]
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
this : Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
⊢ degree f ≤ 0
[PROOFSTEP]
obtain ⟨c, hc⟩ := (f.differentiable.inv hf).exists_const_forall_eq_of_bounded this
[GOAL]
case intro
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
this : Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
c : ℂ
hc : ∀ (z : ℂ), (eval z f)⁻¹ = c
⊢ degree f ≤ 0
[PROOFSTEP]
obtain rfl : f = C c⁻¹ := Polynomial.funext fun z => by rw [eval_C, ← hc z, inv_inv]
[GOAL]
f : ℂ[X]
hf : ∀ (z : ℂ), ¬IsRoot f z
this : Metric.Bounded (Set.range (fun x => eval x f)⁻¹)
c : ℂ
hc : ∀ (z : ℂ), (eval z f)⁻¹ = c
z : ℂ
⊢ eval z f = eval z (↑C c⁻¹)
[PROOFSTEP]
rw [eval_C, ← hc z, inv_inv]
[GOAL]
case intro
c : ℂ
hf : ∀ (z : ℂ), ¬IsRoot (↑C c⁻¹) z
this : Metric.Bounded (Set.range (fun x => eval x (↑C c⁻¹))⁻¹)
hc : ∀ (z : ℂ), (eval z (↑C c⁻¹))⁻¹ = c
⊢ degree (↑C c⁻¹) ≤ 0
[PROOFSTEP]
exact degree_C_le
