let a, b be Real; for s being natural Number holds (a + b) |^ s = Sum ((a,b) In_Power s)
let s be natural Number ; (a + b) |^ s = Sum ((a,b) In_Power s)
A0:
s is Nat
by TARSKI:1;
defpred S1[ Nat] means (a + b) |^ $1 = Sum ((a,b) In_Power $1);
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
reconsider a =
a,
b =
b as
Element of
REAL by XREAL_0:def 1;
let n be
Nat;
( S1[n] implies S1[n + 1] )
reconsider G1 =
(a * ((a,b) In_Power n)) ^ <*(In (0,REAL))*> as
FinSequence of
REAL ;
set G2 =
<*(In (0,REAL))*> ^ (b * ((a,b) In_Power n));
assume
S1[
n]
;
S1[n + 1]
then A2:
(a + b) |^ (n + 1) =
(a + b) * (Sum ((a,b) In_Power n))
by Th6
.=
(a * (Sum ((a,b) In_Power n))) + (b * (Sum ((a,b) In_Power n)))
.=
(Sum (a * ((a,b) In_Power n))) + (b * (Sum ((a,b) In_Power n)))
by RVSUM_1:87
.=
(Sum (a * ((a,b) In_Power n))) + (Sum (b * ((a,b) In_Power n)))
by RVSUM_1:87
;
len (<*(In (0,REAL))*> ^ (b * ((a,b) In_Power n))) =
(len <*0*>) + (len (b * ((a,b) In_Power n)))
by FINSEQ_1:22
.=
1
+ (len (b * ((a,b) In_Power n)))
by FINSEQ_1:40
.=
1
+ (len ((a,b) In_Power n))
by Th2
.=
(n + 1) + 1
by Def4
;
then reconsider F2 =
<*(In (0,REAL))*> ^ (b * ((a,b) In_Power n)) as
Element of
((n + 1) + 1) -tuples_on REAL by FINSEQ_2:92;
len G1 =
(len (a * ((a,b) In_Power n))) + (len <*0*>)
by FINSEQ_1:22
.=
(len (a * ((a,b) In_Power n))) + 1
by FINSEQ_1:40
.=
(len ((a,b) In_Power n)) + 1
by Th2
.=
(n + 1) + 1
by Def4
;
then reconsider F1 =
G1 as
Element of
((n + 1) + 1) -tuples_on REAL by FINSEQ_2:92;
A3:
Sum F2 =
0 + (Sum (b * ((a,b) In_Power n)))
by RVSUM_1:76
.=
Sum (b * ((a,b) In_Power n))
;
Sum F1 =
(Sum (a * ((a,b) In_Power n))) + 0
by RVSUM_1:74
.=
Sum (a * ((a,b) In_Power n))
;
then A4:
Sum (G1 + (<*(In (0,REAL))*> ^ (b * ((a,b) In_Power n)))) = (Sum (a * ((a,b) In_Power n))) + (Sum (b * ((a,b) In_Power n)))
by A3, RVSUM_1:89;
set F =
F1 + F2;
A5:
len F2 = (n + 1) + 1
by CARD_1:def 7;
A6:
len (F1 + F2) = (n + 1) + 1
by CARD_1:def 7;
A7:
len F1 = (n + 1) + 1
by CARD_1:def 7;
A8:
for
i being
Nat st
i in dom ((a,b) In_Power (n + 1)) holds
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
proof
let i be
Nat;
( i in dom ((a,b) In_Power (n + 1)) implies (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
assume A9:
i in dom ((a,b) In_Power (n + 1))
;
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
set r2 =
F2 /. i;
set r1 =
F1 /. i;
set r =
((a,b) In_Power n) /. i;
A10:
len ((a,b) In_Power (n + 1)) = (n + 1) + 1
by Def4;
then A11:
i in Seg ((n + 1) + 1)
by A9, FINSEQ_1:def 3;
then A12:
i in dom F1
by A7, FINSEQ_1:def 3;
A13:
i in dom F2
by A5, A11, FINSEQ_1:def 3;
A14:
(
i in {1} implies
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
proof
n + 1
>= 0 + 1
by XREAL_1:6;
then
1
in Seg (n + 1)
;
then
1
in Seg (len ((a,b) In_Power n))
by Def4;
then A15:
1
in dom ((a,b) In_Power n)
by FINSEQ_1:def 3;
then A16:
1
in dom (a * ((a,b) In_Power n))
by VALUED_1:def 5;
assume
i in {1}
;
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
then A17:
i = 1
by TARSKI:def 1;
then A18:
((a,b) In_Power n) /. i = ((a,b) In_Power n) . 1
by A15, PARTFUN1:def 6;
((a,b) In_Power n) /. i = ((a,b) In_Power n) . i
by A17, A15, PARTFUN1:def 6;
then A19:
((a,b) In_Power n) /. i = a |^ n
by A17, Th28;
A20:
F1 /. i =
((a * ((a,b) In_Power n)) ^ <*0*>) . 1
by A12, A17, PARTFUN1:def 6
.=
(a * ((a,b) In_Power n)) . 1
by A16, FINSEQ_1:def 7
.=
a * (a |^ n)
by A18, A19, RVSUM_1:44
.=
a |^ (n + 1)
by Th6
;
A21:
F2 /. i = F2 . i
by A13, PARTFUN1:def 6;
A22:
F1 /. i = F1 . i
by A12, PARTFUN1:def 6;
F2 /. i =
(<*0*> ^ (b * ((a,b) In_Power n))) . 1
by A13, A17, PARTFUN1:def 6
.=
0
by FINSEQ_1:41
;
then (F1 + F2) . i =
(F1 /. i) + 0
by A22, A21, RVSUM_1:11
.=
((a,b) In_Power (n + 1)) . i
by A17, A20, Th28
;
hence
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
;
verum
end;
i >= 1
by A11, FINSEQ_1:1;
then reconsider j =
i - 1 as
Element of
NAT by INT_1:5;
set x =
((a,b) In_Power n) /. j;
A23:
i = j + 1
;
A24:
i in dom (F1 + F2)
by A6, A11, FINSEQ_1:def 3;
A25:
(
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 A26:
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:5;
A27:
F1 /. i = ((a * ((a,b) In_Power n)) ^ <*0*>) . i
by A12, PARTFUN1:def 6;
1
<= j
by A23, A26, NAT_1:13;
then reconsider m2 =
j - 1 as
Element of
NAT by INT_1:5;
A28:
j <= n + 1
by A23, A26, XREAL_1:6;
then
j - 1
<= (n + 1) - 1
by XREAL_1:9;
then reconsider l2 =
n - m2 as
Element of
NAT by INT_1:5;
1
<= j
by A23, A26, NAT_1:13;
then
j in Seg (n + 1)
by A28;
then
j in Seg (len ((a,b) In_Power n))
by Def4;
then A29:
j in dom ((a,b) In_Power n)
by FINSEQ_1:def 3;
then A30:
((a,b) In_Power n) /. j = ((a,b) In_Power n) . j
by PARTFUN1:def 6;
A31:
i <= n + 1
by A26, NAT_1:13;
then
i in Seg (n + 1)
by A26;
then
i in Seg (len ((a,b) In_Power n))
by Def4;
then A32:
i in dom ((a,b) In_Power n)
by FINSEQ_1:def 3;
then A33:
((a,b) In_Power n) /. i = ((a,b) In_Power n) . i
by PARTFUN1:def 6;
i in dom (a * ((a,b) In_Power n))
by A32, VALUED_1:def 5;
then A34:
F1 /. i =
(a * ((a,b) In_Power n)) . i
by A27, FINSEQ_1:def 7
.=
a * (((a,b) In_Power n) /. i)
by A33, RVSUM_1:44
;
i - 1
<= (n + 1) - 1
by A31, XREAL_1:9;
then reconsider l1 =
n - m1 as
Element of
NAT by INT_1:5;
A35:
l1 + 1
= (n + 1) - (m2 + 1)
;
A36:
j in dom (b * ((a,b) In_Power n))
by A29, VALUED_1:def 5;
A37:
F2 /. i = (<*0*> ^ (b * ((a,b) In_Power n))) . i
by A13, PARTFUN1:def 6;
then F2 /. i =
(<*0*> ^ (b * ((a,b) In_Power n))) . ((len <*0*>) + j)
by A23, FINSEQ_1:40
.=
(b * ((a,b) In_Power n)) . j
by A36, FINSEQ_1:def 7
.=
b * (((a,b) In_Power n) /. j)
by A30, RVSUM_1:44
;
then (F1 + F2) . i =
(a * (((a,b) In_Power n) /. i)) + (b * (((a,b) In_Power n) /. j))
by A24, A27, A37, A34, VALUED_1:def 1
.=
(a * (((a |^ l1) * (n choose m1)) * (b |^ m1))) + (b * (((a,b) In_Power n) /. j))
by A32, A33, Def4
.=
((a * (a |^ l1)) * ((n choose m1) * (b |^ m1))) + (b * (((a,b) In_Power n) /. j))
.=
((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (b * (((a,b) In_Power n) /. j))
by Th6
.=
((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (b * ((b |^ m2) * ((n choose m2) * (a |^ l2))))
by A29, A30, Def4
.=
((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + ((b * (b |^ m2)) * ((n choose m2) * (a |^ l2)))
.=
((a |^ (l1 + 1)) * ((n choose (m2 + 1)) * (b |^ (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2)))
by Th6
.=
(((n choose (m2 + 1)) + (n choose m2)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1))
.=
(((n + 1) choose (m2 + 1)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1))
by Th22
.=
((a,b) In_Power (n + 1)) . i
by A9, A35, Def4
;
hence
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
;
verum
end;
A38:
(
i in {((n + 1) + 1)} implies
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
proof
assume A39:
i in {((n + 1) + 1)}
;
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
then A40:
i = (n + 1) + 1
by TARSKI:def 1;
A41:
j =
((n + 1) + 1) - 1
by A39, TARSKI:def 1
.=
n + 1
;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then
j in Seg (len ((a,b) In_Power n))
by A41, Def4;
then A42:
j in dom ((a,b) In_Power n)
by FINSEQ_1:def 3;
then A43:
((a,b) In_Power n) /. j =
((a,b) In_Power n) . (n + 1)
by A41, PARTFUN1:def 6
.=
b |^ n
by Th29
;
A44:
((a,b) In_Power n) /. j = ((a,b) In_Power n) . j
by A42, PARTFUN1:def 6;
A45:
j in dom (b * ((a,b) In_Power n))
by A42, VALUED_1:def 5;
A46:
F2 /. i =
(<*0*> ^ (b * ((a,b) In_Power n))) . ((1 + n) + 1)
by A13, A40, PARTFUN1:def 6
.=
(<*0*> ^ (b * ((a,b) In_Power n))) . ((len <*0*>) + j)
by A41, FINSEQ_1:39
.=
(b * ((a,b) In_Power n)) . j
by A45, FINSEQ_1:def 7
.=
b * (b |^ n)
by A44, A43, RVSUM_1:44
.=
b |^ (n + 1)
by Th6
;
A47:
F2 /. i = F2 . i
by A13, PARTFUN1:def 6;
n + 1 =
len ((a,b) In_Power n)
by Def4
.=
len (a * ((a,b) In_Power n))
by Th2
;
then A48:
F1 /. i =
((a * ((a,b) In_Power n)) ^ <*0*>) . ((len (a * ((a,b) In_Power n))) + 1)
by A12, A40, PARTFUN1:def 6
.=
0
by FINSEQ_1:42
;
F1 /. i = F1 . i
by A12, PARTFUN1:def 6;
then (F1 + F2) . i =
0 + (F2 /. i)
by A48, A47, RVSUM_1:11
.=
((a,b) In_Power (n + 1)) . i
by A40, A46, Th29
;
hence
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
;
verum
end;
dom ((a,b) In_Power (n + 1)) = Seg ((n + 1) + 1)
by A10, FINSEQ_1:def 3;
hence
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
by A9, A49, Th1, NAT_1:12;
verum
end;
len ((a,b) In_Power (n + 1)) = len (F1 + F2)
by A6, Def4;
hence
S1[
n + 1]
by A2, A4, A8, FINSEQ_2:9;
verum
end;
(a + b) |^ 0 =
Sum <*(In (1,REAL))*>
by FINSOP_1:11, RVSUM_1:94
.=
Sum ((a,b) In_Power 0)
by Th27
;
then A50:
S1[ 0 ]
;
for n being Nat holds S1[n]
from NAT_1:sch 2(A50, A1);
hence
(a + b) |^ s = Sum ((a,b) In_Power s)
by A0; verum