---

Step * 2 of Lemma free-from-atom-rational


1. a : Atom1
2. q : ℚ
3. p : ℤ
4. q@0 : ℤ
5. 0 < q@0
6. ¬(q@0 = 0 ∈ ℚ)
7. q = (p/q@0) ∈ ℚ
8. ¬↑qeq(q@0;0)
9. q@0 ∈ ℤ-o
⊢ a#q@0:ℤ-o
BY
{ (Unfold `int_nzero` 0 THEN (FreeFromAtomSet THEN Auto) THEN FreeFromAtomTrivial THEN Auto)⋅ }

---

Latex:



1.  a  :  Atom1
2.  q  :  \mBbbQ{}
3.  p  :  \mBbbZ{}
4.  q@0  :  \mBbbZ{}
5.  0  <  q@0
6.  \mneg{}(q@0  =  0)
7.  q  =  (p/q@0)
8.  \mneg{}\muparrow{}qeq(q@0;0)
9.  q@0  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}
\mvdash{}  a\#q@0:\mBbbZ{}\msupminus{}\msupzero{}


By

(Unfold  `int\_nzero`  0  THEN  (FreeFromAtomSet  THEN  Auto)  THEN  FreeFromAtomTrivial  THEN  Auto)\mcdot{}

---

Home Index