Step
*
1
1
of Lemma
derivative-mul-part1
1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. f1(x) (proper)continuous for x ∈ I
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. d(f1[x])/dx = λx.g1[x] on I
11. d(f2[x])/dx = λx.g2[x] on I
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
14. i-approx(I;n) ⊆ I
15. icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))
16. mc1 : f1(x) continuous for x ∈ i-approx(I;n)
17. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f1(x)| ≤ a)
18. mc2 : f2(x) continuous for x ∈ i-approx(I;n)
19. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f2(x)| ≤ a)
20. mc3 : g2(x) continuous for x ∈ i-approx(I;n)
21. ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g2(x)| ≤ a)
⊢ ∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
BY
{ (ExRepD
THEN With ⌜imax(r-bound(a);imax(r-bound(a1);r-bound(a2)))⌝ (D 0)⋅
THEN Auto
THEN (RWW "rmax-int<" 0 THENA Auto)
THEN Try ((BLemma `rmax_ub` THEN Auto))) }
1
1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. f1(x) (proper)continuous for x ∈ I
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. d(f1[x])/dx = λx.g1[x] on I
11. d(f2[x])/dx = λx.g2[x] on I
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
14. i-approx(I;n) ⊆ I
15. icompact(i-approx(I;n))
16. iproper(i-approx(I;n))
17. mc1 : f1(x) continuous for x ∈ i-approx(I;n)
18. a2 : ℝ
19. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f1(x)| ≤ a2)
20. mc2 : f2(x) continuous for x ∈ i-approx(I;n)
21. a1 : ℝ
22. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f2(x)| ≤ a1)
23. mc3 : g2(x) continuous for x ∈ i-approx(I;n)
24. a : ℝ
25. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g2(x)| ≤ a)
26. x : {x:ℝ| x ∈ i-approx(I;n)}
⊢ (|f1(x)| ≤ r(r-bound(a))) ∨ (|f1(x)| ≤ rmax(r(r-bound(a1));r(r-bound(a2))))
2
1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. f1(x) (proper)continuous for x ∈ I
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. d(f1[x])/dx = λx.g1[x] on I
11. d(f2[x])/dx = λx.g2[x] on I
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
14. i-approx(I;n) ⊆ I
15. icompact(i-approx(I;n))
16. iproper(i-approx(I;n))
17. mc1 : f1(x) continuous for x ∈ i-approx(I;n)
18. a2 : ℝ
19. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f1(x)| ≤ a2)
20. mc2 : f2(x) continuous for x ∈ i-approx(I;n)
21. a1 : ℝ
22. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f2(x)| ≤ a1)
23. mc3 : g2(x) continuous for x ∈ i-approx(I;n)
24. a : ℝ
25. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g2(x)| ≤ a)
26. x : {x:ℝ| x ∈ i-approx(I;n)}
27. |f1(x)| ≤ r(imax(r-bound(a);imax(r-bound(a1);r-bound(a2))))
⊢ (|f2(x)| ≤ r(r-bound(a))) ∨ (|f2(x)| ≤ rmax(r(r-bound(a1));r(r-bound(a2))))
3
1. I : Interval
2. True
3. f1 : I ⟶ℝ
4. f2 : I ⟶ℝ
5. g1 : I ⟶ℝ
6. g2 : I ⟶ℝ
7. f1(x) (proper)continuous for x ∈ I
8. f2(x) (proper)continuous for x ∈ I
9. g2(x) (proper)continuous for x ∈ I
10. d(f1[x])/dx = λx.g1[x] on I
11. d(f2[x])/dx = λx.g2[x] on I
12. k : ℕ+
13. n : {n:ℕ+| icompact(i-approx(I;n)) ∧ iproper(i-approx(I;n))}
14. i-approx(I;n) ⊆ I
15. icompact(i-approx(I;n))
16. iproper(i-approx(I;n))
17. mc1 : f1(x) continuous for x ∈ i-approx(I;n)
18. a2 : ℝ
19. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f1(x)| ≤ a2)
20. mc2 : f2(x) continuous for x ∈ i-approx(I;n)
21. a1 : ℝ
22. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f2(x)| ≤ a1)
23. mc3 : g2(x) continuous for x ∈ i-approx(I;n)
24. a : ℝ
25. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g2(x)| ≤ a)
26. x : {x:ℝ| x ∈ i-approx(I;n)}
27. |f1(x)| ≤ r(imax(r-bound(a);imax(r-bound(a1);r-bound(a2))))
28. |f2(x)| ≤ r(imax(r-bound(a);imax(r-bound(a1);r-bound(a2))))
⊢ (|g2(x)| ≤ r(r-bound(a))) ∨ (|g2(x)| ≤ rmax(r(r-bound(a1));r(r-bound(a2))))
Latex:
Latex:
1. I : Interval
2. True
3. f1 : I {}\mrightarrow{}\mBbbR{}
4. f2 : I {}\mrightarrow{}\mBbbR{}
5. g1 : I {}\mrightarrow{}\mBbbR{}
6. g2 : I {}\mrightarrow{}\mBbbR{}
7. f1(x) (proper)continuous for x \mmember{} I
8. f2(x) (proper)continuous for x \mmember{} I
9. g2(x) (proper)continuous for x \mmember{} I
10. d(f1[x])/dx = \mlambda{}x.g1[x] on I
11. d(f2[x])/dx = \mlambda{}x.g2[x] on I
12. k : \mBbbN{}\msupplus{}
13. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))\}
14. i-approx(I;n) \msubseteq{} I
15. icompact(i-approx(I;n)) \mwedge{} iproper(i-approx(I;n))
16. mc1 : f1(x) continuous for x \mmember{} i-approx(I;n)
17. \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|f1(x)| \mleq{} a)
18. mc2 : f2(x) continuous for x \mmember{} i-approx(I;n)
19. \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|f2(x)| \mleq{} a)
20. mc3 : g2(x) continuous for x \mmember{} i-approx(I;n)
21. \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|g2(x)| \mleq{} a)
\mvdash{} \mexists{}M:\mBbbN{}\msupplus{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;n)\} . ((|f1(x)| \mleq{} r(M)) \mwedge{} (|f2(x)| \mleq{} r(M)) \mwedge{} (|g2(x)| \mleq{} r(M)))
By
Latex:
(ExRepD
THEN With \mkleeneopen{}imax(r-bound(a);imax(r-bound(a1);r-bound(a2)))\mkleeneclose{} (D 0)\mcdot{}
THEN Auto
THEN (RWW "rmax-int<" 0 THENA Auto)
THEN Try ((BLemma `rmax\_ub` THEN Auto)))
Home
Index