[GOAL]
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
⊢ convergents (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents (of (Int.fract v)⁻¹) n
[PROOFSTEP]
rw [of_convergents_eq_convergents', convergents'_succ, of_convergents_eq_convergents']
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
⊢ ∀ (ε : K), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
intro ε ε_pos
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
rcases(exists_nat_gt (1 / ε) : ∃ N' : ℕ, 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
let N :=
  max N'
    5
      -- set minimum to 5 to have N ≤ fib N work
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
exists N
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
⊢ ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
intro n n_ge_N
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
let g := of v
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
cases' Decidable.em (g.TerminatedAt n) with terminated_at_n not_terminated_at_n
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
have : v = g.convergents n := of_correctness_of_terminatedAt terminated_at_n
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
this : v = convergents g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
have : v - g.convergents n = 0 := sub_eq_zero.mpr this
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
this✝ : v = convergents g n
this : v - convergents g n = 0
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
rw [this]
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
this✝ : v = convergents g n
this : v - convergents g n = 0
⊢ |0| < ε
[PROOFSTEP]
exact_mod_cast ε_pos
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
let B := g.denominators n
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
let nB := g.denominators (n + 1)
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
have abs_v_sub_conv_le : |v - g.convergents n| ≤ 1 / (B * nB) := abs_sub_convergents_le not_terminated_at_n
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
suffices : 1 / (B * nB) < ε
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
this : 1 / (B * nB) < ε
⊢ |v - convergents (of v) n| < ε
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
exact lt_of_le_of_lt abs_v_sub_conv_le this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have nB_ineq : (fib (n + 2) : K) ≤ nB :=
  haveI : ¬g.TerminatedAt (n + 1 - 1) := not_terminated_at_n
  succ_nth_fib_le_of_nth_denom (Or.inr this)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have B_ineq : (fib (n + 1) : K) ≤ B :=
  haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminated_at_n
  succ_nth_fib_le_of_nth_denom (Or.inr this)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have zero_lt_B : 0 < B :=
  haveI : (0 : K) < fib (n + 1) := by exact_mod_cast fib_pos n.zero_lt_succ
  lt_of_lt_of_le this B_ineq
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
⊢ 0 < ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast fib_pos n.zero_lt_succ
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have zero_lt_mul_conts : 0 < B * nB :=
  by
  have : 0 < nB :=
    haveI : (0 : K) < fib (n + 2) := by exact_mod_cast fib_pos (n + 1).zero_lt_succ
    lt_of_lt_of_le this nB_ineq
  solve_by_elim [mul_pos]
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ 0 < B * nB
[PROOFSTEP]
have : 0 < nB :=
  haveI : (0 : K) < fib (n + 2) := by exact_mod_cast fib_pos (n + 1).zero_lt_succ
  lt_of_lt_of_le this nB_ineq
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ 0 < ↑(fib (n + 2))
[PROOFSTEP]
exact_mod_cast fib_pos (n + 1).zero_lt_succ
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
this : 0 < nB
⊢ 0 < B * nB
[PROOFSTEP]
solve_by_elim [mul_pos]
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
suffices : 1 < ε * (B * nB)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
this : 1 < ε * (B * nB)
⊢ 1 / (B * nB) < ε
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * (B * nB)
[PROOFSTEP]
exact (div_lt_iff zero_lt_mul_conts).mpr this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * (B * nB)
[PROOFSTEP]
have one_lt_ε_mul_N : 1 < ε * n :=
  by
  have one_lt_ε_mul_N' : 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N'
  have : (N' : K) ≤ N := by exact_mod_cast le_max_left _ _
  have : ε * N' ≤ ε * n := (mul_le_mul_left ε_pos).mpr (le_trans this (by exact_mod_cast n_ge_N))
  exact lt_of_lt_of_le one_lt_ε_mul_N' this
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * ↑n
[PROOFSTEP]
have one_lt_ε_mul_N' : 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N'
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
⊢ 1 < ε * ↑n
[PROOFSTEP]
have : (N' : K) ≤ N := by exact_mod_cast le_max_left _ _
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
⊢ ↑N' ≤ ↑N
[PROOFSTEP]
exact_mod_cast le_max_left _ _
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
this : ↑N' ≤ ↑N
⊢ 1 < ε * ↑n
[PROOFSTEP]
have : ε * N' ≤ ε * n := (mul_le_mul_left ε_pos).mpr (le_trans this (by exact_mod_cast n_ge_N))
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
this : ↑N' ≤ ↑N
⊢ ↑N ≤ ↑n
[PROOFSTEP]
exact_mod_cast n_ge_N
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
this✝ : ↑N' ≤ ↑N
this : ε * ↑N' ≤ ε * ↑n
⊢ 1 < ε * ↑n
[PROOFSTEP]
exact lt_of_lt_of_le one_lt_ε_mul_N' this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ 1 < ε * (B * nB)
[PROOFSTEP]
suffices : ε * n ≤ ε * (B * nB)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
this : ε * ↑n ≤ ε * (B * nB)
⊢ 1 < ε * (B * nB)
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ε * ↑n ≤ ε * (B * nB)
[PROOFSTEP]
exact lt_of_lt_of_le one_lt_ε_mul_N this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ε * ↑n ≤ ε * (B * nB)
[PROOFSTEP]
suffices : (n : K) ≤ B * nB
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
this : ↑n ≤ B * nB
⊢ ε * ↑n ≤ ε * (B * nB)
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ B * nB
[PROOFSTEP]
exact (mul_le_mul_left ε_pos).mpr this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ B * nB
[PROOFSTEP]
show (n : K) ≤ B * nB
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ B * nB
[PROOFSTEP]
calc
  (n : K) ≤ fib n := by exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
  _ ≤ fib (n + 1) := by exact_mod_cast fib_le_fib_succ
  _ ≤ fib (n + 1) * fib (n + 1) := by exact_mod_cast (fib (n + 1)).le_mul_self
  _ ≤ fib (n + 1) * fib (n + 2) :=
    (mul_le_mul_of_nonneg_left (by exact_mod_cast fib_le_fib_succ) (by exact_mod_cast (fib (n + 1)).zero_le))
  _ ≤ B * nB := mul_le_mul B_ineq nB_ineq (by exact_mod_cast (fib (n + 2)).zero_le) (le_of_lt zero_lt_B)
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ ↑(fib n)
[PROOFSTEP]
exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑(fib n) ≤ ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast fib_le_fib_succ
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑(fib (n + 1)) ≤ ↑(fib (n + 1)) * ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast (fib (n + 1)).le_mul_self
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑(fib (n + 1)) ≤ ↑(fib (n + 2))
[PROOFSTEP]
exact_mod_cast fib_le_fib_succ
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ 0 ≤ ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast (fib (n + 1)).zero_le
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ 0 ≤ ↑(fib (n + 2))
[PROOFSTEP]
exact_mod_cast (fib (n + 2)).zero_le
[GOAL]
K : Type u_1
v : K
inst✝³ : LinearOrderedField K
inst✝² : FloorRing K
inst✝¹ : Archimedean K
inst✝ : OrderTopology K
⊢ Filter.Tendsto (convergents (of v)) Filter.atTop (nhds v)
[PROOFSTEP]
simpa [LinearOrderedAddCommGroup.tendsto_nhds, abs_sub_comm] using of_convergence_epsilon v
