[GOAL]
⊢ φ⁻¹ = -ψ
[PROOFSTEP]
have : 1 + Real.sqrt 5 ≠ 0 := ne_of_gt (add_pos (by norm_num) <| Real.sqrt_pos.mpr (by norm_num))
[GOAL]
⊢ 0 < 1
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 5
[PROOFSTEP]
norm_num
[GOAL]
this : 1 + sqrt 5 ≠ 0
⊢ φ⁻¹ = -ψ
[PROOFSTEP]
field_simp [sub_mul, mul_add]
[GOAL]
this : 1 + sqrt 5 ≠ 0
⊢ 2 * 2 = sqrt 5 * sqrt 5 - 1
[PROOFSTEP]
norm_num
[GOAL]
⊢ ψ⁻¹ = -φ
[PROOFSTEP]
rw [inv_eq_iff_eq_inv, ← neg_inv, ← neg_eq_iff_eq_neg]
[GOAL]
⊢ -ψ = φ⁻¹
[PROOFSTEP]
exact inv_gold.symm
[GOAL]
⊢ φ * ψ = -1
[PROOFSTEP]
field_simp
[GOAL]
⊢ (1 + sqrt 5) * (1 - sqrt 5) = -(2 * 2)
[PROOFSTEP]
rw [← sq_sub_sq]
[GOAL]
⊢ 1 ^ 2 - sqrt 5 ^ 2 = -(2 * 2)
[PROOFSTEP]
norm_num
[GOAL]
⊢ ψ * φ = -1
[PROOFSTEP]
rw [mul_comm]
[GOAL]
⊢ φ * ψ = -1
[PROOFSTEP]
exact gold_mul_goldConj
[GOAL]
⊢ φ + ψ = 1
[PROOFSTEP]
rw [goldenRatio, goldenConj]
[GOAL]
⊢ (1 + sqrt 5) / 2 + (1 - sqrt 5) / 2 = 1
[PROOFSTEP]
ring
[GOAL]
⊢ 1 - φ = ψ
[PROOFSTEP]
linarith [gold_add_goldConj]
[GOAL]
⊢ 1 - ψ = φ
[PROOFSTEP]
linarith [gold_add_goldConj]
[GOAL]
⊢ φ - ψ = sqrt 5
[PROOFSTEP]
rw [goldenRatio, goldenConj]
[GOAL]
⊢ (1 + sqrt 5) / 2 - (1 - sqrt 5) / 2 = sqrt 5
[PROOFSTEP]
ring
[GOAL]
⊢ φ ^ 2 = φ + 1
[PROOFSTEP]
rw [goldenRatio, ← sub_eq_zero]
[GOAL]
⊢ ((1 + sqrt 5) / 2) ^ 2 - ((1 + sqrt 5) / 2 + 1) = 0
[PROOFSTEP]
ring_nf
[GOAL]
⊢ sqrt 5 ^ 2 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
rw [Real.sq_sqrt]
[GOAL]
⊢ 5 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 ≤ 5
[PROOFSTEP]
norm_num
[GOAL]
⊢ ψ ^ 2 = ψ + 1
[PROOFSTEP]
rw [goldenConj, ← sub_eq_zero]
[GOAL]
⊢ ((1 - sqrt 5) / 2) ^ 2 - ((1 - sqrt 5) / 2 + 1) = 0
[PROOFSTEP]
ring_nf
[GOAL]
⊢ sqrt 5 ^ 2 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
rw [Real.sq_sqrt]
[GOAL]
⊢ 5 * (↑(Int.ofNat 1) / ↑4) + ↑(Int.negOfNat 5) * (↑(Int.ofNat 1) / ↑4) = 0
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 ≤ 5
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 1 + sqrt 5
[PROOFSTEP]
apply add_pos
[GOAL]
case ha
⊢ 0 < 1
[PROOFSTEP]
norm_num
[GOAL]
case hb
⊢ 0 < sqrt 5
[PROOFSTEP]
norm_num
[GOAL]
⊢ 1 < φ
[PROOFSTEP]
refine' lt_of_mul_lt_mul_left _ (le_of_lt gold_pos)
[GOAL]
⊢ φ * 1 < φ * φ
[PROOFSTEP]
simp [← sq, gold_pos, zero_lt_one, -div_pow]
  -- Porting note: Added `- div_pow`
