---

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


1. u : ℕ@i
2. ¬(u = 0 ∈ ℤ)
3. ¬(u ~ 1)
4. ∀b,c:ℤ.  ((u | (b * c)) ⇒ ((u | b) ∨ (u | c)))
5. v : {m:ℕ| prime(m)}  List@i
6. (1 = reduce(λx,y. (x * y);1;v) ∈ ℤ) ⇒ permutation(ℤ;[];v)
7. 1 = (u * reduce(λx,y. (x * y);1;v)) ∈ ℤ
8. u | 1
⊢ False
BY
{ TACTIC:(D 3 THEN D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  u  :  \mBbbN{}@i
2.  \mneg{}(u  =  0)
3.  \mneg{}(u  \msim{}  1)
4.  \mforall{}b,c:\mBbbZ{}.    ((u  |  (b  *  c))  {}\mRightarrow{}  ((u  |  b)  \mvee{}  (u  |  c)))
5.  v  :  \{m:\mBbbN{}|  prime(m)\}    List@i
6.  (1  =  reduce(\mlambda{}x,y.  (x  *  y);1;v))  {}\mRightarrow{}  permutation(\mBbbZ{};[];v)
7.  1  =  (u  *  reduce(\mlambda{}x,y.  (x  *  y);1;v))
8.  u  |  1
\mvdash{}  False


By

---

Latex:
TACTIC:(D  3  THEN  D  0  THEN  Auto)

---

Home Index