---

Step * 1 1 1 2 of Lemma IVT-locally-non-constant


1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. ∀x,y:{x:ℝ| (a ≤ x) ∧ (x ≤ b)} .  ((x = y) ⇒ (f[x] = f[y]))
5. a ≤ b
6. c : ℝ
7. f(a) ≤ c
8. c ≤ f(b)
9. locally-non-constant(f;a;b;c)
10. a1 : ℝ
11. b1 : ℝ
12. a ≤ a1
13. a1 ≤ b
14. f(a1) ≤ c
15. a ≤ b1
16. b1 ≤ b
17. c ≤ f(b1)
18. a1 < b1
19. a1 < ((r(2) * a1) + b1/r(3))
20. ((r(2) * a1) + b1/r(3)) < ((r(2) * b1) + a1/r(3))
21. ((r(2) * b1) + a1/r(3)) < b1
22. z : ℝ
23. ((r(2) * a1) + b1/r(3)) ≤ z
24. z ≤ ((r(2) * b1) + a1/r(3))
25. c < f(z)
26. a1 ≤ a1
27. a1 < z
28. z ≤ b1
⊢ (z - a1) ≤ ((b1 - a1) * (r(2)/r(3)))
BY
{ ((RWO  "-5" 0 THENM nRMul ⌜r(3)⌝ 0⋅) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}x,y:\{x:\mBbbR{}|  (a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b)\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
5.  a  \mleq{}  b
6.  c  :  \mBbbR{}
7.  f(a)  \mleq{}  c
8.  c  \mleq{}  f(b)
9.  locally-non-constant(f;a;b;c)
10.  a1  :  \mBbbR{}
11.  b1  :  \mBbbR{}
12.  a  \mleq{}  a1
13.  a1  \mleq{}  b
14.  f(a1)  \mleq{}  c
15.  a  \mleq{}  b1
16.  b1  \mleq{}  b
17.  c  \mleq{}  f(b1)
18.  a1  <  b1
19.  a1  <  ((r(2)  *  a1)  +  b1/r(3))
20.  ((r(2)  *  a1)  +  b1/r(3))  <  ((r(2)  *  b1)  +  a1/r(3))
21.  ((r(2)  *  b1)  +  a1/r(3))  <  b1
22.  z  :  \mBbbR{}
23.  ((r(2)  *  a1)  +  b1/r(3))  \mleq{}  z
24.  z  \mleq{}  ((r(2)  *  b1)  +  a1/r(3))
25.  c  <  f(z)
26.  a1  \mleq{}  a1
27.  a1  <  z
28.  z  \mleq{}  b1
\mvdash{}  (z  -  a1)  \mleq{}  ((b1  -  a1)  *  (r(2)/r(3)))


By

---

Latex:
((RWO    "-5"  0  THENM  nRMul  \mkleeneopen{}r(3)\mkleeneclose{}  0\mcdot{})  THEN  Auto)

---

Home Index