---

Step * 1 1 of Lemma log-by-IVT


1. a : {a:ℝ| (r1/r(2)) < a} @i
⊢ ∃x:ℝ. (x = rlog(a))
BY
{ ((Assert r0 < a BY
          (D 1 THEN Unhide THEN Auto THEN RWO "-1<" 0 THEN Auto))
   THEN ((InstLemma `r-archimedean` [⌜a⌝]⋅ THENA Auto) THEN ExRepD)
   THEN (InstLemma `IVT-locally-non-constant` [⌜r(-1)⌝;⌜r(n)⌝;⌜λ2x.real_exp(x)⌝;⌜a⌝]⋅ THENA Auto)
   THEN RepUR ``r-ap so_lambda`` 0
   THEN RepUR ``r-ap so_lambda`` -1) }

1
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
6. x : {x:ℝ| x ∈ [r(-1), r(n)]} 
7. y : {x:ℝ| x ∈ [r(-1), r(n)]} 
8. x = y
⊢ real_exp(x) = real_exp(y)

2
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
⊢ real_exp(r(-1)) ≤ a

3
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
⊢ a ≤ real_exp(r(n))

4
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
⊢ locally-non-constant(λx.real_exp(x);r(-1);r(n);a)

5
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
6. ∃x:ℝ [(((r(-1) ≤ x) ∧ (x ≤ r(n))) ∧ (real_exp(x) = a))]
⊢ ∃x:ℝ. (x = rlog(a))

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  (r1/r(2))  <  a\}  @i
\mvdash{}  \mexists{}x:\mBbbR{}.  (x  =  rlog(a))


By

---

Latex:
((Assert  r0  <  a  BY
                (D  1  THEN  Unhide  THEN  Auto  THEN  RWO  "-1<"  0  THEN  Auto))
  THEN  ((InstLemma  `r-archimedean`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (InstLemma  `IVT-locally-non-constant`  [\mkleeneopen{}r(-1)\mkleeneclose{};\mkleeneopen{}r(n)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.real\_exp(x)\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``r-ap  so\_lambda``  0
  THEN  RepUR  ``r-ap  so\_lambda``  -1)

---

Home Index