---

Step * of Lemma equipollent-nat-powered

∀n:ℕ. ℕ ~ (ℕ^n + 1)
BY
{ ((Auto THEN NatInd 1) THEN Auto) }

1
.....basecase..... 
ℕ ~ (ℕ^0 + 1)

2
.....upcase..... 
1. n : ℤ
2. [%1] : 0 < n
3. ℕ ~ (ℕ^(n - 1) + 1)
⊢ ℕ ~ (ℕ^n + 1)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mBbbN{}  \msim{}  (\mBbbN{}\^{}n  +  1)


By

---

Latex:
((Auto  THEN  NatInd  1)  THEN  Auto)

---

Home Index