---

Step * 1 2 of Lemma least-factor_wf


1. n : ℤ
2. 1 < |n|
3. (n rem |n|) = 0 ∈ ℤ
⊢ least-factor(n) ∈ {p:ℕ| 1 < p ∧ prime(p) ∧ (p | n) ∧ (∀q:ℕ. (prime(q) ⇒ (q | n) ⇒ (p ≤ q)))} 
BY
{ ((Assert ∃m:ℕ|n| - 1. (↑((λi.(n rem i + 2 =z 0)) m)) BY
          (Reduce 0
           THEN InstConcl [⌜|n| - 2⌝]⋅
           THEN Auto'
           THEN (RW IntNormC 0 THEN Auto)
           THEN RW assert_pushdownC 0
           THEN Auto))
   THEN (Assert ∃m:ℕ. (↑((λi.(n rem i + 2 =z 0)) m)) BY
               (All Reduce THEN ParallelLast))
   THEN (InstLemma `mu_wf` [⌜λi.(n rem i + 2 =z 0)⌝]⋅ THENA Auto)
   THEN (InstLemma `mu-property` [⌜λi.(n rem i + 2 =z 0)⌝]⋅ THENA Auto)) }

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. (↑((λ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)))
⊢ 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
\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:
((Assert  \mexists{}m:\mBbbN{}|n|  -  1.  (\muparrow{}((\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  m))  BY
                (Reduce  0
                  THEN  InstConcl  [\mkleeneopen{}|n|  -  2\mkleeneclose{}]\mcdot{}
                  THEN  Auto'
                  THEN  (RW  IntNormC  0  THEN  Auto)
                  THEN  RW  assert\_pushdownC  0
                  THEN  Auto))
  THEN  (Assert  \mexists{}m:\mBbbN{}.  (\muparrow{}((\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  m))  BY
                          (All  Reduce  THEN  ParallelLast))
  THEN  (InstLemma  `mu\_wf`  [\mkleeneopen{}\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `mu-property`  [\mkleeneopen{}\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0)\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index