---

Step * of Lemma assert-is_prime

∀n:ℕ. (↑is_prime(n) ⇐⇒ prime(n))
BY
{ xxx((UnivCD THENA Auto) THEN Unfold `is_prime` 0)xxx }

1
1. n : ℕ
⊢ ↑isl(TERMOF{decidable__prime:o, 1:l} n) ⇐⇒ prime(n)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  (\muparrow{}is\_prime(n)  \mLeftarrow{}{}\mRightarrow{}  prime(n))


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  Unfold  `is\_prime`  0)xxx

---

Home Index