---

Step * 1 1 1 of Lemma prime-factors-unique


∀qs:{m:ℕ| prime(m)}  List. ((1 = reduce(λx,y. (x * y);1;qs) ∈ ℤ) ⇒ permutation(ℤ;[];qs))
BY
{ (InductionOnList THEN Reduce 0)⋅ }

1
(1 = 1 ∈ ℤ) ⇒ permutation(ℤ;[];[])

2
1. u : {m:ℕ| prime(m)} @i
2. v : {m:ℕ| prime(m)}  List@i
3. (1 = reduce(λx,y. (x * y);1;v) ∈ ℤ) ⇒ permutation(ℤ;[];v)
⊢ (1 = (u * reduce(λx,y. (x * y);1;v)) ∈ ℤ) ⇒ permutation(ℤ;[];[u / v])

---

Latex:

---

Latex:

\mforall{}qs:\{m:\mBbbN{}|  prime(m)\}    List.  ((1  =  reduce(\mlambda{}x,y.  (x  *  y);1;qs))  {}\mRightarrow{}  permutation(\mBbbZ{};[];qs))


By

---

Latex:
(InductionOnList  THEN  Reduce  0)\mcdot{}

---

Home Index