let R be non empty add-cancelable left_zeroed unital associative commutative distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a, b being Element of R
for n being Element of NAT holds (a + b) |^ n = Sum (a,b In_Power n)
let a, b be Element of R; :: thesis: for n being Element of NAT holds (a + b) |^ n = Sum (a,b In_Power n)
let n be Element of NAT ; :: thesis: (a + b) |^ n = Sum (a,b In_Power n)
defpred S1[ Element of NAT ] means (a + b) |^ $1 = Sum (a,b In_Power $1);
A1:
S1[ 0 ]
A2:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )
assume
S1[
n]
;
:: thesis: S1[n + 1]
then A3:
(a + b) |^ (n + 1) =
(Sum (a,b In_Power n)) * (a + b)
by GROUP_1:def 8
.=
((Sum (a,b In_Power n)) * a) + ((Sum (a,b In_Power n)) * b)
by VECTSP_1:def 11
.=
(Sum ((a,b In_Power n) * a)) + ((Sum (a,b In_Power n)) * b)
by Th5
.=
(Sum ((a,b In_Power n) * a)) + (Sum ((a,b In_Power n) * b))
by Th5
;
set G1 =
((a,b In_Power n) * a) ^ <*(0. R)*>;
set G2 =
<*(0. R)*> ^ ((a,b In_Power n) * b);
A4:
Seg (len ((a,b In_Power n) * a)) =
dom ((a,b In_Power n) * a)
by FINSEQ_1:def 3
.=
dom (a,b In_Power n)
by POLYNOM1:def 3
.=
Seg (len (a,b In_Power n))
by FINSEQ_1:def 3
;
A5:
Seg (len ((a,b In_Power n) * b)) =
dom ((a,b In_Power n) * b)
by FINSEQ_1:def 3
.=
dom (a,b In_Power n)
by POLYNOM1:def 3
.=
Seg (len (a,b In_Power n))
by FINSEQ_1:def 3
;
len (((a,b In_Power n) * a) ^ <*(0. R)*>) =
(len ((a,b In_Power n) * a)) + (len <*(0. R)*>)
by FINSEQ_1:35
.=
(len ((a,b In_Power n) * a)) + 1
by FINSEQ_1:57
.=
(len (a,b In_Power n)) + 1
by A4, FINSEQ_1:8
.=
(n + 1) + 1
by Def10
;
then reconsider F1 =
((a,b In_Power n) * a) ^ <*(0. R)*> as
Element of
((n + 1) + 1) -tuples_on the
carrier of
R by FINSEQ_2:110;
len (<*(0. R)*> ^ ((a,b In_Power n) * b)) =
(len ((a,b In_Power n) * b)) + (len <*(0. R)*>)
by FINSEQ_1:35
.=
(len ((a,b In_Power n) * b)) + 1
by FINSEQ_1:57
.=
(len (a,b In_Power n)) + 1
by A5, FINSEQ_1:8
.=
(n + 1) + 1
by Def10
;
then reconsider F2 =
<*(0. R)*> ^ ((a,b In_Power n) * b) as
Element of
((n + 1) + 1) -tuples_on the
carrier of
R by FINSEQ_2:110;
A6:
len F1 = (n + 1) + 1
by FINSEQ_1:def 18;
A7:
len F2 = (n + 1) + 1
by FINSEQ_1:def 18;
A8:
dom F1 =
Seg (len F1)
by FINSEQ_1:def 3
.=
dom F2
by A6, A7, FINSEQ_1:def 3
;
A9:
Sum F1 =
(Sum ((a,b In_Power n) * a)) + (Sum <*(0. R)*>)
by RLVECT_1:58
.=
(Sum ((a,b In_Power n) * a)) + (0. R)
by Th3
.=
Sum ((a,b In_Power n) * a)
by RLVECT_1:def 7
;
Sum F2 =
(Sum <*(0. R)*>) + (Sum ((a,b In_Power n) * b))
by RLVECT_1:58
.=
(0. R) + (Sum ((a,b In_Power n) * b))
by Th3
.=
Sum ((a,b In_Power n) * b)
by ALGSTR_1:def 5
;
then A10:
Sum ((((a,b In_Power n) * a) ^ <*(0. R)*>) + (<*(0. R)*> ^ ((a,b In_Power n) * b))) = (Sum ((a,b In_Power n) * a)) + (Sum ((a,b In_Power n) * b))
by A8, A9, Th7;
set F =
F1 + F2;
A11:
Seg (len (F1 + F2)) =
dom (F1 + F2)
by FINSEQ_1:def 3
.=
dom F1
by A8, Def4
.=
Seg (len F1)
by FINSEQ_1:def 3
;
then A12:
len (F1 + F2) = (n + 1) + 1
by A6, FINSEQ_1:8;
A13:
for
i being
Nat st 1
<= i &
i <= len (a,b In_Power (n + 1)) holds
(F1 + F2) . i = (a,b In_Power (n + 1)) . i
proof
let i be
Nat;
:: thesis: ( 1 <= i & i <= len (a,b In_Power (n + 1)) implies (F1 + F2) . i = (a,b In_Power (n + 1)) . i )
assume A14:
( 1
<= i &
i <= len (a,b In_Power (n + 1)) )
;
:: thesis: (F1 + F2) . i = (a,b In_Power (n + 1)) . i
A15:
len (a,b In_Power (n + 1)) = (n + 1) + 1
by Def10;
then A16:
dom (a,b In_Power (n + 1)) = Seg ((n + 1) + 1)
by FINSEQ_1:def 3;
then A17:
i in dom (a,b In_Power (n + 1))
by A14, A15, FINSEQ_1:3;
A18:
i in Seg ((n + 1) + 1)
by A14, A15, FINSEQ_1:3;
reconsider j =
i - 1 as
Element of
NAT by A14, INT_1:18;
A19:
i in dom (F1 + F2)
by A6, A11, A18, FINSEQ_1:def 3;
A20:
i in dom F1
by A6, A18, FINSEQ_1:def 3;
A21:
i in dom F2
by A7, A18, FINSEQ_1:def 3;
A22:
i = j + 1
;
set x =
(a,b In_Power n) /. j;
set r =
(a,b In_Power n) /. i;
set r1 =
F1 /. i;
set r2 =
F2 /. i;
A23:
i <= len (F1 + F2)
by A12, A14, Def10;
A24:
(
i in {1} implies
(F1 + F2) . i = (a,b In_Power (n + 1)) . i )
proof
assume
i in {1}
;
:: thesis: (F1 + F2) . i = (a,b In_Power (n + 1)) . i
then A25:
i = 1
by TARSKI:def 1;
n + 1
>= 0 + 1
by XREAL_1:8;
then
1
in Seg (n + 1)
by FINSEQ_1:3;
then A26:
1
in Seg (len (a,b In_Power n))
by Def10;
then A27:
1
in dom (a,b In_Power n)
by FINSEQ_1:def 3;
A28:
1
in dom ((a,b In_Power n) * a)
by A4, A26, FINSEQ_1:def 3;
A29:
(a,b In_Power n) /. i = (a,b In_Power n) . i
by A25, A27, PARTFUN1:def 8;
A30:
F1 /. i =
(((a,b In_Power n) * a) ^ <*(0. R)*>) . 1
by A20, A25, PARTFUN1:def 8
.=
((a,b In_Power n) * a) . 1
by A28, FINSEQ_1:def 7
.=
((a,b In_Power n) * a) /. 1
by A28, PARTFUN1:def 8
.=
((a,b In_Power n) /. 1) * a
by A27, POLYNOM1:def 3
.=
(a |^ n) * a
by A25, A29, Th24
.=
a |^ (n + 1)
by GROUP_1:def 8
;
A31:
F2 /. i =
(<*(0. R)*> ^ ((a,b In_Power n) * b)) . 1
by A21, A25, PARTFUN1:def 8
.=
0. R
by FINSEQ_1:58
;
thus (F1 + F2) . i =
(F1 + F2) /. i
by A19, PARTFUN1:def 8
.=
(F1 /. i) + (F2 /. i)
by A8, A14, A23, Def4
.=
a |^ (n + 1)
by A30, A31, RLVECT_1:def 7
.=
(a,b In_Power (n + 1)) . i
by A25, Th24
;
:: thesis: verum
end;
A32:
(
i in {((n + 1) + 1)} implies
(F1 + F2) . i = (a,b In_Power (n + 1)) . i )
proof
assume A33:
i in {((n + 1) + 1)}
;
:: thesis: (F1 + F2) . i = (a,b In_Power (n + 1)) . i
then A34:
i = (n + 1) + 1
by TARSKI:def 1;
dom (F1 + F2) = Seg ((n + 1) + 1)
by A6, A11, FINSEQ_1:def 3;
then A35:
i in dom (F1 + F2)
by A14, A34, FINSEQ_1:3;
A36:
j =
((n + 1) + 1) - 1
by A33, TARSKI:def 1
.=
n + 1
;
A37:
n + 1 =
len (a,b In_Power n)
by Def10
.=
len ((a,b In_Power n) * a)
by A4, FINSEQ_1:8
;
n + 1
in Seg (n + 1)
by FINSEQ_1:6;
then A38:
j in Seg (len (a,b In_Power n))
by A36, Def10;
then A39:
j in dom (a,b In_Power n)
by FINSEQ_1:def 3;
A40:
j in dom ((a,b In_Power n) * b)
by A5, A38, FINSEQ_1:def 3;
A41:
(a,b In_Power n) /. j =
(a,b In_Power n) . (n + 1)
by A36, A39, PARTFUN1:def 8
.=
b |^ n
by Th25
;
A42:
F1 /. i =
(((a,b In_Power n) * a) ^ <*(0. R)*>) . ((len ((a,b In_Power n) * a)) + 1)
by A20, A34, A37, PARTFUN1:def 8
.=
0. R
by FINSEQ_1:59
;
A43:
F2 /. i =
(<*(0. R)*> ^ ((a,b In_Power n) * b)) . (1 + (n + 1))
by A21, A34, PARTFUN1:def 8
.=
(<*(0. R)*> ^ ((a,b In_Power n) * b)) . ((len <*(0. R)*>) + j)
by A36, FINSEQ_1:56
.=
((a,b In_Power n) * b) . j
by A40, FINSEQ_1:def 7
.=
((a,b In_Power n) * b) /. j
by A40, PARTFUN1:def 8
.=
(b |^ n) * b
by A39, A41, POLYNOM1:def 3
.=
b |^ (n + 1)
by GROUP_1:def 8
;
thus (F1 + F2) . i =
(F1 + F2) /. i
by A35, PARTFUN1:def 8
.=
(0. R) + (F2 /. i)
by A8, A14, A23, A42, Def4
.=
b |^ (n + 1)
by A43, ALGSTR_1:def 5
.=
(a,b In_Power (n + 1)) . i
by A34, Th25
;
:: thesis: verum
end;
A44:
(
i in { k where k is Element of NAT : ( k > 1 & k < (n + 1) + 1 ) } implies
(F1 + F2) . i = (a,b In_Power (n + 1)) . i )
proof
assume
i in { k where k is Element of NAT : ( 1 < k & k < (n + 1) + 1 ) }
;
:: thesis: (F1 + F2) . i = (a,b In_Power (n + 1)) . i
then A45:
ex
k being
Element of
NAT st
(
k = i & 1
< k &
k < (n + 1) + 1 )
;
then A46:
( 1
<= i &
i <= n + 1 )
by NAT_1:13;
then
i in Seg (n + 1)
by FINSEQ_1:3;
then A47:
i in Seg (len (a,b In_Power n))
by Def10;
then A48:
i in dom (a,b In_Power n)
by FINSEQ_1:def 3;
A49:
i in dom ((a,b In_Power n) * a)
by A4, A47, FINSEQ_1:def 3;
reconsider m1 =
i - 1 as
Element of
NAT by A45, INT_1:18;
i - 1
<= (n + 1) - 1
by A46, XREAL_1:11;
then reconsider l1 =
n - m1 as
Element of
NAT by INT_1:18;
A50:
( 1
<= j &
j + 1
<= (n + 1) + 1 )
by A22, A45, NAT_1:13;
A51:
( 1
<= j &
j <= n + 1 )
by A22, A45, NAT_1:13, XREAL_1:8;
then
j in Seg (n + 1)
by FINSEQ_1:3;
then A52:
j in Seg (len (a,b In_Power n))
by Def10;
then A53:
j in dom (a,b In_Power n)
by FINSEQ_1:def 3;
A54:
j in dom ((a,b In_Power n) * b)
by A5, A52, FINSEQ_1:def 3;
reconsider m2 =
j - 1 as
Element of
NAT by A50, INT_1:18;
A55:
l1 + 1
= (n + 1) - (m2 + 1)
;
j - 1
<= (n + 1) - 1
by A51, XREAL_1:11;
then reconsider l2 =
n - m2 as
Element of
NAT by INT_1:18;
A56:
j in dom ((a,b In_Power n) * b)
by A5, A52, FINSEQ_1:def 3;
A57:
F1 /. i = (((a,b In_Power n) * a) ^ <*(0. R)*>) . i
by A20, PARTFUN1:def 8;
A58:
F2 /. i = (<*(0. R)*> ^ ((a,b In_Power n) * b)) . i
by A21, PARTFUN1:def 8;
A59:
F1 /. i =
((a,b In_Power n) * a) . i
by A49, A57, FINSEQ_1:def 7
.=
((a,b In_Power n) * a) /. i
by A49, PARTFUN1:def 8
.=
((a,b In_Power n) /. i) * a
by A48, POLYNOM1:def 3
;
A60:
F2 /. i =
(<*(0. R)*> ^ ((a,b In_Power n) * b)) . ((len <*(0. R)*>) + j)
by A22, A58, FINSEQ_1:57
.=
((a,b In_Power n) * b) . j
by A54, FINSEQ_1:def 7
.=
((a,b In_Power n) * b) /. j
by A56, PARTFUN1:def 8
.=
((a,b In_Power n) /. j) * b
by A53, POLYNOM1:def 3
;
thus (F1 + F2) . i =
(F1 + F2) /. i
by A19, PARTFUN1:def 8
.=
(F1 /. i) + (((a,b In_Power n) /. j) * b)
by A8, A14, A23, A60, Def4
.=
((((n choose m1) * (a |^ l1)) * (b |^ m1)) * a) + (((a,b In_Power n) /. j) * b)
by A48, A59, Def10
.=
((((a |^ l1) * (n choose m1)) * (b |^ m1)) * a) + (((a,b In_Power n) /. j) * b)
by Th18
.=
(a * ((a |^ l1) * ((n choose m1) * (b |^ m1)))) + (((a,b In_Power n) /. j) * b)
by Th22
.=
((a * (a |^ l1)) * ((n choose m1) * (b |^ m1))) + (((a,b In_Power n) /. j) * b)
by GROUP_1:def 4
.=
((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (((a,b In_Power n) /. j) * b)
by GROUP_1:def 8
.=
((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (((b |^ m2) * ((n choose m2) * (a |^ l2))) * b)
by A53, Def10
.=
((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (((b |^ m2) * b) * ((n choose m2) * (a |^ l2)))
by GROUP_1:def 4
.=
((a |^ (l1 + 1)) * ((n choose (m2 + 1)) * (b |^ (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))
by GROUP_1:def 8
.=
(((b |^ (m2 + 1)) * (a |^ (l1 + 1))) * (n choose (m2 + 1))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))
by Th21
.=
((b |^ (m2 + 1)) * ((n choose (m2 + 1)) * (a |^ (l1 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))
by Th21
.=
((b |^ (m2 + 1)) * ((a |^ (l1 + 1)) * (n choose (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))
by Th18
.=
(((a |^ (l1 + 1)) * (n choose (m2 + 1))) + ((n choose m2) * (a |^ l2))) * (b |^ (m2 + 1))
by VECTSP_1:def 18
.=
(((n choose (m2 + 1)) * (a |^ (l1 + 1))) + ((n choose m2) * (a |^ (l1 + 1)))) * (b |^ (m2 + 1))
by Th18
.=
(((n choose (m2 + 1)) + (n choose m2)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1))
by Th16
.=
(((n + 1) choose (m2 + 1)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1))
by NEWTON:32
.=
(a,b In_Power (n + 1)) /. i
by A17, A55, Def10
.=
(a,b In_Power (n + 1)) . i
by A17, PARTFUN1:def 8
;
:: thesis: verum
end;
hence
(F1 + F2) . i = (a,b In_Power (n + 1)) . i
by A16, A17, NAT_1:12, NEWTON:5;
:: thesis: verum
end;
len (a,b In_Power (n + 1)) = len (F1 + F2)
by A12, Def10;
hence
S1[
n + 1]
by A3, A10, A13, FINSEQ_1:18;
:: thesis: verum
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A1, A2);
hence
(a + b) |^ n = Sum (a,b In_Power n)
; :: thesis: verum