Step
*
1
2
2
of Lemma
near-inverse-of-increasing-function
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. [n@0] : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
⊢ ∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])
BY
{ ((Evaluate ⌜aa = (2 * a) ∈ ℤ⌝⋅ THENA Auto)
THEN InstHyp [⌜n@0 - 1⌝;⌜aa⌝;⌜m⌝;⌜j⌝] 6⋅
THEN Auto
THEN Try ((BHyp 12 THEN Auto))) }
1
.....antecedent.....
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
21. aa : ℤ
22. aa = (2 * a) ∈ ℤ
⊢ ((M * (m - aa)) - j) ≤ (n@0 - 1)
2
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
21. aa : ℤ
22. aa = (2 * a) ∈ ℤ
23. x : ℝ
24. y : ℝ
25. (r(aa))/j ≤ x
26. x < y
27. y ≤ (r(m))/j
⊢ (r(a))/k ≤ x
3
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
21. aa : ℤ
22. aa = (2 * a) ∈ ℤ
23. x : ℝ
24. y : ℝ
25. (r(aa))/j ≤ x
26. x < y
27. y ≤ (r(m))/j
⊢ y ≤ (r(b))/k
4
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
21. aa : ℤ
22. aa = (2 * a) ∈ ℤ
23. x : ℝ
24. y : ℝ
25. (r(aa))/j ≤ x
26. x < y
27. y ≤ (r(m))/j
28. f[x] ≤ f[y]
29. (y - x) ≤ (r1/r(M))
⊢ (r(a))/k ≤ x
5
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
21. aa : ℤ
22. aa = (2 * a) ∈ ℤ
23. x : ℝ
24. y : ℝ
25. (r(aa))/j ≤ x
26. x < y
27. y ≤ (r(m))/j
28. f[x] ≤ f[y]
29. (y - x) ≤ (r1/r(M))
⊢ y ≤ (r(b))/k
6
.....antecedent.....
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. n@0 : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
21. aa : ℤ
22. aa = (2 * a) ∈ ℤ
⊢ f[(r(aa))/j] ≤ z
7
1. f : ℝ ⟶ ℝ
2. n : ℕ+
3. M : ℕ+
4. z : ℝ
5. [n@0] : ℕ
6. ∀[m:ℕn@0]
∀a,b:ℤ.
∀k:ℕ+
(∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing
((z ≤ f[(r(b))/k]) and
(f[(r(a))/k] ≤ z) and
(∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))) and
(((M * (b - a)) - k) ≤ m))
supposing a < b
7. a : ℤ
8. b : ℤ
9. a < b
10. k : ℕ+
11. ((M * (b - a)) - k) ≤ n@0
12. ∀x,y:ℝ.
(((r(a))/k ≤ x)
⇒ (x < y)
⇒ (y ≤ (r(b))/k)
⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n))))))
13. f[(r(a))/k] ≤ z
14. z ≤ f[(r(b))/k]
15. ¬((M * (b - a)) ≤ k)
16. m : ℤ
17. m = (a + b) ∈ ℤ
18. j : ℤ
19. j = (2 * k) ∈ ℤ
20. z < f[(r(m))/j]
21. aa : ℤ
22. aa = (2 * a) ∈ ℤ
23. ∃c:ℤ. (∃j@0:ℕ+ [((|f[(r(c))/j@0] - z| ≤ (r1/r(n))) ∧ ((r(aa))/j ≤ (r(c))/j@0) ∧ ((r(c))/j@0 ≤ (r(m))/j))])
⊢ ∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])
Latex:
Latex:
1. f : \mBbbR{} {}\mrightarrow{} \mBbbR{}
2. n : \mBbbN{}\msupplus{}
3. M : \mBbbN{}\msupplus{}
4. z : \mBbbR{}
5. [n@0] : \mBbbN{}
6. \mforall{}[m:\mBbbN{}n@0]
\mforall{}a,b:\mBbbZ{}.
\mforall{}k:\mBbbN{}\msupplus{}
(\mexists{}c:\mBbbZ{}
(\mexists{}j:\mBbbN{}\msupplus{} [((|f[(r(c))/j] - z| \mleq{} (r1/r(n)))
\mwedge{} ((r(a))/k \mleq{} (r(c))/j)
\mwedge{} ((r(c))/j \mleq{} (r(b))/k))])) supposing
((z \mleq{} f[(r(b))/k]) and
(f[(r(a))/k] \mleq{} z) and
(\mforall{}x,y:\mBbbR{}.
(((r(a))/k \mleq{} x)
{}\mRightarrow{} (x < y)
{}\mRightarrow{} (y \mleq{} (r(b))/k)
{}\mRightarrow{} ((f[x] \mleq{} f[y]) \mwedge{} (((y - x) \mleq{} (r1/r(M))) {}\mRightarrow{} ((f[y] - f[x]) \mleq{} (r1/r(n))))))) and
(((M * (b - a)) - k) \mleq{} m))
supposing a < b
7. a : \mBbbZ{}
8. b : \mBbbZ{}
9. a < b
10. k : \mBbbN{}\msupplus{}
11. ((M * (b - a)) - k) \mleq{} n@0
12. \mforall{}x,y:\mBbbR{}.
(((r(a))/k \mleq{} x)
{}\mRightarrow{} (x < y)
{}\mRightarrow{} (y \mleq{} (r(b))/k)
{}\mRightarrow{} ((f[x] \mleq{} f[y]) \mwedge{} (((y - x) \mleq{} (r1/r(M))) {}\mRightarrow{} ((f[y] - f[x]) \mleq{} (r1/r(n))))))
13. f[(r(a))/k] \mleq{} z
14. z \mleq{} f[(r(b))/k]
15. \mneg{}((M * (b - a)) \mleq{} k)
16. m : \mBbbZ{}
17. m = (a + b)
18. j : \mBbbZ{}
19. j = (2 * k)
20. z < f[(r(m))/j]
\mvdash{} \mexists{}c:\mBbbZ{}. (\mexists{}j:\mBbbN{}\msupplus{} [((|f[(r(c))/j] - z| \mleq{} (r1/r(n))) \mwedge{} ((r(a))/k \mleq{} (r(c))/j) \mwedge{} ((r(c))/j \mleq{} (r(b))/k))])
By
Latex:
((Evaluate \mkleeneopen{}aa = (2 * a)\mkleeneclose{}\mcdot{} THENA Auto)
THEN InstHyp [\mkleeneopen{}n@0 - 1\mkleeneclose{};\mkleeneopen{}aa\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}] 6\mcdot{}
THEN Auto
THEN Try ((BHyp 12 THEN Auto)))
Home
Index