---

Step * of Lemma egyptian-number

∀q:ℚ. (∃p:{ℤ × (ℕ+ List)| let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ})
BY
{ (Auto
   THEN (InstLemma `integer-fractional-parts` [⌜q⌝]⋅ THENA Auto)
   THEN (InstLemma `egyptian-fraction` [⌜fractional-part(q)⌝] ⋅ THENA Auto)
   THEN D -1
   THEN With <integer-part(q), L> (D 0)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  (\mexists{}p:\{\mBbbZ{}  \mtimes{}  (\mBbbN{}\msupplus{}  List)|  let  x,L  =  p  in  q  =  (x  +  \mSigma{}0  \mleq{}  i  <  ||L||.  (1/L[i]))\})


By

---

Latex:
(Auto
  THEN  (InstLemma  `integer-fractional-parts`  [\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `egyptian-fraction`  [\mkleeneopen{}fractional-part(q)\mkleeneclose{}]  \mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  With  <integer-part(q),  L>  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index