---

Step * 1 of Lemma atomic_char


1. a : ℤ@i
2. ¬(a = 0 ∈ ℤ)
3. ¬(a ~ 1)
4. ¬reducible(a)
5. b : ℤ@i
6. b | a
⊢ (b ~ 1) ∨ (b ~ a)
BY
{ (((((NegateConcl2 THEN Auto) THENA (BLemma `stable__from_decidable` THEN Auto)) THENM RWH (LemmaC `not_over_or`) (-1))
   THENM D (-1)
   )
   THENA Auto
   ) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  \mneg{}(a  =  0)
3.  \mneg{}(a  \msim{}  1)
4.  \mneg{}reducible(a)
5.  b  :  \mBbbZ{}@i
6.  b  |  a
\mvdash{}  (b  \msim{}  1)  \mvee{}  (b  \msim{}  a)


By

---

Latex:
(((((NegateConcl2  THEN  Auto)  THENA  (BLemma  `stable\_\_from\_decidable`  THEN  Auto))
    THENM  RWH  (LemmaC  `not\_over\_or`)  (-1)
    )
  THENM  D  (-1)
  )
  THENA  Auto
  )

---

Home Index