---

Step * 1 1 of Lemma prime-factors-unique


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

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(InductionOnList  THEN  Reduce  0)

---

Home Index