---

Step * of Lemma free-from-atom-rational

∀[a:Atom1]. ∀[q:ℚ].  a#q:ℚ
BY
{ (Auto THEN (At ⌈𝕌'⌉ ElimRationals⋅ THEN Auto) THEN (Assert q@0 ∈ ℤ-o BY Auto) THEN FreeFromAtomApElim ⌈q@0⌉⋅) }

1
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 ─→ ℚ

2
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

---

Latex:


\mforall{}[a:Atom1].  \mforall{}[q:\mBbbQ{}].    a\#q:\mBbbQ{}


By

(Auto
  THEN  (At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  ElimRationals\mcdot{}  THEN  Auto)
  THEN  (Assert  q@0  \mmember{}  \mBbbZ{}\msupminus{}\msupzero{}  BY
                          Auto)
  THEN  FreeFromAtomApElim  \mkleeneopen{}q@0\mkleeneclose{}\mcdot{})

---

Home Index