Step
*
2
1
1
2
of Lemma
prime-factors
1. n : {2...}
2. factorit(n;2;[];[])
= factorit(n;2;[];[])
∈ {L:{p:ℕ| prime(p)} List| reduce(λp,q. (p * q);1;L) = (n * reduce(λp,q. (p * q);1;[])) ∈ ℤ}
3. x : {p:ℕ| prime(p)} List
4. reduce(λp,q. (p * q);1;x) = (n * 1) ∈ ℤ
5. x = x ∈ ({p:ℕ| prime(p)} List)
⊢ ∀x:ℕ. (prime(x)
⇒ prime(x))
BY
{ Auto }
Latex:
Latex:
1. n : \{2...\}
2. factorit(n;2;[];[]) = factorit(n;2;[];[])
3. x : \{p:\mBbbN{}| prime(p)\} List
4. reduce(\mlambda{}p,q. (p * q);1;x) = (n * 1)
5. x = x
\mvdash{} \mforall{}x:\mBbbN{}. (prime(x) {}\mRightarrow{} prime(x))
By
Latex:
Auto
Home
Index