Step
*
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))
⊢ ∃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
{ ((Assert ratreal(m) ∈ {x:ℝ| (ratreal(a) ≤ x) ∧ (x ≤ ratreal(b))} BY
(DSetVars THEN All Reduce THEN MemTypeCD THEN Auto))
THEN (Assert g[ratreal(m)] = ratreal(f[m]) BY
((Unhide THENA Auto)
THEN ExRepD
THEN (MemTypeHD (-1) THENA Auto)
THEN (Unhide THENA Auto)
THEN (Assert ratreal(rat-nat-div(ratadd(x;y);2)) ∈ [ratreal(a), ratreal(b)] BY
(RWO "13<" 0 THEN Auto))
THEN RWO "13" 0
THEN Auto))
THEN (RWO "-6<" (-1) 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))
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)))))
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))
\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:
((Assert ratreal(m) \mmember{} \{x:\mBbbR{}| (ratreal(a) \mleq{} x) \mwedge{} (x \mleq{} ratreal(b))\} BY
(DSetVars THEN All Reduce THEN MemTypeCD THEN Auto))
THEN (Assert g[ratreal(m)] = ratreal(f[m]) BY
((Unhide THENA Auto)
THEN ExRepD
THEN (MemTypeHD (-1) THENA Auto)
THEN (Unhide THENA Auto)
THEN (Assert ratreal(rat-nat-div(ratadd(x;y);2)) \mmember{} [ratreal(a), ratreal(b)] BY
(RWO "13<" 0 THEN Auto))
THEN RWO "13" 0
THEN Auto))
THEN (RWO "-6<" (-1) THENA Auto))
Home
Index