---

Step * of Lemma not-prime-square

∀[x:ℤ]. (¬prime(x * x))
BY
{ (Auto THEN (D 0 THENA Auto) THEN FLemma  `prime_imp_atomic` [-1] THEN Auto THEN RepeatFor 3 (D -1)) }

1
1. x : ℤ
2. prime(x * x)
3. ¬((x * x) = 0 ∈ ℤ)
4. ¬((x * x) ~ 1)
⊢ reducible(x * x)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  FLemma    `prime\_imp\_atomic`  [-1]  THEN  Auto  THEN  RepeatFor  3  (D  -1))

---

Home Index