---

Step * 1 of Lemma bag-member-two-factorizations


1. n : ℕ
2. a : ℤ
3. b : ℤ
⊢ uiff((<a, b> ∈ two-factorizations(n));(1 ≤ a) ∧ (a ≤ n) ∧ ((a * b) = n ∈ ℤ))
BY
{ xxx(Unfold `two-factorizations` 0 THEN (RWO "member-mapfilter" 0 THENA Auto))xxx }

1
1. n : ℕ
2. a : ℤ
3. b : ℤ
⊢ uiff(∃y:{x:ℤ| (1 ≤ x) ∧ x < n + 1} 
        ((y ∈ [1, n + 1)) ∧ ((↑((λa.(n rem a =z 0)) y)) c∧ (<a, b> = ((λa.<a, n ÷ a>) y) ∈ (ℤ × ℤ))));(1 ≤ a)
∧ (a ≤ n)
∧ ((a * b) = n ∈ ℤ))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
\mvdash{}  uiff((<a,  b>  \mmember{}  two-factorizations(n));(1  \mleq{}  a)  \mwedge{}  (a  \mleq{}  n)  \mwedge{}  ((a  *  b)  =  n))


By

---

Latex:
xxx(Unfold  `two-factorizations`  0  THEN  (RWO  "member-mapfilter"  0  THENA  Auto))xxx

---

Home Index