---

Step * 1 of Lemma least-factor_wf


1. n : ℤ
2. 1 < |n|
⊢ least-factor(n) ∈ {p:ℕ| 1 < p ∧ prime(p) ∧ (p | n) ∧ (∀q:ℕ. (prime(q) ⇒ (q | n) ⇒ (p ≤ q)))} 
BY
{ xxxAssert ⌜(n rem |n|) = 0 ∈ ℤ⌝⋅xxx }

1
.....assertion..... 
1. n : ℤ
2. 1 < |n|
⊢ (n rem |n|) = 0 ∈ ℤ

2
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)))} 

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  1  <  |n|
\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:
xxxAssert  \mkleeneopen{}(n  rem  |n|)  =  0\mkleeneclose{}\mcdot{}xxx

---

Home Index