---

Step * of Lemma bag-member-two-factorizations

∀[n:ℕ]. ∀[a,b:ℤ].  uiff(<a, b> ↓∈ two-factorizations(n);(1 ≤ a) ∧ (a ≤ n) ∧ ((a * b) = n ∈ ℤ))
BY
{ xxx((UnivCD THENA Auto) THEN (RWO "bag-member-list" 0 THENA Auto))xxx }

1
1. n : ℕ
2. a : ℤ
3. b : ℤ
⊢ uiff((<a, b> ∈ two-factorizations(n));(1 ≤ a) ∧ (a ≤ n) ∧ ((a * b) = n ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbZ{}].    uiff(<a,  b>  \mdownarrow{}\mmember{}  two-factorizations(n);(1  \mleq{}  a)  \mwedge{}  (a  \mleq{}  n)  \mwedge{}  ((a  *  b)  =  n))


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  (RWO  "bag-member-list"  0  THENA  Auto))xxx

---

Home Index