---

Step * 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)
⊢ ∃b,c:ℤ-o. ((¬(b ~ 1)) ∧ (¬(c ~ 1)) ∧ (a = (b * c) ∈ ℤ))
BY
{ ((CopyToEnd 2 THENM (HypSubst 6 (-1) THENA Auto))
THENM ((Sel (-1) (FLemma `zero_ann_b` [-1]) THENM D (-1)) THENA Auto)
) }

1
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) ∈ ℤ))

---

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)
\mvdash{}  \mexists{}b,c:\mBbbZ{}\msupminus{}\msupzero{}.  ((\mneg{}(b  \msim{}  1))  \mwedge{}  (\mneg{}(c  \msim{}  1))  \mwedge{}  (a  =  (b  *  c)))


By

---

Latex:
((CopyToEnd  2  THENM  (HypSubst  6  (-1)  THENA  Auto))
THENM  ((Sel  (-1)  (FLemma  `zero\_ann\_b`  [-1])  THENM  D  (-1))  THENA  Auto)
)

---

Home Index