---

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


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))
BY
{ Auto }

1
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))
4. qs : {m:ℕ| prime(m)}  List
5. (u * reduce(λx,y. (x * y);1;v)) = reduce(λx,y. (x * y);1;qs) ∈ ℤ
⊢ permutation(ℤ;[u / v];qs)

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index