---

Step * 2 1 1 1 of Lemma baire2cantor2baire


1. a : ℕ ⟶ ℕ
2. init0(a)
3. ∀n:ℕ. (((a (n + 1)) = (a n) ∈ ℕ) ∨ ((a (n + 1)) = ((a n) + 1) ∈ ℕ))
4. x : ℤ
5. a x ≠ a (x - 1)
6. x ≠ 0
7. 0 < x
8. cantor2baire-aux(baire2cantor(a);x - 1) = (a (x - 1)) ∈ ℕ
9. ((a x) = (a (x - 1)) ∈ ℕ) ∨ ((a x) = ((a (x - 1)) + 1) ∈ ℕ)
⊢ ((a (x - 1)) + 1) = (a x) ∈ ℕ
BY
{ (D (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  init0(a)
3.  \mforall{}n:\mBbbN{}.  (((a  (n  +  1))  =  (a  n))  \mvee{}  ((a  (n  +  1))  =  ((a  n)  +  1)))
4.  x  :  \mBbbZ{}
5.  a  x  \mneq{}  a  (x  -  1)
6.  x  \mneq{}  0
7.  0  <  x
8.  cantor2baire-aux(baire2cantor(a);x  -  1)  =  (a  (x  -  1))
9.  ((a  x)  =  (a  (x  -  1)))  \mvee{}  ((a  x)  =  ((a  (x  -  1))  +  1))
\mvdash{}  ((a  (x  -  1))  +  1)  =  (a  x)


By

---

Latex:
(D  (-1)  THEN  Auto)

---

Home Index