---

Step * 2 of Lemma prime-factors-unique


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)
BY
{ TACTIC:(RepeatFor 2 (ParallelLast) THEN D -1 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}ps,qs:\{m:\mBbbN{}|  prime(m)\}    List.    ((\mPi{}(ps)    =  \mPi{}(qs)  )  {}\mRightarrow{}  permutation(\mBbbZ{};ps;qs))
\mvdash{}  \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:
TACTIC:(RepeatFor  2  (ParallelLast)  THEN  D  -1  THEN  Auto)

---

Home Index