---

Step * of Lemma decidable__prime

∀n:ℕ. Dec(prime(n))
BY
{ (Auto THEN Assert ⌜prime(n) ⇐⇒ atomic(n)⌝⋅) }

1
.....assertion..... 
1. n : ℕ@i
⊢ prime(n) ⇐⇒ atomic(n)

2
1. n : ℕ@i
2. prime(n) ⇐⇒ atomic(n)
⊢ Dec(prime(n))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  Dec(prime(n))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}prime(n)  \mLeftarrow{}{}\mRightarrow{}  atomic(n)\mkleeneclose{}\mcdot{})

---

Home Index