---

Step * 1 1 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)])} 
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))
15. ratreal(m) ∈ {x:ℝ| (ratreal(a) ≤ x) ∧ (x ≤ ratreal(b))} 
16. g[ratreal(m)] = ratreal(r)
⊢ ∃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
{ ((MemTypeHD (-2) THENA Auto)
   THEN (Assert rinv(r(2)) = (r1/r(2)) BY
               (nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
   THEN (InstLemma `rat-zero-cases` [⌜r⌝]⋅ THENA Auto)
   THEN (D -1 THENL [D 0 With ⌜<x, m>⌝ ; D 0 With ⌜<m, y>⌝ ])
   THEN Reduce 0
   THEN Auto
   THEN RWO "-4" 0
   THEN Auto) }

---

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)])\} 
8.  m  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
9.  m  =  rat-nat-div(ratadd(x;y);2)
10.  r  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
11.  r  =  f[m]
12.  ((ratreal(m)  -  ratreal(x))  =  ((r1/r(2))  *  (ratreal(y)  -  ratreal(x))))
\mwedge{}  ((ratreal(y)  -  ratreal(m))  =  ((r1/r(2))  *  (ratreal(y)  -  ratreal(x))))
13.  (ratreal(x)  \mleq{}  ratreal(m))  \mwedge{}  (ratreal(m)  \mleq{}  ratreal(y))
14.  ratreal(rat-nat-div(ratadd(x;y);2))  =  ravg(ratreal(x);ratreal(y))
15.  ratreal(m)  \mmember{}  \{x:\mBbbR{}|  (ratreal(a)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  ratreal(b))\} 
16.  g[ratreal(m)]  =  ratreal(r)
\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:
((MemTypeHD  (-2)  THENA  Auto)
  THEN  (Assert  rinv(r(2))  =  (r1/r(2))  BY
                          (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `rat-zero-cases`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  THENL  [D  0  With  \mkleeneopen{}<x,  m>\mkleeneclose{}  ;  D  0  With  \mkleeneopen{}<m,  y>\mkleeneclose{}  ])
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "-4"  0
  THEN  Auto)

---

Home Index