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