---

Step * 1 1 2 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) ∧ (x1 ≤ n)) ∧ ((x1 * x2) = n ∈ ℤ)
⊢ <x1, x2> ∈ ℕ × ℕ
BY
{ xxxAutoxxx }

1
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 ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  two-factorizations(n)  =  two-factorizations(n)
3.  x1  :  \mBbbZ{}
4.  x2  :  \mBbbZ{}
5.  ((1  \mleq{}  x1)  \mwedge{}  (x1  \mleq{}  n))  \mwedge{}  ((x1  *  x2)  =  n)
\mvdash{}  <x1,  x2>  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}


By

---

Latex:
xxxAutoxxx

---

Home Index