pith. machine review for the scientific record. sign in
lemma proved tactic proof

phi17_lt

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 214private lemma phi17_lt : Constants.phi ^ (17 : ℕ) < (3574 : ℝ) := by

proof body

Tactic-mode proof.

 215  rw [phi_eq_goldenRatio]
 216  have h8_hi := Numerics.phi_pow8_lt
 217  have hφ_hi := Numerics.phi_lt_16185
 218  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 219  have hφ_pos : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
 220  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
 221  rw [heq]
 222  have h16_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 < (46.99 : ℝ) * (46.99 : ℝ) :=
 223    mul_lt_mul h8_hi (le_of_lt h8_hi) hpos8 (by norm_num)
 224  have h17_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio <
 225      (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) :=
 226    mul_lt_mul h16_hi (le_of_lt hφ_hi) hφ_pos (by norm_num)
 227  linarith [show (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) < (3574 : ℝ) from by norm_num]
 228

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.