lemma proved tactic proof

`phi_lt_1_7`

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

formal statement (Lean)

  90lemma phi_lt_1_7 : phi < 1.7 := by

proof body

Tactic-mode proof.

  91  unfold phi
  92  norm_num
  93  have : Real.sqrt 5 < 2.4 := by
  94    rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.4)]
  95    apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  96  linarith
  97
  98/-- φ¹⁰ > 100. -/

used by (3)

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

ml_is_phi_power in IndisputableMonolith.Derivations.MassToLight decl_use
phi_bounds_stub in IndisputableMonolith.Support.PhiApprox decl_use
phi_lt_1_7 in IndisputableMonolith.Support.PhiApprox decl_use

depends on (1)

Lean names referenced from this declaration's body.

phi_lt_1_7 in IndisputableMonolith.Support.PhiApprox decl_use