[GOAL]
⊢ ψ < 0
[PROOFSTEP]
linarith [one_sub_goldConj, one_lt_gold]
[GOAL]
⊢ -1 < ψ
[PROOFSTEP]
rw [neg_lt, ← inv_gold]
[GOAL]
⊢ φ⁻¹ < 1
[PROOFSTEP]
exact inv_lt_one one_lt_gold
[GOAL]
⊢ Irrational φ
[PROOFSTEP]
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
[GOAL]
⊢ Nat.Prime 5
[PROOFSTEP]
norm_num
[GOAL]
this : Irrational (sqrt ↑5)
⊢ Irrational φ
[PROOFSTEP]
have := this.rat_add 1
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 + sqrt ↑5)
⊢ Irrational φ
[PROOFSTEP]
have := this.rat_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 + sqrt ↑5)
⊢ 0.5 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 + sqrt ↑5)
this : Irrational (↑0.5 * (↑1 + sqrt ↑5))
⊢ Irrational φ
[PROOFSTEP]
convert this
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 + sqrt ↑5)
this : Irrational (↑0.5 * (↑1 + sqrt ↑5))
⊢ φ = ↑0.5 * (↑1 + sqrt ↑5)
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 + sqrt ↑5)
this : Irrational (↑0.5 * (↑1 + sqrt ↑5))
⊢ φ = 1 / 2 * (1 + sqrt 5)
[PROOFSTEP]
field_simp
[GOAL]
⊢ Irrational ψ
[PROOFSTEP]
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
[GOAL]
⊢ Nat.Prime 5
[PROOFSTEP]
norm_num
[GOAL]
this : Irrational (sqrt ↑5)
⊢ Irrational ψ
[PROOFSTEP]
have := this.rat_sub 1
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 - sqrt ↑5)
⊢ Irrational ψ
[PROOFSTEP]
have := this.rat_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
[GOAL]
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 - sqrt ↑5)
⊢ 0.5 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ Irrational ψ
[PROOFSTEP]
convert this
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ ψ = ↑0.5 * (↑1 - sqrt ↑5)
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ ψ = 1 / 2 * (1 - sqrt 5)
[PROOFSTEP]
field_simp
[GOAL]
α : Type u_1
inst✝¹ : CommSemiring α
β : Type u_2
inst✝ : CommRing β
⊢ LinearRecurrence.charPoly fibRec = X ^ 2 - (X + 1)
[PROOFSTEP]
rw [fibRec, LinearRecurrence.charPoly]
[GOAL]
α : Type u_1
inst✝¹ : CommSemiring α
β : Type u_2
inst✝ : CommRing β
⊢ (↑(monomial { order := 2, coeffs := ![1, 1] }.order) 1 -
      Finset.sum Finset.univ fun i => ↑(monomial ↑i) (LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i)) =
    X ^ 2 - (X + 1)
[PROOFSTEP]
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ', ← smul_X_eq_monomial]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => ↑(Nat.fib x)
[PROOFSTEP]
rw [fibRec]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution { order := 2, coeffs := ![1, 1] } fun x => ↑(Nat.fib x)
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ (fun x => ↑(Nat.fib x)) (n + { order := 2, coeffs := ![1, 1] }.order) =
    Finset.sum Finset.univ fun i =>
      LinearRecurrence.coeffs { order := 2, coeffs := ![1, 1] } i * (fun x => ↑(Nat.fib x)) (n + ↑i)
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 2)) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
[PROOFSTEP]
rw [Nat.fib_add_two, add_comm]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
n : ℕ
⊢ ↑(Nat.fib (n + 1) + Nat.fib n) = Finset.sum Finset.univ fun x => Matrix.vecCons 1 ![1] x * ↑(Nat.fib (n + ↑x))
[PROOFSTEP]
simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ']
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => φ ^ x
[PROOFSTEP]
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ IsRoot (X ^ 2 - (X + 1)) φ
[PROOFSTEP]
simp [sub_eq_zero, -div_pow]
  -- Porting note: Added `- div_pow`
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ LinearRecurrence.IsSolution fibRec fun x => ψ ^ x
[PROOFSTEP]
rw [fibRec.geom_sol_iff_root_charPoly, fibRec_charPoly_eq]
[GOAL]
α : Type u_1
inst✝ : CommSemiring α
⊢ IsRoot (X ^ 2 - (X + 1)) ψ
[PROOFSTEP]
simp [sub_eq_zero, -div_pow]
  -- Porting note: Added `- div_pow`
