---

Step * 1 1 1 1 of Lemma egyptian-fraction


1. a : ℕ
2. a = 0 ∈ ℤ
3. b : ℕ
4. 0 ≤ 0
5. 0 < b
⊢ ∃L:ℕ+ List [((0/b) = Σ0 ≤ i < ||L||. (1/L[i]) ∈ ℚ)]
BY
{ ((Thin (-2) THEN Auto) THEN With ⌜[]⌝ (D 0)⋅ THEN Auto) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}
2.  a  =  0
3.  b  :  \mBbbN{}
4.  0  \mleq{}  0
5.  0  <  b
\mvdash{}  \mexists{}L:\mBbbN{}\msupplus{}  List  [((0/b)  =  \mSigma{}0  \mleq{}  i  <  ||L||.  (1/L[i]))]


By

---

Latex:
((Thin  (-2)  THEN  Auto)  THEN  With  \mkleeneopen{}[]\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index