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_add 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