---

Step * 1 2 1 1 1 1 1 of Lemma least-factor_wf

.....assertion..... 
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. least-factor(n) | n
8. ∀[i:ℕ]. ¬↑(n rem i + 2 =z 0) supposing i < least-factor(n) - 2
9. least-factor(n) ∈ ℕ
10. 1 < least-factor(n)
11. mu(λi.(n rem i + 2 =z 0)) ~ least-factor(n) - 2
⊢ ∀i:ℕ. (1 < i ⇒ i < least-factor(n) ⇒ (¬(i | n)))
BY
{ (Auto THEN InstHyp [⌜i - 2⌝] (-7)⋅ THEN 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. least-factor(n) | n
8. ∀[i:ℕ]. ¬↑(n rem i + 2 =z 0) supposing i < least-factor(n) - 2
9. least-factor(n) ∈ ℕ
10. 1 < least-factor(n)
11. mu(λi.(n rem i + 2 =z 0)) ~ least-factor(n) - 2
12. i : ℕ
13. 1 < i
14. i < least-factor(n)
15. ¬↑(n rem (i - 2) + 2 =z 0)
⊢ ¬(i | n)

---

Latex:

---

Latex:
.....assertion..... 
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.  least-factor(n)  |  n
8.  \mforall{}[i:\mBbbN{}].  \mneg{}\muparrow{}(n  rem  i  +  2  =\msubz{}  0)  supposing  i  <  least-factor(n)  -  2
9.  least-factor(n)  \mmember{}  \mBbbN{}
10.  1  <  least-factor(n)
11.  mu(\mlambda{}i.(n  rem  i  +  2  =\msubz{}  0))  \msim{}  least-factor(n)  -  2
\mvdash{}  \mforall{}i:\mBbbN{}.  (1  <  i  {}\mRightarrow{}  i  <  least-factor(n)  {}\mRightarrow{}  (\mneg{}(i  |  n)))


By

---

Latex:
(Auto  THEN  InstHyp  [\mkleeneopen{}i  -  2\mkleeneclose{}]  (-7)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index