---

Step * 1 1 of Lemma rational-IVT-1

.....assertion..... 
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]))))
⊢ ∀p:x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}  × {y:ℤ × ℕ+| 
                                                                                   (ratreal(y)
                                                                                   ∈ [ratreal(a), ratreal(b)])
                                                                                   ∧ (ratreal(x) ≤ ratreal(y))
                                                                                   ∧ (r0 ≤ g[ratreal(y)])} 
    ∃q:x:{x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)}  × {y:ℤ × ℕ+| 
                                                                                     (ratreal(y)
                                                                                     ∈ [ratreal(a), ratreal(b)])
                                                                                     ∧ (ratreal(x) ≤ ratreal(y))
                                                                                     ∧ (r0 ≤ g[ratreal(y)])} 
     ((ratreal(fst(p)) ≤ ratreal(fst(q)))
     ∧ (ratreal(snd(q)) ≤ ratreal(snd(p)))
     ∧ ((ratreal(snd(q)) - ratreal(fst(q))) = (rinv(r(2)) * (ratreal(snd(p)) - ratreal(fst(p))))))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN RenameVar `y' (-1) THEN Reduce 0) }

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]))))
6. x : {x:ℤ × ℕ+| (ratreal(x) ∈ [ratreal(a), ratreal(b)]) ∧ (g[ratreal(x)] ≤ r0)} 
7. y : {y:ℤ × ℕ+| (ratreal(y) ∈ [ratreal(a), ratreal(b)]) ∧ (ratreal(x) ≤ ratreal(y)) ∧ (r0 ≤ g[ratreal(y)])} 
⊢ ∃q:x:{x:ℤ × ℕ+| ((ratreal(a) ≤ ratreal(x)) ∧ (ratreal(x) ≤ ratreal(b))) ∧ (g[ratreal(x)] ≤ r0)} 
     × {y:ℤ × ℕ+| 
        ((ratreal(a) ≤ ratreal(y)) ∧ (ratreal(y) ≤ ratreal(b))) ∧ (ratreal(x) ≤ ratreal(y)) ∧ (r0 ≤ g[ratreal(y)])} 
   ((ratreal(x) ≤ ratreal(fst(q)))
   ∧ (ratreal(snd(q)) ≤ ratreal(y))
   ∧ ((ratreal(snd(q)) - ratreal(fst(q))) = (rinv(r(2)) * (ratreal(y) - ratreal(x)))))

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  b  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
3.  f  :  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})
4.  [g]  :  \{x:\mBbbR{}|  x  \mmember{}  [ratreal(a),  ratreal(b)]\}    {}\mrightarrow{}  \mBbbR{}
5.  [\%]  :  (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]))))
\mvdash{}  \mforall{}p:x:\{x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  (ratreal(x)  \mmember{}  [ratreal(a),  ratreal(b)])  \mwedge{}  (g[ratreal(x)]  \mleq{}  r0)\} 
          \mtimes{}  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}| 
                (ratreal(y)  \mmember{}  [ratreal(a),  ratreal(b)])  \mwedge{}  (ratreal(x)  \mleq{}  ratreal(y))  \mwedge{}  (r0  \mleq{}  g[ratreal(y)])\} 
        \mexists{}q:x:\{x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  (ratreal(x)  \mmember{}  [ratreal(a),  ratreal(b)])  \mwedge{}  (g[ratreal(x)]  \mleq{}  r0)\} 
              \mtimes{}  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}| 
                    (ratreal(y)  \mmember{}  [ratreal(a),  ratreal(b)])
                    \mwedge{}  (ratreal(x)  \mleq{}  ratreal(y))
                    \mwedge{}  (r0  \mleq{}  g[ratreal(y)])\} 
          ((ratreal(fst(p))  \mleq{}  ratreal(fst(q)))
          \mwedge{}  (ratreal(snd(q))  \mleq{}  ratreal(snd(p)))
          \mwedge{}  ((ratreal(snd(q))  -  ratreal(fst(q)))  =  (rinv(r(2))  *  (ratreal(snd(p))  -  ratreal(fst(p))))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  RenameVar  `y'  (-1)  THEN  Reduce  0)

---

Home Index