Step
*
of Lemma
equipollent-primes
ℕ ~ {p:ℕ| prime(p)}
BY
{ (BLemma `equipollent-nat-decidable-subset` THEN Auto) }
1
1. m : ℕ@i
⊢ ∃p:ℕ. (prime(p) ∧ (m ≤ p))
Latex:
Latex:
\mBbbN{} \msim{} \{p:\mBbbN{}| prime(p)\}
By
Latex:
(BLemma `equipollent-nat-decidable-subset` THEN Auto)
Home
Index