---

Step * 1 1 4 4 of Lemma log-by-IVT


1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
6. e^x strictly-increasing for x ∈ [r(-1), r(n)]
⊢ locally-non-constant(λx.real_exp(x);r(-1);r(n);a)
BY
{ (D 0 THEN Auto THEN (D 6 With ⌜u⌝  THENA Auto) THEN D -1 With ⌜v⌝  THEN Auto) }

1
1. a : {a:ℝ| (r1/r(2)) < a} @i
2. r0 < a
3. n : ℕ
4. r(-n) ≤ a
5. a ≤ r(n)
6. u : ℝ
7. v : ℝ
8. r(-1) ≤ u
9. u < v
10. v ≤ r(n)
11. e^u < e^v
⊢ ∃z:ℝ. ((u ≤ z) ∧ (z ≤ v) ∧ λx.real_exp(x)(z) ≠ a)

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  (r1/r(2))  <  a\}  @i
2.  r0  <  a
3.  n  :  \mBbbN{}
4.  r(-n)  \mleq{}  a
5.  a  \mleq{}  r(n)
6.  e\^{}x  strictly-increasing  for  x  \mmember{}  [r(-1),  r(n)]
\mvdash{}  locally-non-constant(\mlambda{}x.real\_exp(x);r(-1);r(n);a)


By

---

Latex:
(D  0  THEN  Auto  THEN  (D  6  With  \mkleeneopen{}u\mkleeneclose{}    THENA  Auto)  THEN  D  -1  With  \mkleeneopen{}v\mkleeneclose{}    THEN  Auto)

---

Home Index