---

Step * of Lemma prime-factors-unique

No Annotations
∀ps:{m:ℕ| prime(m)}  List. ∀qs:{qs:{m:ℕ| prime(m)}  List| Π(ps)  = Π(qs)  ∈ ℤ} .  permutation(ℤ;ps;qs)
BY
{ Assert ⌜∀ps,qs:{m:ℕ| prime(m)}  List.  ((Π(ps)  = Π(qs)  ∈ ℤ) ⇒ permutation(ℤ;ps;qs))⌝⋅ }

1
.....assertion..... 
∀ps,qs:{m:ℕ| prime(m)}  List.  ((Π(ps)  = Π(qs)  ∈ ℤ) ⇒ permutation(ℤ;ps;qs))

2
1. ∀ps,qs:{m:ℕ| prime(m)}  List.  ((Π(ps)  = Π(qs)  ∈ ℤ) ⇒ permutation(ℤ;ps;qs))
⊢ ∀ps:{m:ℕ| prime(m)}  List. ∀qs:{qs:{m:ℕ| prime(m)}  List| Π(ps)  = Π(qs)  ∈ ℤ} .  permutation(ℤ;ps;qs)

---

Latex:

---

Latex:
No  Annotations
\mforall{}ps:\{m:\mBbbN{}|  prime(m)\}    List.  \mforall{}qs:\{qs:\{m:\mBbbN{}|  prime(m)\}    List|  \mPi{}(ps)    =  \mPi{}(qs)  \}  .    permutation(\mBbbZ{};ps;qs)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}ps,qs:\{m:\mBbbN{}|  prime(m)\}    List.    ((\mPi{}(ps)    =  \mPi{}(qs)  )  {}\mRightarrow{}  permutation(\mBbbZ{};ps;qs))\mkleeneclose{}\mcdot{}

---

Home Index