Step * 2 1 of Lemma factorit_wf


1. ∀[d:ℕ]. ∀[x:ℕ+]. ∀[b:ℕ].
     (x b < d
      (2 ≤ b)
      (∀[tried:{L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((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)) ∈ ℤ)))
2. : ℕ+
3. : ℕ
4. 2 ≤ b
5. x < b
⊢ ∀[tried:{L:{p:ℕprime(p) ∧ p < b}  List| ∀p:{p:ℕprime(p)} (p <  ((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 ∈ ℤ)
BY
((InstHyp [⌜0⌝;⌜x⌝;⌜b⌝1⋅ THENA Auto') THEN Trivial) }


Latex:


Latex:

1.  \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\000C))\}  )))
2.  x  :  \mBbbN{}\msupplus{}
3.  b  :  \mBbbN{}
4.  2  \mleq{}  b
5.  x  <  b  *  b
\mvdash{}  \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))\}  )


By


Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  1\mcdot{}  THENA  Auto')  THEN  Trivial)




Home Index