---

Step * of Lemma qexp-difference-factor

∀[a,b:ℚ].  ∀n:ℕ. ((a ↑ n - b ↑ n) = ((a - b) * Σ0 ≤ i < n. a ↑ i * b ↑ n - i + 1) ∈ ℚ)
BY
{ xxxAssert ⌜∀[a,b:ℚ].  ∀n:ℕ. ((a ↑ n + 1 - b ↑ n + 1) = ((a - b) * Σ0 ≤ i < n + 1. a ↑ i * b ↑ n - i) ∈ ℚ)⌝⋅xxx }

1
.....assertion..... 
∀[a,b:ℚ].  ∀n:ℕ. ((a ↑ n + 1 - b ↑ n + 1) = ((a - b) * Σ0 ≤ i < n + 1. a ↑ i * b ↑ n - i) ∈ ℚ)

2
1. ∀[a,b:ℚ].  ∀n:ℕ. ((a ↑ n + 1 - b ↑ n + 1) = ((a - b) * Σ0 ≤ i < n + 1. a ↑ i * b ↑ n - i) ∈ ℚ)
⊢ ∀[a,b:ℚ].  ∀n:ℕ. ((a ↑ n - b ↑ n) = ((a - b) * Σ0 ≤ i < n. a ↑ i * b ↑ n - i + 1) ∈ ℚ)

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    \mforall{}n:\mBbbN{}.  ((a  \muparrow{}  n  -  b  \muparrow{}  n)  =  ((a  -  b)  *  \mSigma{}0  \mleq{}  i  <  n.  a  \muparrow{}  i  *  b  \muparrow{}  n  -  i  +  1))


By

---

Latex:
xxxAssert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}xxx

---

Home Index