---

Step * of Lemma not-prime-mult

∀[n,m:{2...}]. ∀[x:ℤ].  (¬prime((n * m) * x))
BY
{ ((Auto THEN (D 0 THENA Auto)) THEN (FLemma `prime-mult` [-1] THENA Auto)) }

1
.....wf..... 
1. n : {2...}
2. m : {2...}
3. x : ℤ
4. prime((n * m) * x)
⊢ n * m ∈ {2...}

2
1. n : {2...}
2. m : {2...}
3. x : ℤ
4. prime((n * m) * x)
5. prime(n * m)
⊢ False

---

Latex:

---

Latex:
\mforall{}[n,m:\{2...\}].  \mforall{}[x:\mBbbZ{}].    (\mneg{}prime((n  *  m)  *  x))


By

---

Latex:
((Auto  THEN  (D  0  THENA  Auto))  THEN  (FLemma  `prime-mult`  [-1]  THENA  Auto))

---

Home Index