---

Step * 1 1 of Lemma IVT-test


1. rational-fun-zero(λ2x.ratsub(ratexp(x;3);<2, 1>);<1, 1>;<2, 1>) ∈ {c:ℝ| (c ∈ [ratreal(<1, 1>), ratreal(<2, 1>)]) ∧ ((\000Cc^3 - r(2)) = r0)} 
⊢ rational-fun-zero(λx.ratsub(ratexp(x;3);<2, 1>);<1, 1>;<2, 1>) ∈ ∃x:ℝ [(x^3 = r(2))]
BY
{ (Unfold `so_lambda` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  rational-fun-zero(\mlambda{}\msubtwo{}x.ratsub(ratexp(x;3);ɚ,  1>);ə,  1>ɚ,  1>)  \mmember{}  \{c:\mBbbR{}|  (c  \mmember{}  [ratreal(ə,  1>),  ra\000Ctreal(ɚ,  1>)])  \mwedge{}  ((c\^{}3  -  r(2))  =  r0)\} 
\mvdash{}  rational-fun-zero(\mlambda{}x.ratsub(ratexp(x;3);ɚ,  1>);ə,  1>ɚ,  1>)  \mmember{}  \mexists{}x:\mBbbR{}  [(x\^{}3  =  r(2))]


By

---

Latex:
(Unfold  `so\_lambda`  -1  THEN  Auto)

---

Home Index