---

Step * 1 1 2 1 2 1 1 1 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))
4. qs : {m:ℕ| prime(m)}  List
5. (u * reduce(λx,y. (x * y);1;v)) = reduce(λx,y. (x * y);1;qs) ∈ ℤ
6. (u ∈ qs)
7. L' : {m:ℕ| prime(m)}  List
8. {permutation({m:ℕ| prime(m)} ;qs;[u / L'])}
9. permutation({m:ℕ| prime(m)} ;qs;[u / L'])
⊢ ...system_error_message... permutation(ℤ;qs;[u / L'])
BY
{ (Unfold `label` 0 THEN RepeatFor 3 (ParallelLast)) }

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) ∈ ℤ
6. (u ∈ qs)
7. L' : {m:ℕ| prime(m)}  List
8. {permutation({m:ℕ| prime(m)} ;qs;[u / L'])}
9. f : ℕ||qs|| ⟶ ℕ||qs||
10. Inj(ℕ||qs||;ℕ||qs||;f)
11. [u / L'] = (qs o f) ∈ ({m:ℕ| prime(m)}  List)
⊢ [u / L'] = (qs o f) ∈ (ℤ List)

---

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))
4.  qs  :  \{m:\mBbbN{}|  prime(m)\}    List
5.  (u  *  reduce(\mlambda{}x,y.  (x  *  y);1;v))  =  reduce(\mlambda{}x,y.  (x  *  y);1;qs)
6.  (u  \mmember{}  qs)
7.  L'  :  \{m:\mBbbN{}|  prime(m)\}    List
8.  \{permutation(\{m:\mBbbN{}|  prime(m)\}  ;qs;[u  /  L'])\}
9.  permutation(\{m:\mBbbN{}|  prime(m)\}  ;qs;[u  /  L'])
\mvdash{}  ...system\_error\_message...  permutation(\mBbbZ{};qs;[u  /  L'])


By

---

Latex:
(Unfold  `label`  0  THEN  RepeatFor  3  (ParallelLast))

---

Home Index