---

Step * 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) ∈ ℚ)
⊢ ∀[a,b:ℚ].  ∀n:ℕ. ((a ↑ n - b ↑ n) = ((a - b) * Σ0 ≤ i < n. a ↑ i * b ↑ n - i + 1) ∈ ℚ)
BY
{ (Auto THEN CaseNat 0 `n') }

1
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) ∈ ℚ

2
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) ∈ ℚ

---

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))
\mvdash{}  \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:
(Auto  THEN  CaseNat  0  `n')

---

Home Index