---

Step * 1 1 1 1 of Lemma atomic_char


1. a : ℤ@i
2. ¬(a = 0 ∈ ℤ)
3. ¬(a ~ 1)
4. b : ℤ@i
5. c : ℤ@i
6. a = (b * c) ∈ ℤ
7. ¬(b ~ 1)
8. ¬(b ~ a)
9. ¬((b * c) = 0 ∈ ℤ)
10. ¬(b = 0 ∈ ℤ)
11. ¬(c = 0 ∈ ℤ)
⊢ ∃b,c:ℤ-o. ((¬(b ~ 1)) ∧ (¬(c ~ 1)) ∧ (a = (b * c) ∈ ℤ))
BY
{ ((InstConcl [⌜b⌝;⌜c⌝] THEN Auto)
   THEN ((HypSubst 6 8 THENM D 0) THENA Auto)
   THEN (D 8 THEN RWO  "-1" 0 THEN Auto)
   THEN (RW IntNormC 0 THEN Auto)
   THEN RelRST
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  \mneg{}(a  =  0)
3.  \mneg{}(a  \msim{}  1)
4.  b  :  \mBbbZ{}@i
5.  c  :  \mBbbZ{}@i
6.  a  =  (b  *  c)
7.  \mneg{}(b  \msim{}  1)
8.  \mneg{}(b  \msim{}  a)
9.  \mneg{}((b  *  c)  =  0)
10.  \mneg{}(b  =  0)
11.  \mneg{}(c  =  0)
\mvdash{}  \mexists{}b,c:\mBbbZ{}\msupminus{}\msupzero{}.  ((\mneg{}(b  \msim{}  1))  \mwedge{}  (\mneg{}(c  \msim{}  1))  \mwedge{}  (a  =  (b  *  c)))


By

---

Latex:
((InstConcl  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  THEN  Auto)
  THEN  ((HypSubst  6  8  THENM  D  0)  THENA  Auto)
  THEN  (D  8  THEN  RWO    "-1"  0  THEN  Auto)
  THEN  (RW  IntNormC  0  THEN  Auto)
  THEN  RelRST
  THEN  Auto)

---

Home Index