---

Step * 2 1 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 ↑ 0 - b ↑ 0) = ((a - b) * Σ0 ≤ i < 0. a ↑ i * b ↑ 0 - i + 1) ∈ ℚ
BY
{ xxx((RWO "sum_unroll_base_q exp_zero_q" 0 THENA Auto) THEN QNorm 0)xxx }

---

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.  n  =  0
\mvdash{}  (a  \muparrow{}  0  -  b  \muparrow{}  0)  =  ((a  -  b)  *  \mSigma{}0  \mleq{}  i  <  0.  a  \muparrow{}  i  *  b  \muparrow{}  0  -  i  +  1)


By

---

Latex:
xxx((RWO  "sum\_unroll\_base\_q  exp\_zero\_q"  0  THENA  Auto)  THEN  QNorm  0)xxx

---

Home Index