---

Step * 1 of Lemma reals-uncountable-simple


1. f : ℕ ⟶ ℝ@i
2. Surj(ℕ;ℝ;f)@i
3. u : ℝ
4. r0 ≤ u
5. u ≤ r1
6. ∀n:ℕ. u ≠ f n
⊢ False
BY
{ ((With ⌜u⌝ (D 2)⋅ THEN Auto) THEN ExRepD THEN InstHyp [⌜a⌝] (-3)⋅ THEN Auto THEN RWO "-2" (-1) THEN Auto)⋅ }

1
1. f : ℕ ⟶ ℝ@i
2. u : ℝ
3. r0 ≤ u
4. u ≤ r1
5. ∀n:ℕ. u ≠ f n
6. a : ℕ@i
7. (f a) = u ∈ ℝ@i
8. u ≠ u
⊢ False

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}@i
2.  Surj(\mBbbN{};\mBbbR{};f)@i
3.  u  :  \mBbbR{}
4.  r0  \mleq{}  u
5.  u  \mleq{}  r1
6.  \mforall{}n:\mBbbN{}.  u  \mneq{}  f  n
\mvdash{}  False


By

---

Latex:
((With  \mkleeneopen{}u\mkleeneclose{}  (D  2)\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-3)\mcdot{}
  THEN  Auto
  THEN  RWO  "-2"  (-1)
  THEN  Auto)\mcdot{}

---

Home Index