Step
*
1
of Lemma
derivative-mul-part1
.....assertion.....
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))
⊢ ∃M:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;n)} . ((|f1(x)| ≤ r(M)) ∧ (|f2(x)| ≤ r(M)) ∧ (|g2(x)| ≤ r(M)))
BY
{ ((Assert f1(x) continuous for x ∈ i-approx(I;n) BY
(BLemma `proper-continuous-implies` THEN Auto))
THEN (RenameVar `mc1' (-1)
THEN (Assert ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f1(x)| ≤ a) BY
((InstLemma `Inorm-bound` [⌜i-approx(I;n)⌝;⌜λ2x.f1(x)⌝;⌜mc1⌝]⋅ THENA Auto)
THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜λ2x.f1(x)⌝;⌜mc1⌝]⋅ THENA Auto)
THEN With ⌜||f1(x)||_i-approx(I;n)⌝ (D 0)⋅
THEN Auto))
)
THEN (Assert f2(x) continuous for x ∈ i-approx(I;n) BY
(BLemma `proper-continuous-implies` THEN Auto))
THEN RenameVar `mc2' (-1)
THEN (Assert ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|f2(x)| ≤ a) BY
((InstLemma `Inorm-bound` [⌜i-approx(I;n)⌝;⌜λ2x.f2(x)⌝;⌜mc2⌝]⋅ THENA Auto)
THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜λ2x.f2(x)⌝;⌜mc2⌝]⋅ THENA Auto)
THEN With ⌜||f2(x)||_i-approx(I;n)⌝ (D 0)⋅
THEN Auto))
THEN ((Assert g2(x) continuous for x ∈ i-approx(I;n) BY
(BLemma `proper-continuous-implies` THEN Auto))
THEN RenameVar `mc3' (-1)
THEN (Assert ∃a:ℝ. ∀[x:{r:ℝ| r ∈ i-approx(I;n)} ]. (|g2(x)| ≤ a) BY
((InstLemma `Inorm-bound` [⌜i-approx(I;n)⌝;⌜λ2x.g2(x)⌝;⌜mc3⌝]⋅ THENA Auto)
THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜λ2x.g2(x)⌝;⌜mc3⌝]⋅ THENA Auto)
THEN With ⌜||g2(x)||_i-approx(I;n)⌝ (D 0)⋅
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)) ∧ 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)))
Latex:
Latex:
.....assertion.....
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))
\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:
((Assert f1(x) continuous for x \mmember{} i-approx(I;n) BY
(BLemma `proper-continuous-implies` THEN Auto))
THEN (RenameVar `mc1' (-1)
THEN (Assert \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|f1(x)| \mleq{} a) BY
((InstLemma `Inorm-bound` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f1(x)\mkleeneclose{};\mkleeneopen{}mc1\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `Inorm\_wf` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f1(x)\mkleeneclose{};\mkleeneopen{}mc1\mkleeneclose{}]\mcdot{} THENA Auto)
THEN With \mkleeneopen{}||f1(x)||\_i-approx(I;n)\mkleeneclose{} (D 0)\mcdot{}
THEN Auto))
)
THEN (Assert f2(x) continuous for x \mmember{} i-approx(I;n) BY
(BLemma `proper-continuous-implies` THEN Auto))
THEN RenameVar `mc2' (-1)
THEN (Assert \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|f2(x)| \mleq{} a) BY
((InstLemma `Inorm-bound` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f2(x)\mkleeneclose{};\mkleeneopen{}mc2\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `Inorm\_wf` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f2(x)\mkleeneclose{};\mkleeneopen{}mc2\mkleeneclose{}]\mcdot{} THENA Auto)
THEN With \mkleeneopen{}||f2(x)||\_i-approx(I;n)\mkleeneclose{} (D 0)\mcdot{}
THEN Auto))
THEN ((Assert g2(x) continuous for x \mmember{} i-approx(I;n) BY
(BLemma `proper-continuous-implies` THEN Auto))
THEN RenameVar `mc3' (-1)
THEN (Assert \mexists{}a:\mBbbR{}. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;n)\} ]. (|g2(x)| \mleq{} a) BY
((InstLemma `Inorm-bound` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.g2(x)\mkleeneclose{};\mkleeneopen{}mc3\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `Inorm\_wf` [\mkleeneopen{}i-approx(I;n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.g2(x)\mkleeneclose{};\mkleeneopen{}mc3\mkleeneclose{}]\mcdot{} THENA Auto)
THEN With \mkleeneopen{}||g2(x)||\_i-approx(I;n)\mkleeneclose{} (D 0)\mcdot{}
THEN Auto)))\mcdot{})
Home
Index