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

pi_pow5_gt_d6

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)

 216theorem pi_pow5_gt_d6 : (306.0193 : ℝ) < pi ^ 5 := by

proof body

Tactic-mode proof.

 217  have h := Real.pi_gt_d6  -- 3.141592 < π
 218  have hpos : 0 < pi := Real.pi_pos
 219  have h1 : (3.141592 : ℝ) ^ 5 < pi ^ 5 := by
 220    have hle : (3.141592 : ℝ) ≤ pi := le_of_lt h
 221    have hlo : (0 : ℝ) < 3.141592 := by norm_num
 222    nlinarith [sq_nonneg pi, sq_nonneg (pi - 3.141592), mul_self_nonneg pi,
 223               mul_self_nonneg (pi ^ 2), mul_self_nonneg (pi ^ 2 - 3.141592 ^ 2)]
 224  calc (306.0193 : ℝ) < (3.141592 : ℝ) ^ 5 := by norm_num
 225    _ < pi ^ 5 := h1
 226
 227/-- π⁵ < 306.0199 (using π < 3.141593) -/

used by (1)

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