[GOAL]
⊢ (fun n => ↑(Nat.fib n)) = fun n => (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
rw [fibRec.sol_eq_of_eq_init]
[GOAL]
⊢ Set.EqOn (fun n => ↑(Nat.fib n)) (fun n => (φ ^ n - ψ ^ n) / sqrt 5) ↑(Finset.range fibRec.order)
[PROOFSTEP]
intro i hi
[GOAL]
i : ℕ
hi : i ∈ ↑(Finset.range fibRec.order)
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
[PROOFSTEP]
norm_cast at hi 
[GOAL]
i : ℕ
hi : i ∈ Finset.range fibRec.order
⊢ (fun n => ↑(Nat.fib n)) i = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) i
[PROOFSTEP]
fin_cases hi
[GOAL]
case head
⊢ (fun n => ↑(Nat.fib n)) 0 = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) 0
[PROOFSTEP]
simp
[GOAL]
case tail.head
⊢ (fun n => ↑(Nat.fib n)) 1 = (fun n => (φ ^ n - ψ ^ n) / sqrt 5) 1
[PROOFSTEP]
simp only [goldenRatio, goldenConj]
[GOAL]
case tail.head
⊢ ↑(Nat.fib 1) = (((1 + sqrt 5) / 2) ^ 1 - ((1 - sqrt 5) / 2) ^ 1) / sqrt 5
[PROOFSTEP]
ring_nf
[GOAL]
case tail.head
⊢ 1 = sqrt 5 * (sqrt 5)⁻¹
[PROOFSTEP]
rw [mul_inv_cancel]
[GOAL]
case tail.head
⊢ sqrt 5 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case hu
⊢ LinearRecurrence.IsSolution fibRec fun n => ↑(Nat.fib n)
[PROOFSTEP]
exact fib_isSol_fibRec
[GOAL]
case hv
⊢ LinearRecurrence.IsSolution fibRec fun n => (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
suffices LinearRecurrence.IsSolution fibRec ((fun n ↦ (sqrt 5)⁻¹ * φ ^ n) - (fun n ↦ (sqrt 5)⁻¹ * ψ ^ n))
  by
  convert this
  rw [Pi.sub_apply]
  ring
[GOAL]
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
⊢ LinearRecurrence.IsSolution fibRec fun n => (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
convert this
[GOAL]
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n) x✝
[PROOFSTEP]
rw [Pi.sub_apply]
[GOAL]
case h.e'_4.h
this : LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
x✝ : ℕ
⊢ (φ ^ x✝ - ψ ^ x✝) / sqrt 5 = (sqrt 5)⁻¹ * φ ^ x✝ - (sqrt 5)⁻¹ * ψ ^ x✝
[PROOFSTEP]
ring
[GOAL]
case hv
⊢ LinearRecurrence.IsSolution fibRec ((fun n => (sqrt 5)⁻¹ * φ ^ n) - fun n => (sqrt 5)⁻¹ * ψ ^ n)
[PROOFSTEP]
apply (@fibRec ℝ _).solSpace.sub_mem
[GOAL]
case hv.a
⊢ (fun n => (sqrt 5)⁻¹ * φ ^ n) ∈ LinearRecurrence.solSpace fibRec
[PROOFSTEP]
exact Submodule.smul_mem fibRec.solSpace (Real.sqrt 5)⁻¹ geom_gold_isSol_fibRec
[GOAL]
case hv.a
⊢ (fun n => (sqrt 5)⁻¹ * ψ ^ n) ∈ LinearRecurrence.solSpace fibRec
[PROOFSTEP]
exact Submodule.smul_mem fibRec.solSpace (Real.sqrt 5)⁻¹ geom_goldConj_isSol_fibRec
[GOAL]
⊢ ∀ (n : ℕ), ↑(Nat.fib n) = (φ ^ n - ψ ^ n) / sqrt 5
[PROOFSTEP]
rw [← Function.funext_iff, Real.coe_fib_eq']
