---

Step * 1 1 1 of Lemma rational-IVT-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)))))
BY
{ ((Evaluate ⌜m = rat-nat-div(ratadd(x;y);2) ∈ (ℤ × ℕ+)⌝⋅ THENA Auto)
   THEN (Evaluate ⌜r = f[m] ∈ (ℤ × ℕ+)⌝⋅ THENA Auto)
   THEN (InstLemma `ravg-dist-when-rleq` [⌜ratreal(x)⌝;⌜ratreal(y)⌝]⋅ THENA Auto)
   THEN (InstLemma `ravg-weak-between` [⌜ratreal(x)⌝;⌜ratreal(y)⌝]⋅ THENA Auto)
   THEN (Assert ratreal(rat-nat-div(ratadd(x;y);2)) = ravg(ratreal(x);ratreal(y)) BY
               ((RW (AddrC [1] ratreal_pushdownC) 0 THENA Auto)
                THEN (RWO "int-rdiv-req" 0 THENA Auto)
                THEN Fold `ravg` 0
                THEN Auto))
   THEN (RWW "-1< 9<" (-2) THENA Auto)
   THEN (RWW "-1< 9<" (-3) THENA Auto)) }

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)])} 
8. m : ℤ × ℕ+
9. m = rat-nat-div(ratadd(x;y);2) ∈ (ℤ × ℕ+)
10. r : ℤ × ℕ+
11. r = f[m] ∈ (ℤ × ℕ+)
12. ((ratreal(m) - ratreal(x)) = ((r1/r(2)) * (ratreal(y) - ratreal(x))))
∧ ((ratreal(y) - ratreal(m)) = ((r1/r(2)) * (ratreal(y) - ratreal(x))))
13. (ratreal(x) ≤ ratreal(m)) ∧ (ratreal(m) ≤ ratreal(y))
14. ratreal(rat-nat-div(ratadd(x;y);2)) = ravg(ratreal(x);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:

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]))))
6.  x  :  \{x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  (ratreal(x)  \mmember{}  [ratreal(a),  ratreal(b)])  \mwedge{}  (g[ratreal(x)]  \mleq{}  r0)\} 
7.  y  :  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}| 
                (ratreal(y)  \mmember{}  [ratreal(a),  ratreal(b)])  \mwedge{}  (ratreal(x)  \mleq{}  ratreal(y))  \mwedge{}  (r0  \mleq{}  g[ratreal(y)])\} 
\mvdash{}  \mexists{}q:x:\{x:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  ((ratreal(a)  \mleq{}  ratreal(x))  \mwedge{}  (ratreal(x)  \mleq{}  ratreal(b)))  \mwedge{}  (g[ratreal(x)]  \mleq{}  r0)\} 
          \mtimes{}  \{y:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}| 
                ((ratreal(a)  \mleq{}  ratreal(y))  \mwedge{}  (ratreal(y)  \mleq{}  ratreal(b)))
                \mwedge{}  (ratreal(x)  \mleq{}  ratreal(y))
                \mwedge{}  (r0  \mleq{}  g[ratreal(y)])\} 
      ((ratreal(x)  \mleq{}  ratreal(fst(q)))
      \mwedge{}  (ratreal(snd(q))  \mleq{}  ratreal(y))
      \mwedge{}  ((ratreal(snd(q))  -  ratreal(fst(q)))  =  (rinv(r(2))  *  (ratreal(y)  -  ratreal(x)))))


By

---

Latex:
((Evaluate  \mkleeneopen{}m  =  rat-nat-div(ratadd(x;y);2)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}r  =  f[m]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `ravg-dist-when-rleq`  [\mkleeneopen{}ratreal(x)\mkleeneclose{};\mkleeneopen{}ratreal(y)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `ravg-weak-between`  [\mkleeneopen{}ratreal(x)\mkleeneclose{};\mkleeneopen{}ratreal(y)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  ratreal(rat-nat-div(ratadd(x;y);2))  =  ravg(ratreal(x);ratreal(y))  BY
                          ((RW  (AddrC  [1]  ratreal\_pushdownC)  0  THENA  Auto)
                            THEN  (RWO  "int-rdiv-req"  0  THENA  Auto)
                            THEN  Fold  `ravg`  0
                            THEN  Auto))
  THEN  (RWW  "-1<  9<"  (-2)  THENA  Auto)
  THEN  (RWW  "-1<  9<"  (-3)  THENA  Auto))

---

Home Index