---

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


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 ∈ ℤ
⊢ x2 ∈ ℕ
BY
{ (MemTypeCD THEN Auto) }

1
.....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

---

Latex:

---

Latex:

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{}  x2  \mmember{}  \mBbbN{}


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index