Step
*
of Lemma
factorit_wf
∀[x:ℕ+]. ∀[b:ℕ].
∀[tried:{L:{p:ℕ| prime(p) ∧ p < b} List| ∀p:{p:ℕ| prime(p)} . (p < b
⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
∀[facs:{p:ℕ| prime(p)} List].
(factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)} List| reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs))\000C ∈ ℤ} )
supposing 2 ≤ b
BY
{ Assert ⌜∀[d:ℕ]. ∀[x:ℕ+]. ∀[b:ℕ].
(x - b * b < d
⇒ (2 ≤ b)
⇒ (∀[tried:{L:{p:ℕ| prime(p) ∧ p < b} List| ∀p:{p:ℕ| prime(p)} . (p < b
⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
∀[facs:{p:ℕ| prime(p)} List].
(factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)} List|
reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} )))⌝⋅\000C }
1
.....assertion.....
∀[d:ℕ]. ∀[x:ℕ+]. ∀[b:ℕ].
(x - b * b < d
⇒ (2 ≤ b)
⇒ (∀[tried:{L:{p:ℕ| prime(p) ∧ p < b} List| ∀p:{p:ℕ| prime(p)} . (p < b
⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
∀[facs:{p:ℕ| prime(p)} List].
(factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)} List| reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;fa\000Ccs)) ∈ ℤ} )))
2
1. ∀[d:ℕ]. ∀[x:ℕ+]. ∀[b:ℕ].
(x - b * b < d
⇒ (2 ≤ b)
⇒ (∀[tried:{L:{p:ℕ| prime(p) ∧ p < b} List| ∀p:{p:ℕ| prime(p)} . (p < b
⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
∀[facs:{p:ℕ| prime(p)} List].
(factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)} List|
reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs)) ∈ ℤ} )))
⊢ ∀[x:ℕ+]. ∀[b:ℕ].
∀[tried:{L:{p:ℕ| prime(p) ∧ p < b} List| ∀p:{p:ℕ| prime(p)} . (p < b
⇒ ((p ∈ L) ∧ (¬(p | x))))} ].
∀[facs:{p:ℕ| prime(p)} List].
(factorit(x;b;tried;facs) ∈ {L:{p:ℕ| prime(p)} List| reduce(λp,q. (p * q);1;L) = (x * reduce(λp,q. (p * q);1;facs\000C)) ∈ ℤ} )
supposing 2 ≤ b
Latex:
Latex:
\mforall{}[x:\mBbbN{}\msupplus{}]. \mforall{}[b:\mBbbN{}].
\mforall{}[tried:\{L:\{p:\mBbbN{}| prime(p) \mwedge{} p < b\} List| \mforall{}p:\{p:\mBbbN{}| prime(p)\} . (p < b {}\mRightarrow{} ((p \mmember{} L) \mwedge{} (\mneg{}(p | x))))\} \000C].
\mforall{}[facs:\{p:\mBbbN{}| prime(p)\} List].
(factorit(x;b;tried;facs) \mmember{} \{L:\{p:\mBbbN{}| prime(p)\} List|
reduce(\mlambda{}p,q. (p * q);1;L) = (x * reduce(\mlambda{}p,q. (p * q);1;facs))\} )
supposing 2 \mleq{} b
By
Latex:
Assert \mkleeneopen{}\mforall{}[d:\mBbbN{}]. \mforall{}[x:\mBbbN{}\msupplus{}]. \mforall{}[b:\mBbbN{}].
(x - b * b < d
{}\mRightarrow{} (2 \mleq{} b)
{}\mRightarrow{} (\mforall{}[tried:\{L:\{p:\mBbbN{}| prime(p) \mwedge{} p < b\} List|
\mforall{}p:\{p:\mBbbN{}| prime(p)\} . (p < b {}\mRightarrow{} ((p \mmember{} L) \mwedge{} (\mneg{}(p | x))))\} ].
\mforall{}[facs:\{p:\mBbbN{}| prime(p)\} List].
(factorit(x;b;tried;facs) \mmember{} \{L:\{p:\mBbbN{}| prime(p)\} List|
reduce(\mlambda{}p,q. (p * q);1;L)
= (x * reduce(\mlambda{}p,q. (p * q);1;facs))\} )))\mkleeneclose{}\mcdot{}
Home
Index