---

Step * 1 of Lemma trial-division_wf


1. n : ℕ+
2. u : {2...}
3. v : {2...} List
4. trial-division(n;v) ∈ ∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))] + Top
5. y : Top
6. trial-division(n;v) = (inr y ) ∈ (∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))] + Top)
7. u < n
8. 1 < gcd(u;n)
⊢ gcd(u;n) < n
BY
{ ((Assert gcd(u;n) ≤ u BY ((BLemma `divisor_bound`  THEN Auto) THEN BLemma `gcd_is_divisor_1` THEN Auto)) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  u  :  \{2...\}
3.  v  :  \{2...\}  List
4.  trial-division(n;v)  \mmember{}  \mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))]  +  Top
5.  y  :  Top
6.  trial-division(n;v)  =  (inr  y  )
7.  u  <  n
8.  1  <  gcd(u;n)
\mvdash{}  gcd(u;n)  <  n


By

---

Latex:
((Assert  gcd(u;n)  \mleq{}  u  BY
                ((BLemma  `divisor\_bound`    THEN  Auto)  THEN  BLemma  `gcd\_is\_divisor\_1`  THEN  Auto))
  THEN  Auto
  )\mcdot{}

---

Home Index