---

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

1
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 (ℕ × ℕ)

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(SubtypeReasoning1  THEN  Auto)xxx

---

Home Index