Proof of Nuprl Lemma : derivative-mul-part1

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)⌝;⌜λ₂x.f1(x)⌝;⌜mc1⌝]⋅ THENA Auto)

                      THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜λ₂x.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)⌝;⌜λ₂x.f2(x)⌝;⌜mc2⌝]⋅ THENA Auto)

                THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜λ₂x.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)⌝;⌜λ₂x.g2(x)⌝;⌜mc3⌝]⋅ THENA Auto)

                      THEN (InstLemma `Inorm_wf` [⌜i-approx(I;n)⌝;⌜λ₂x.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