---

Step * 1 2 1 1 of Lemma least-factor_wf


1. n : ℤ
2. 1 < |n|
3. (n rem |n|) = 0 ∈ ℤ
4. ∃m:ℕ|n| - 1. (↑((λi.(n rem i + 2 =z 0)) m))
5. ∃m:ℕ. (↑((λi.(n rem i + 2 =z 0)) m))
6. mu(λi.(n rem i + 2 =z 0)) ∈ ℕ
7. (↑((λi.(n rem i + 2 =z 0)) mu(λi.(n rem i + 2 =z 0))))
∧ (∀[i:ℕ]. ¬↑((λi.(n rem i + 2 =z 0)) i) supposing i < mu(λi.(n rem i + 2 =z 0)))
8. least-factor(n) ∈ ℕ
⊢ least-factor(n) ∈ {p:ℕ| 1 < p ∧ prime(p) ∧ (p | n) ∧ (∀q:ℕ. (prime(q) ⇒ (q | n) ⇒ (p ≤ q)))} 
BY
{ xxx((Assert 1 < least-factor(n) BY
             (Unfold `least-factor` 0 THEN Auto'))
      THEN (Assert mu(λi.(n rem i + 2 =z 0)) ~ least-factor(n) - 2 BY
                  (Unfold `least-factor` 0 THEN Auto'))
      THEN HypSubst' -1 -4
      THEN Reduce (-4)
      THEN (RW IntNormC (-4) THENA Auto))xxx }

1
1. n : ℤ
2. 1 < |n|
3. (n rem |n|) = 0 ∈ ℤ
4. ∃m:ℕ|n| - 1. (↑((λi.(n rem i + 2 =z 0)) m))
5. ∃m:ℕ. (↑((λi.(n rem i + 2 =z 0)) m))
6. mu(λi.(n rem i + 2 =z 0)) ∈ ℕ
7. (↑(n rem least-factor(n) =z 0)) ∧ (∀[i:ℕ]. ¬↑(n rem i + 2 =z 0) supposing i < least-factor(n) - 2)
8. least-factor(n) ∈ ℕ
9. 1 < least-factor(n)
10. mu(λi.(n rem i + 2 =z 0)) ~ least-factor(n) - 2
⊢ least-factor(n) ∈ {p:ℕ| 1 < p ∧ prime(p) ∧ (p | n) ∧ (∀q:ℕ. (prime(q) ⇒ (q | n) ⇒ (p ≤ q)))} 

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  1  <  |n|
3.  (n  rem  |n|)  =  0
4.  \mexists{}m:\mBbbN{}|n|  -  1.  (\muparrow{}((\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  m))
5.  \mexists{}m:\mBbbN{}.  (\muparrow{}((\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  m))
6.  mu(\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  \mmember{}  \mBbbN{}
7.  (\muparrow{}((\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  mu(\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))))
\mwedge{}  (\mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}((\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  i)  supposing  i  <  mu(\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0)))
8.  least-factor(n)  \mmember{}  \mBbbN{}
\mvdash{}  least-factor(n)  \mmember{}  \{p:\mBbbN{}|  1  <  p  \mwedge{}  prime(p)  \mwedge{}  (p  |  n)  \mwedge{}  (\mforall{}q:\mBbbN{}.  (prime(q)  {}\mRightarrow{}  (q  |  n)  {}\mRightarrow{}  (p  \mleq{}  q)))\} 


By

---

Latex:
xxx((Assert  1  <  least-factor(n)  BY
                      (Unfold  `least-factor`  0  THEN  Auto'))
        THEN  (Assert  mu(\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  \msim{}  least-factor(n)  -  2  BY
                                (Unfold  `least-factor`  0  THEN  Auto'))
        THEN  HypSubst'  -1  -4
        THEN  Reduce  (-4)
        THEN  (RW  IntNormC  (-4)  THENA  Auto))xxx

---

Home Index