---

Step * of Lemma IVT-test

∃x:ℝ [(x^3 = r(2))]
BY
{ UseWitness ⌜rational-fun-zero(λx.ratsub(ratexp(x;3);<2, 1>);<1, 1>;<2, 1>)⌝⋅ }

1
rational-fun-zero(λx.ratsub(ratexp(x;3);<2, 1>);<1, 1>;<2, 1>) ∈ ∃x:ℝ [(x^3 = r(2))]

---

Latex:

---

Latex:
\mexists{}x:\mBbbR{}  [(x\^{}3  =  r(2))]


By

---

Latex:
UseWitness  \mkleeneopen{}rational-fun-zero(\mlambda{}x.ratsub(ratexp(x;3);ɚ,  1>);ə,  1>ɚ,  1>)\mkleeneclose{}\mcdot{}

---

Home Index