---

Step * of Lemma rabs-nonzero-on-compact

∀a,b:ℝ.
  ((a ≤ b)
  ⇒ (∀f:[a, b] ⟶ℝ. ∀k:ℕ+.
        (f[x] continuous for x ∈ [a, b]
        ⇒ (∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ |f[x]|)))
        ⇒ ((∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ f[x]))) ∨ (∀x:ℝ. ((x ∈ [a, b]) ⇒ (f[x] ≤ (r(-1)/r(k)))))))))
BY
{ (Auto
   THEN (InstHyp [⌜a⌝] (-1)⋅ THENA Auto)
   THEN (RWO "rabs-ub" (-1) THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN (InstHyp [⌜x⌝] (-4)⋅ THENA Auto)
   THEN (RWO "rabs-ub" (-1) THENA Auto)
   THEN D -1
   THEN Auto) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. k : ℕ+
6. f[x] continuous for x ∈ [a, b]
7. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ |f[x]|))
8. (r1/r(k)) ≤ f[a]
9. x : ℝ
10. x ∈ [a, b]
11. (r1/r(k)) ≤ -(f[x])
⊢ (r1/r(k)) ≤ f[x]

2
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. k : ℕ+
6. f[x] continuous for x ∈ [a, b]
7. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ |f[x]|))
8. (r1/r(k)) ≤ -(f[a])
9. x : ℝ
10. x ∈ [a, b]
11. (r1/r(k)) ≤ f[x]
⊢ f[x] ≤ (r(-1)/r(k))

3
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. k : ℕ+
6. f[x] continuous for x ∈ [a, b]
7. ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((r1/r(k)) ≤ |f[x]|))
8. (r1/r(k)) ≤ -(f[a])
9. x : ℝ
10. x ∈ [a, b]
11. (r1/r(k)) ≤ -(f[x])
⊢ f[x] ≤ (r(-1)/r(k))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    ((a  \mleq{}  b)
    {}\mRightarrow{}  (\mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}k:\mBbbN{}\msupplus{}.
                (f[x]  continuous  for  x  \mmember{}  [a,  b]
                {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  ((r1/r(k))  \mleq{}  |f[x]|)))
                {}\mRightarrow{}  ((\mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  ((r1/r(k))  \mleq{}  f[x])))
                      \mvee{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  (f[x]  \mleq{}  (r(-1)/r(k)))))))))


By

---

Latex:
(Auto
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  (RWO  "rabs-ub"  (-1)  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  (RWO  "rabs-ub"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index