---

Step * of Lemma egyptian-fraction

∀r:{r:ℚ| (0 ≤ r) ∧ r < 1} . (∃L:ℕ+ List [(r = Σ0 ≤ i < ||L||. (1/L[i]) ∈ ℚ)])
BY
{ (Auto
   THEN D -1
   THEN (Assert (0 ≤ r) ∧ r < 1 BY
               (Unhide THEN Auto))
   THEN Thin (-2)
   THEN (InstLemma `fractional-part-rep` [⌜r⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN HypSubst' -1 0
   THEN Auto
   THEN ThinVar `r') }

1
1. a : ℕ
2. b : ℕ
3. 0 ≤ a
4. a < b
⊢ ∃L:ℕ+ List [((a/b) = Σ0 ≤ i < ||L||. (1/L[i]) ∈ ℚ)]

---

Latex:

---

Latex:
\mforall{}r:\{r:\mBbbQ{}|  (0  \mleq{}  r)  \mwedge{}  r  <  1\}  .  (\mexists{}L:\mBbbN{}\msupplus{}  List  [(r  =  \mSigma{}0  \mleq{}  i  <  ||L||.  (1/L[i]))])


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  (Assert  (0  \mleq{}  r)  \mwedge{}  r  <  1  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-2)
  THEN  (InstLemma  `fractional-part-rep`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  HypSubst'  -1  0
  THEN  Auto
  THEN  ThinVar  `r')

---

Home Index