---

Step * 1 of Lemma egyptian-fraction


1. a : ℕ
2. b : ℕ
3. 0 ≤ a
4. a < b
⊢ ∃L:ℕ+ List [((a/b) = Σ0 ≤ i < ||L||. (1/L[i]) ∈ ℚ)]
BY
{ xxx(RepeatFor 4 (MoveToConcl (-1)) THEN (GeneralInductionOnNat ⋅ THENA RepeatFor 2 (Auto)))xxx }

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

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(RepeatFor  4  (MoveToConcl  (-1))  THEN  (GeneralInductionOnNat  \mcdot{}  THENA  RepeatFor  2  (Auto)))xxx

---

Home Index