---

Step * 1 1 of Lemma IVT-strictly-increasing-open


1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
5. (a, b) ⊆ [a, b] 
6. a' : ℝ
7. b' : ℝ
8. a < a'
9. a' < b'
10. b' < b
11. c : ℝ
12. u : ℝ
13. v : ℝ
14. a' ≤ u
15. u < v
16. v ≤ b'
17. f[u] < f[v]
⊢ ∃z:ℝ. ((u ≤ z) ∧ (z ≤ v) ∧ f(z) ≠ c)
BY
{ ((InstLemma `rless-cases` [⌜f[u]⌝;⌜f[v]⌝;⌜c⌝]⋅ THENA Auto) THEN D -1) }

1
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
5. (a, b) ⊆ [a, b] 
6. a' : ℝ
7. b' : ℝ
8. a < a'
9. a' < b'
10. b' < b
11. c : ℝ
12. u : ℝ
13. v : ℝ
14. a' ≤ u
15. u < v
16. v ≤ b'
17. f[u] < f[v]
18. f[u] < c
⊢ ∃z:ℝ. ((u ≤ z) ∧ (z ≤ v) ∧ f(z) ≠ c)

2
1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : [a, b] ⟶ℝ
4. ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (f[x] = f[y]))
5. (a, b) ⊆ [a, b] 
6. a' : ℝ
7. b' : ℝ
8. a < a'
9. a' < b'
10. b' < b
11. c : ℝ
12. u : ℝ
13. v : ℝ
14. a' ≤ u
15. u < v
16. v ≤ b'
17. f[u] < f[v]
18. c < f[v]
⊢ ∃z:ℝ. ((u ≤ z) ∧ (z ≤ v) ∧ f(z) ≠ c)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
5.  (a,  b)  \msubseteq{}  [a,  b] 
6.  a'  :  \mBbbR{}
7.  b'  :  \mBbbR{}
8.  a  <  a'
9.  a'  <  b'
10.  b'  <  b
11.  c  :  \mBbbR{}
12.  u  :  \mBbbR{}
13.  v  :  \mBbbR{}
14.  a'  \mleq{}  u
15.  u  <  v
16.  v  \mleq{}  b'
17.  f[u]  <  f[v]
\mvdash{}  \mexists{}z:\mBbbR{}.  ((u  \mleq{}  z)  \mwedge{}  (z  \mleq{}  v)  \mwedge{}  f(z)  \mneq{}  c)


By

---

Latex:
((InstLemma  `rless-cases`  [\mkleeneopen{}f[u]\mkleeneclose{};\mkleeneopen{}f[v]\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index