Step
*
1
1
2
of Lemma
qexp-difference-factor
1. a : ℚ
2. b : ℚ
3. n : ℕ
⊢ (a ↑ n + 1 + -(b ↑ n + 1))
= ((Σ0 + 1 ≤ i < n + 1. (a ↑ i * b ↑ n - i) * b + ((a ↑ n * 1) * a))
+ -(((1 * b ↑ n) * b) + Σ0 + 1 ≤ i < n + 1. (a ↑ i * b ↑ n - i) * b))
∈ ℚ
BY
{ xxx(((RW (AddrC [2;1] (LemmaC `exp_unroll_q`)) 0 THENA Auto)⋅
THEN (RW (AddrC [2;2;2] (LemmaC `exp_unroll_q`)) 0 THENA Auto)⋅
)
THEN QNorm 0
THEN Auto)xxx }
Latex:
Latex:
1. a : \mBbbQ{}
2. b : \mBbbQ{}
3. n : \mBbbN{}
\mvdash{} (a \muparrow{} n + 1 + -(b \muparrow{} n + 1))
= ((\mSigma{}0 + 1 \mleq{} i < n + 1. (a \muparrow{} i * b \muparrow{} n - i) * b + ((a \muparrow{} n * 1) * a))
+ -(((1 * b \muparrow{} n) * b) + \mSigma{}0 + 1 \mleq{} i < n + 1. (a \muparrow{} i * b \muparrow{} n - i) * b))
By
Latex:
xxx(((RW (AddrC [2;1] (LemmaC `exp\_unroll\_q`)) 0 THENA Auto)\mcdot{}
THEN (RW (AddrC [2;2;2] (LemmaC `exp\_unroll\_q`)) 0 THENA Auto)\mcdot{}
)
THEN QNorm 0
THEN Auto)xxx
Home
Index