---

Step * of Lemma rational-fun-zero_wf

∀a,b:ℤ × ℕ+. ∀f:(ℤ × ℕ+) ⟶ (ℤ × ℕ+).
  ∀[g:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ]
    rational-fun-zero(f;a;b) ∈ {c:ℝ| (c ∈ [ratreal(a), ratreal(b)]) ∧ (g[c] = r0)}  
    supposing (ratreal(a) ≤ ratreal(b))
    ∧ (ratreal(f[a]) ≤ r0)
    ∧ (r0 ≤ ratreal(f[b]))
    ∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
    ∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
BY
{ (Intros THEN Unhide) }

1
1. a : ℤ × ℕ+
2. b : ℤ × ℕ+
3. f : (ℤ × ℕ+) ⟶ (ℤ × ℕ+)
4. g : {x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ
5. (ratreal(a) ≤ ratreal(b))
∧ (ratreal(f[a]) ≤ r0)
∧ (r0 ≤ ratreal(f[b]))
∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
⊢ rational-fun-zero(f;a;b) ∈ {c:ℝ| (c ∈ [ratreal(a), ratreal(b)]) ∧ (g[c] = r0)} 

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  \mforall{}f:(\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}).
    \mforall{}[g:\{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}    {}\mrightarrow{}  \mBbbR{}]
        rational-fun-zero(f;a;b)  \mmember{}  \{c:\mBbbR{}|  (c  \mmember{}  [ratreal(a),  ratreal(b)])  \mwedge{}  (g[c]  =  r0)\}   
        supposing  (ratreal(a)  \mleq{}  ratreal(b))
        \mwedge{}  (ratreal(f[a])  \mleq{}  r0)
        \mwedge{}  (r0  \mleq{}  ratreal(f[b]))
        \mwedge{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))
        \mwedge{}  (\mforall{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  ((ratreal(r)  \mmember{}  [ratreal(a),  ratreal(b)])  {}\mRightarrow{}  (g[ratreal(r)]  =  ratreal(f[r]))))


By

---

Latex:
(Intros  THEN  Unhide)

---

Home Index