---

Step * of Lemma atomic_char

∀a:ℤ. (atomic(a) ⇐⇒ {(¬(a ~ 1)) ∧ (∀b:ℤ. ((b | a) ⇒ ((b ~ 1) ∨ (b ~ a))))})
BY
{ (Unfolds ``guard atomic`` 0 THEN GenExRepD THEN Auto) }

1
1. a : ℤ@i
2. ¬(a = 0 ∈ ℤ)
3. ¬(a ~ 1)
4. ¬reducible(a)
5. b : ℤ@i
6. b | a
⊢ (b ~ 1) ∨ (b ~ a)

2
1. a : ℤ@i
2. ¬(a ~ 1)
3. ∀b:ℤ. ((b | a) ⇒ ((b ~ 1) ∨ (b ~ a)))
⊢ ¬(a = 0 ∈ ℤ)

3
1. a : ℤ@i
2. ¬(a ~ 1)
3. ∀b:ℤ. ((b | a) ⇒ ((b ~ 1) ∨ (b ~ a)))
⊢ ¬reducible(a)

---

Latex:

---

Latex:
\mforall{}a:\mBbbZ{}.  (atomic(a)  \mLeftarrow{}{}\mRightarrow{}  \{(\mneg{}(a  \msim{}  1))  \mwedge{}  (\mforall{}b:\mBbbZ{}.  ((b  |  a)  {}\mRightarrow{}  ((b  \msim{}  1)  \mvee{}  (b  \msim{}  a))))\})


By

---

Latex:
(Unfolds  ``guard  atomic``  0  THEN  GenExRepD  THEN  Auto)

---

Home Index