---

Step * 1 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))
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))))
BY
{ (OrRight THEN Auto THEN BLemma `rmax_ub` THEN Auto THEN OrRight 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(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))
16.  iproper(i-approx(I;n))
17.  mc1  :  f1(x)  continuous  for  x  \mmember{}  i-approx(I;n)
18.  a2  :  \mBbbR{}
19.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|f1(x)|  \mleq{}  a2)
20.  mc2  :  f2(x)  continuous  for  x  \mmember{}  i-approx(I;n)
21.  a1  :  \mBbbR{}
22.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|f2(x)|  \mleq{}  a1)
23.  mc3  :  g2(x)  continuous  for  x  \mmember{}  i-approx(I;n)
24.  a  :  \mBbbR{}
25.  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  i-approx(I;n)\}  ].  (|g2(x)|  \mleq{}  a)
26.  x  :  \{x:\mBbbR{}|  x  \mmember{}  i-approx(I;n)\} 
\mvdash{}  (|f1(x)|  \mleq{}  r(r-bound(a)))  \mvee{}  (|f1(x)|  \mleq{}  rmax(r(r-bound(a1));r(r-bound(a2))))


By

---

Latex:
(OrRight  THEN  Auto  THEN  BLemma  `rmax\_ub`  THEN  Auto  THEN  OrRight  THEN  Auto)

---

Home Index