---

Step * 1 1 2 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 ∈ ℤ)} )
⊢ {p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)}  ⊆r (ℕ × ℕ)
BY
{ xxx(D 0 THENA Auto)xxx }

1
.....subterm..... T:t
1:n
1. n : ℕ
2. two-factorizations(n)
= two-factorizations(n)
∈ bag({p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)} )
3. x : {p:ℤ × ℤ| ((1 ≤ (fst(p))) ∧ ((fst(p)) ≤ n)) ∧ (((fst(p)) * (snd(p))) = n ∈ ℤ)} 
⊢ x ∈ ℕ × ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  two-factorizations(n)  =  two-factorizations(n)
\mvdash{}  \{p:\mBbbZ{}  \mtimes{}  \mBbbZ{}|  ((1  \mleq{}  (fst(p)))  \mwedge{}  ((fst(p))  \mleq{}  n))  \mwedge{}  (((fst(p))  *  (snd(p)))  =  n)\}    \msubseteq{}r  (\mBbbN{}  \mtimes{}  \mBbbN{})


By

---

Latex:
xxx(D  0  THENA  Auto)xxx

---

Home Index