---

Step * of Lemma atomic_imp_prime

∀a:ℤ. prime(a) supposing atomic(a)
BY
{ ((UnivCD THENM FLemma `atomic_char` [-1]) THENA Auto) }

1
1. a : ℤ
2. atomic(a)
3. (¬(a ~ 1)) ∧ (∀b:ℤ. ((b | a) ⇒ ((b ~ 1) ∨ (b ~ a))))
⊢ prime(a)

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  prime(a)  supposing  atomic(a)


By

---

Latex:
((UnivCD  THENM  FLemma  `atomic\_char`  [-1])  THENA  Auto)

---

Home Index