---

Step * 1 1 2 of Lemma rexp-rlog


1. x : ℝ
2. r0 < x
3. e^rlog(x) ≠ x
4. x_∫-e^rlog(x) (r1/t) dt = r0
⊢ False
BY
{ ((Assert λt.(r1/t) ∈ {f:(r0, ∞) ⟶ℝ| ∀a,b:{x:ℝ| r0 < x} .  ((a = b) ⇒ (f[a] = f[b]))}  BY
          (MemTypeCD THEN Reduce 0 THEN Auto THEN RepUR ``so_apply`` 0 THEN RWO "-1" 0 THEN Auto))
   THEN (InstLemma `integral-is-Riemann-on-interval` [⌜(r0, ∞)⌝;⌜λ2t.(r1/t)⌝ ]⋅ THENA Auto)
   ) }

1
1. x : ℝ
2. r0 < x
3. e^rlog(x) ≠ x
4. x_∫-e^rlog(x) (r1/t) dt = r0
5. λt.(r1/t) ∈ {f:(r0, ∞) ⟶ℝ| ∀a,b:{x:ℝ| r0 < x} .  ((a = b) ⇒ (f[a] = f[b]))} 
6. ∀[a,b:{x:ℝ| x ∈ (r0, ∞)} ].  a_∫-b (r1/x) dx = ∫ (r1/x) dx on [a, b] supposing a ≤ b
⊢ False

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  <  x
3.  e\^{}rlog(x)  \mneq{}  x
4.  x\_\mint{}\msupminus{}e\^{}rlog(x)  (r1/t)  dt  =  r0
\mvdash{}  False


By

---

Latex:
((Assert  \mlambda{}t.(r1/t)  \mmember{}  \{f:(r0,  \minfty{})  {}\mrightarrow{}\mBbbR{}|  \mforall{}a,b:\{x:\mBbbR{}|  r0  <  x\}  .    ((a  =  b)  {}\mRightarrow{}  (f[a]  =  f[b]))\}    BY
                (MemTypeCD  THEN  Reduce  0  THEN  Auto  THEN  RepUR  ``so\_apply``  0  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  (InstLemma  `integral-is-Riemann-on-interval`  [\mkleeneopen{}(r0,  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t.(r1/t)\mkleeneclose{}  ]\mcdot{}  THENA  Auto)
  )

---

Home Index