---

Step * 1 of Lemma rlog-integral-non-zero


1. a : ℝ
2. b : ℝ
3. r0 < a
4. a < b
⊢ ¬(∫ (r1/t) dt on [a, b] = r0)
BY
{ (InstLemma `Riemann-integral-lower-bound` [⌜a⌝;⌜b⌝; ⌜λ2t.(r1/t)⌝;⌜(r1/b)⌝]⋅
   THENA ((Auto THEN Try ((RWO "-1" 0 THEN Auto)))
          THEN Try (Complete (((OrRight THEN Auto)
                               THEN DSetVars
                               THEN (Unhide THEN Auto)
                               THEN All Reduce
                               THEN ExRepD
                               THEN Auto)))
          )
   ) }

1
1. a : ℝ
2. b : ℝ
3. r0 < a
4. a < b
5. x : ℝ
6. x ∈ [a, b]
⊢ (r1/b) ≤ (r1/x)

2
1. a : ℝ
2. b : ℝ
3. r0 < a
4. a < b
5. ((r1/b) * (b - a)) ≤ ∫ (r1/x) dx on [a, b]
⊢ ¬(∫ (r1/t) dt on [a, b] = r0)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  r0  <  a
4.  a  <  b
\mvdash{}  \mneg{}(\mint{}  (r1/t)  dt  on  [a,  b]  =  r0)


By

---

Latex:
(InstLemma  `Riemann-integral-lower-bound`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}t.(r1/t)\mkleeneclose{};\mkleeneopen{}(r1/b)\mkleeneclose{}]\mcdot{}
  THENA  ((Auto  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))
                THEN  Try  (Complete  (((OrRight  THEN  Auto)
                                                          THEN  DSetVars
                                                          THEN  (Unhide  THEN  Auto)
                                                          THEN  All  Reduce
                                                          THEN  ExRepD
                                                          THEN  Auto)))
                )
  )

---

Home Index