theorem proved term proof

`phi_lt_onePointEight`

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

formal statement (Lean)

 102theorem phi_lt_onePointEight : φ < (1.8 : ℝ) :=

Term-mode proof.

 103  lt_trans phi_lt_onePointSixOneNine (by norm_num)
 104
 105/-- φ > 1.6. -/

Lean names referenced from this declaration's body.

lt_trans in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
phi_lt_onePointSixOneNine in IndisputableMonolith.Foundation.PhiForcing decl_use