Theorem: f_ne_zero (Ray/Dynamics/Multibrot/Iterates.lean)

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ z ^ d + c ≠ 0
Tactic:
rw [← Complex.abs.ne_zero_iff]
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ d + c) ≠ 0

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ Complex.abs (z ^ d + c) ≠ 0
Tactic:
apply ne_of_gt
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)
Tactic:
have z1 : 1 ≤ abs z := le_trans (by norm_num) z3
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ 0 < Complex.abs (z ^ d + c)
Tactic:
calc abs (z ^ d + c)
  _ ≥ abs (z ^ d) - abs c := by bound
  _ = abs z ^ d - abs c := by rw [Complex.abs.map_pow]
  _ ≥ abs z ^ 2 - abs z := by bound
  _ = abs z * (abs z - 1) := by ring
  _ ≥ 3 * (3 - 1) := by bound
  _ > 0 := by norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
⊢ 1 ≤ 3
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs (z ^ d + c) ≥ Complex.abs (z ^ d) - Complex.abs c
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs (z ^ d) - Complex.abs c = Complex.abs z ^ d - Complex.abs c
Tactic:
rw [Complex.abs.map_pow]
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs z ^ d - Complex.abs c ≥ Complex.abs z ^ 2 - Complex.abs z
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs z ^ 2 - Complex.abs z = Complex.abs z * (Complex.abs z - 1)
Tactic:
ring
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ Complex.abs z * (Complex.abs z - 1) ≥ 3 * (3 - 1)
Tactic:
bound
State after:
no goals

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
cz : Complex.abs c ≤ Complex.abs z
z3 : 3 ≤ Complex.abs z
z1 : 1 ≤ Complex.abs z
⊢ 3 * (3 - 1) > 0
Tactic:
norm_num
State after:
no goals