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