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

phi_lt_exp_0483

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)

 272private lemma phi_lt_exp_0483 : 16180340 / 10000000 + exp_error_10_at_0483 < exp_taylor_10_at_0483 := by

proof body

Term-mode proof.

 273  native_decide
 274
 275/-- Rigorous upper bound: log(φ) < 0.483
 276
 277    Proof using exp monotonicity: log(φ) < 0.483 ↔ φ < exp(0.483).
 278    We have φ < 1.6180340 and exp(0.483) ≈ 1.6210... > 1.6180340. -/

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.