---

Step * 1 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#λz.(p/z):v:ℤ-o ─→ ℚ
BY
{ (FreeFromAtomApElim ⌈p⌉⋅ THEN FreeFromAtomTrivial)⋅ }

---

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\#\mlambda{}z.(p/z):v:\mBbbZ{}\msupminus{}\msupzero{}  {}\mrightarrow{}  \mBbbQ{}


By

(FreeFromAtomApElim  \mkleeneopen{}p\mkleeneclose{}\mcdot{}  THEN  FreeFromAtomTrivial)\mcdot{}

---

Home Index