---

Step * 2 2 of Lemma qexp-difference-factor


1. ∀[a,b:ℚ].  ∀n:ℕ. ((a ↑ n + 1 - b ↑ n + 1) = ((a - b) * Σ0 ≤ i < n + 1. a ↑ i * b ↑ n - i) ∈ ℚ)
2. a : ℚ
3. b : ℚ
4. n : ℕ
5. ¬(n = 0 ∈ ℤ)
⊢ (a ↑ n - b ↑ n) = ((a - b) * Σ0 ≤ i < n. a ↑ i * b ↑ n - i + 1) ∈ ℚ
BY
{ ((InstHyp [⌜a⌝;⌜b⌝;⌜n - 1⌝] 1⋅ THENA Auto) THEN NthHypEq (-1) THEN RepeatFor 3 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

1.  \mforall{}[a,b:\mBbbQ{}].    \mforall{}n:\mBbbN{}.  ((a  \muparrow{}  n  +  1  -  b  \muparrow{}  n  +  1)  =  ((a  -  b)  *  \mSigma{}0  \mleq{}  i  <  n  +  1.  a  \muparrow{}  i  *  b  \muparrow{}  n  -  i))
2.  a  :  \mBbbQ{}
3.  b  :  \mBbbQ{}
4.  n  :  \mBbbN{}
5.  \mneg{}(n  =  0)
\mvdash{}  (a  \muparrow{}  n  -  b  \muparrow{}  n)  =  ((a  -  b)  *  \mSigma{}0  \mleq{}  i  <  n.  a  \muparrow{}  i  *  b  \muparrow{}  n  -  i  +  1)


By

---

Latex:
((InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}n  -  1\mkleeneclose{}]  1\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index