---

Step * of Lemma posint_atom_imp_prime

∀a:Atom{<ℤ+,*>}. IsPrime(a)
BY
{ TACTIC:(RepUR ``matom_ty mprime matomic munit mreducible`` 0 THEN Auto) }

1
1. a : {a:ℕ+| (¬(a | 1)) ∧ (¬(∃b,c:ℕ+. ((¬(b | 1)) ∧ (¬(c | 1)) ∧ (a = (b * c) ∈ ℕ+))))} 
2. ¬(a | 1)
3. b : ℕ+
4. c : ℕ+
5. a | (b * c)
⊢ (a | b) ∨ (a | c)

---

Latex:

---

Latex:
\mforall{}a:Atom\{<\mBbbZ{}\msupplus{},*>\}.  IsPrime(a)


By

---

Latex:
TACTIC:(RepUR  ``matom\_ty  mprime  matomic  munit  mreducible``  0  THEN  Auto)

---

Home Index