---

Step * 1 1 2 1 1 1 1 1 of Lemma d-conv_wf

.....set predicate..... 
1. n : ℕ
2. two-factorizations(n)
= two-factorizations(n)
∈ bag({p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)} )
3. x1 : ℤ
4. x2 : ℤ
5. 1 ≤ x1
6. x1 ≤ n
7. (x1 * x2) = n ∈ ℤ
⊢ 0 ≤ x2
BY
{ xxx(Mul ⌜x1⌝ 0⋅ THEN Auto)xxx }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  n  :  \mBbbN{}
2.  two-factorizations(n)  =  two-factorizations(n)
3.  x1  :  \mBbbZ{}
4.  x2  :  \mBbbZ{}
5.  1  \mleq{}  x1
6.  x1  \mleq{}  n
7.  (x1  *  x2)  =  n
\mvdash{}  0  \mleq{}  x2


By

---

Latex:
xxx(Mul  \mkleeneopen{}x1\mkleeneclose{}  0\mcdot{}  THEN  Auto)xxx

---

Home Index