---

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