---

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


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

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

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)
4. 1 = (u * reduce(λx,y. (x * y);1;v)) ∈ ℤ
5. u | 1
⊢ permutation(ℤ;[];[u / v])

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}u  |  1\mkleeneclose{}\mcdot{}

---

Home Index