p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ IsCauSeq norm newton_seq
intro ε hε
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
cases' bound hnorm hε with N hN
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∀ (j : ℕ), j ≥ N → ‖newton_seq j - newton_seq N‖ < ε
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
exists N
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ < ε
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∀ (j : ℕ), j ≥ N → ‖newton_seq j - newton_seq N‖ < ε
intro j hj
case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ ≤ ?intro.b

case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ?intro.b < ε

case intro.b
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ℝ
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ < ε
apply lt_of_le_of_lt
no goals
case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ ≤ ?intro.b
apply newton_seq_dist hnorm hj
case intro.a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ N ≥ N
case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ N < ε
apply hN
no goals
case intro.a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ N ≥ N
exact le_rfl