---

Step * 1 1 1 1 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. f(z) < c
26. a1 ≤ z
27. z < b1
28. b1 ≤ b1
⊢ (b1 - z) ≤ ((b1 - a1) * (r(2)/r(3)))
BY
{ ((RWO  "-6<" 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.  f(z)  <  c
26.  a1  \mleq{}  z
27.  z  <  b1
28.  b1  \mleq{}  b1
\mvdash{}  (b1  -  z)  \mleq{}  ((b1  -  a1)  *  (r(2)/r(3)))


By

---

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

---

Home Index