---

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


1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. (a, b) ⊆ [a, b] 
5. a < b
6. f[x] continuous for x ∈ [a, b]
7. ∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c)))
8. c : ℝ
9. f(a) < c
10. c < f(b)
11. a' : ℝ
12. a < a'
13. a' < b
14. f(a') < c
15. b' : ℝ
16. a' < b'
17. b' < b
18. c < f(b')
⊢ ∃x:ℝ. (((a < x) ∧ (x < b)) ∧ (f(x) = c))
BY
{ ((InstLemma `IVT-locally-non-constant` [⌜a'⌝;⌜b'⌝;⌜f⌝;⌜c⌝]⋅ THENM (Reduce -1 THEN ParallelLast))
   THEN Auto
   THEN Try ((Unhide THEN Auto))) }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. (a, b) ⊆ [a, b] 
5. a < b
6. f[x] continuous for x ∈ [a, b]
7. ∀a',b':ℝ.  (((a < a') ∧ (a' < b') ∧ (b' < b)) ⇒ (∀c:ℝ. locally-non-constant(f;a';b';c)))
8. c : ℝ
9. f(a) < c
10. c < f(b)
11. a' : ℝ
12. a < a'
13. a' < b
14. f(a') < c
15. b' : ℝ
16. a' < b'
17. b' < b
18. c < f(b')
19. x : {x:ℝ| x ∈ [a', b']} 
20. y : {x:ℝ| x ∈ [a', b']} 
21. x = y
⊢ f[x] = f[y]

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
4.  (a,  b)  \msubseteq{}  [a,  b] 
5.  a  <  b
6.  f[x]  continuous  for  x  \mmember{}  [a,  b]
7.  \mforall{}a',b':\mBbbR{}.    (((a  <  a')  \mwedge{}  (a'  <  b')  \mwedge{}  (b'  <  b))  {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  locally-non-constant(f;a';b';c)))
8.  c  :  \mBbbR{}
9.  f(a)  <  c
10.  c  <  f(b)
11.  a'  :  \mBbbR{}
12.  a  <  a'
13.  a'  <  b
14.  f(a')  <  c
15.  b'  :  \mBbbR{}
16.  a'  <  b'
17.  b'  <  b
18.  c  <  f(b')
\mvdash{}  \mexists{}x:\mBbbR{}.  (((a  <  x)  \mwedge{}  (x  <  b))  \mwedge{}  (f(x)  =  c))


By

---

Latex:
((InstLemma  `IVT-locally-non-constant`  [\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENM  (Reduce  -1  THEN  ParallelLast))
  THEN  Auto
  THEN  Try  ((Unhide  THEN  Auto)))

---

Home Index