this : Irrational (sqrt ↑5)
⊢ Irrational ψ
⊢ Irrational ψ
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 - sqrt ↑5)
⊢ Irrational ψ
this : Irrational (sqrt ↑5)
⊢ Irrational ψ
have := this.rat_sub 1
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ Irrational ψ
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 - sqrt ↑5)
⊢ Irrational ψ
have := this.rat_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
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)
this✝¹ : Irrational (sqrt ↑5)
this✝ : Irrational (↑1 - sqrt ↑5)
this : Irrational (↑0.5 * (↑1 - sqrt ↑5))
⊢ Irrational ψ
convert this
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)
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)
norm_num
no goals
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)
field_simp
no goals
⊢ Nat.Prime 5
norm_num
no goals
this✝ : Irrational (sqrt ↑5)
this : Irrational (↑1 - sqrt ↑5)
⊢ 0.5 ≠ 0
norm_num