---

Step * 1 of Lemma IVT-test


rational-fun-zero(λx.ratsub(ratexp(x;3);<2, 1>);<1, 1>;<2, 1>) ∈ ∃x:ℝ [(x^3 = r(2))]
BY
{ (InstLemma `rational-fun-zero_wf` 
      [⌜<1, 1>⌝;⌜<2, 1>⌝;⌜λ2x.ratsub(ratexp(x;3);<2, 1>)⌝;⌜λ2x.x^3 - r(2)⌝]⋅
   THENA (Auto
          THEN RW (SubC ratreal_pushdownC) 0
          THEN Auto
          THEN nRNorm 0
          THEN Auto
          THEN (RWO "rnexp-int" 0 THENA Auto)
          THEN RWO "radd-int" 0
          THEN Auto)
   ) }

1
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))]

---

Latex:

---

Latex:

rational-fun-zero(\mlambda{}x.ratsub(ratexp(x;3);ɚ,  1>);ə,  1>ɚ,  1>)  \mmember{}  \mexists{}x:\mBbbR{}  [(x\^{}3  =  r(2))]


By

---

Latex:
(InstLemma  `rational-fun-zero\_wf` 
        [\mkleeneopen{}ə,  1>\mkleeneclose{};\mkleeneopen{}ɚ,  1>\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.ratsub(ratexp(x;3);ɚ,  1>)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.x\^{}3  -  r(2)\mkleeneclose{}]\mcdot{}
  THENA  (Auto
                THEN  RW  (SubC  ratreal\_pushdownC)  0
                THEN  Auto
                THEN  nRNorm  0
                THEN  Auto
                THEN  (RWO  "rnexp-int"  0  THENA  Auto)
                THEN  RWO  "radd-int"  0
                THEN  Auto)
  )

---

Home Index