let s be Nat; :: thesis: for a, b being real number holds (a + b) |^ s = Sum (a,b In_Power s)
let a, b be real number ; :: thesis: (a + b) |^ s = Sum (a,b In_Power s)
defpred S1[ Nat] means (a + b) |^ $1 = Sum (a,b In_Power $1);
(a + b) |^ 0 =
1
by RVSUM_1:124
.=
Sum <*1*>
by FINSOP_1:12
.=
Sum (a,b In_Power 0 )
by Th38
;
then A1:
S1[ 0 ]
;
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
:: thesis: S1[n + 1]
reconsider a =
a,
b =
b as
Real by XREAL_0:def 1;
A4:
(a + b) |^ (n + 1) =
(a + b) * (Sum (a,b In_Power n))
by A3, Th11
.=
(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:117
.=
(Sum (a * (a,b In_Power n))) + (Sum (b * (a,b In_Power n)))
by RVSUM_1:117
;
reconsider G1 =
(a * (a,b In_Power n)) ^ <*0 *> as
FinSequence of
REAL ;
set G2 =
<*0 *> ^ (b * (a,b In_Power n));
len G1 =
(len (a * (a,b In_Power n))) + (len <*0 *>)
by FINSEQ_1:35
.=
(len (a * (a,b In_Power n))) + 1
by FINSEQ_1:57
.=
(len (a,b In_Power n)) + 1
by Th6
.=
(n + 1) + 1
by Def4
;
then reconsider F1 =
G1 as
Element of
((n + 1) + 1) -tuples_on REAL by FINSEQ_2:110;
A5:
len F1 = (n + 1) + 1
by FINSEQ_1:def 18;
len (<*0 *> ^ (b * (a,b In_Power n))) =
(len <*0 *>) + (len (b * (a,b In_Power n)))
by FINSEQ_1:35
.=
1
+ (len (b * (a,b In_Power n)))
by FINSEQ_1:57
.=
1
+ (len (a,b In_Power n))
by Th6
.=
(n + 1) + 1
by Def4
;
then reconsider F2 =
<*0 *> ^ (b * (a,b In_Power n)) as
Element of
((n + 1) + 1) -tuples_on REAL by FINSEQ_2:110;
A6:
len F2 = (n + 1) + 1
by FINSEQ_1:def 18;
A7:
Sum F1 =
(Sum (a * (a,b In_Power n))) + 0
by RVSUM_1:104
.=
Sum (a * (a,b In_Power n))
;
Sum F2 =
0 + (Sum (b * (a,b In_Power n)))
by RVSUM_1:106
.=
Sum (b * (a,b In_Power n))
;
then A8:
Sum (G1 + (<*0 *> ^ (b * (a,b In_Power n)))) = (Sum (a * (a,b In_Power n))) + (Sum (b * (a,b In_Power n)))
by A7, RVSUM_1:119;
set F =
F1 + F2;
A9:
len (F1 + F2) = (n + 1) + 1
by FINSEQ_1:def 18;
A10:
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;
:: thesis: ( i in dom (a,b In_Power (n + 1)) implies (F1 + F2) . i = (a,b In_Power (n + 1)) . i )
assume A11:
i in dom (a,b In_Power (n + 1))
;
:: thesis: (F1 + F2) . i = (a,b In_Power (n + 1)) . i
A12:
len (a,b In_Power (n + 1)) = (n + 1) + 1
by Def4;
then A13:
dom (a,b In_Power (n + 1)) = Seg ((n + 1) + 1)
by FINSEQ_1:def 3;
A14:
i in Seg ((n + 1) + 1)
by A11, A12, FINSEQ_1:def 3;
then
(
i >= 1 &
(n + 1) + 1
>= i )
by FINSEQ_1:3;
then reconsider j =
i - 1 as
Element of
NAT by INT_1:18;
A15:
i in dom (F1 + F2)
by A9, A14, FINSEQ_1:def 3;
A16:
i in dom F1
by A5, A14, FINSEQ_1:def 3;
A17:
i in dom F2
by A6, A14, FINSEQ_1:def 3;
A18:
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;
A19:
(
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 A20:
i = 1
by TARSKI:def 1;
n + 1
>= 0 + 1
by XREAL_1:8;
then
1
in Seg (n + 1)
;
then
1
in Seg (len (a,b In_Power n))
by Def4;
then A21:
1
in dom (a,b In_Power n)
by FINSEQ_1:def 3;
then A22:
1
in dom (a * (a,b In_Power n))
by Th7;
A23:
(a,b In_Power n) /. i = (a,b In_Power n) . i
by A20, A21, PARTFUN1:def 8;
A24:
(a,b In_Power n) /. i = (a,b In_Power n) . 1
by A20, A21, PARTFUN1:def 8;
A25:
(a,b In_Power n) /. i = a |^ n
by A20, A23, Th39;
A26:
F1 /. i = F1 . i
by A16, PARTFUN1:def 8;
A27:
F1 /. i =
((a * (a,b In_Power n)) ^ <*0 *>) . 1
by A16, A20, PARTFUN1:def 8
.=
(a * (a,b In_Power n)) . 1
by A22, FINSEQ_1:def 7
.=
a * (a |^ n)
by A24, A25, RVSUM_1:66
.=
a |^ (n + 1)
by Th11
;
A28:
F2 /. i = F2 . i
by A17, PARTFUN1:def 8;
F2 /. i =
(<*0 *> ^ (b * (a,b In_Power n))) . 1
by A17, A20, PARTFUN1:def 8
.=
0
by FINSEQ_1:58
;
then (F1 + F2) . i =
(F1 /. i) + 0
by A26, A28, RVSUM_1:27
.=
(a,b In_Power (n + 1)) . i
by A20, A27, Th39
;
hence
(F1 + F2) . i = (a,b In_Power (n + 1)) . i
;
:: thesis: verum
end;
A29:
(
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 A30:
ex
k being
Element of
NAT st
(
k = i & 1
< k &
k < (n + 1) + 1 )
;
then A31:
( 1
<= i &
i <= n + 1 )
by NAT_1:13;
then
i in Seg (n + 1)
by A30;
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:
i in dom (a * (a,b In_Power n))
by Th7;
reconsider m1 =
i - 1 as
Element of
NAT by A30, INT_1:18;
i - 1
<= (n + 1) - 1
by A31, XREAL_1:11;
then reconsider l1 =
n - m1 as
Element of
NAT by INT_1:18;
A34:
( 1
<= j &
j + 1
<= (n + 1) + 1 )
by A18, A30, NAT_1:13;
A35:
( 1
<= j &
j <= n + 1 )
by A18, A30, NAT_1:13, XREAL_1:8;
then
j in Seg (n + 1)
;
then
j in Seg (len (a,b In_Power n))
by Def4;
then A36:
j in dom (a,b In_Power n)
by FINSEQ_1:def 3;
then A37:
j in dom (b * (a,b In_Power n))
by Th7;
reconsider m2 =
j - 1 as
Element of
NAT by A34, INT_1:18;
A38:
l1 + 1
= (n + 1) - (m2 + 1)
;
j - 1
<= (n + 1) - 1
by A35, XREAL_1:11;
then reconsider l2 =
n - m2 as
Element of
NAT by INT_1:18;
A39:
(a,b In_Power n) /. j = (a,b In_Power n) . j
by A36, PARTFUN1:def 8;
A40:
(a,b In_Power n) /. i = (a,b In_Power n) . i
by A32, PARTFUN1:def 8;
A41:
F1 /. i = ((a * (a,b In_Power n)) ^ <*0 *>) . i
by A16, PARTFUN1:def 8;
A42:
F2 /. i = (<*0 *> ^ (b * (a,b In_Power n))) . i
by A17, PARTFUN1:def 8;
A43:
F1 /. i =
(a * (a,b In_Power n)) . i
by A33, A41, FINSEQ_1:def 7
.=
a * ((a,b In_Power n) /. i)
by A40, RVSUM_1:66
;
F2 /. i =
(<*0 *> ^ (b * (a,b In_Power n))) . ((len <*0 *>) + j)
by A18, A42, FINSEQ_1:57
.=
(b * (a,b In_Power n)) . j
by A37, FINSEQ_1:def 7
.=
b * ((a,b In_Power n) /. j)
by A39, RVSUM_1:66
;
then (F1 + F2) . i =
(a * ((a,b In_Power n) /. i)) + (b * ((a,b In_Power n) /. j))
by A15, A41, A42, A43, VALUED_1:def 1
.=
(a * (((a |^ l1) * (n choose m1)) * (b |^ m1))) + (b * ((a,b In_Power n) /. j))
by A32, A40, 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 Th11
.=
((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (b * ((b |^ m2) * ((n choose m2) * (a |^ l2))))
by A36, A39, 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 Th11
.=
(((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 Th32
.=
(a,b In_Power (n + 1)) . i
by A11, A38, Def4
;
hence
(F1 + F2) . i = (a,b In_Power (n + 1)) . i
;
:: thesis: verum
end;
A44:
(
i in {((n + 1) + 1)} implies
(F1 + F2) . i = (a,b In_Power (n + 1)) . i )
proof
assume A45:
i in {((n + 1) + 1)}
;
:: thesis: (F1 + F2) . i = (a,b In_Power (n + 1)) . i
then A46:
i = (n + 1) + 1
by TARSKI:def 1;
A47:
j =
((n + 1) + 1) - 1
by A45, TARSKI:def 1
.=
n + 1
;
A48:
n + 1 =
len (a,b In_Power n)
by Def4
.=
len (a * (a,b In_Power n))
by Th6
;
n + 1
in Seg (n + 1)
by FINSEQ_1:6;
then
j in Seg (len (a,b In_Power n))
by A47, Def4;
then A49:
j in dom (a,b In_Power n)
by FINSEQ_1:def 3;
then A50:
j in dom (b * (a,b In_Power n))
by Th7;
A51:
(a,b In_Power n) /. j = (a,b In_Power n) . j
by A49, PARTFUN1:def 8;
A52:
(a,b In_Power n) /. j =
(a,b In_Power n) . (n + 1)
by A47, A49, PARTFUN1:def 8
.=
b |^ n
by Th40
;
A53:
F1 /. i = F1 . i
by A16, PARTFUN1:def 8;
A54:
F1 /. i =
((a * (a,b In_Power n)) ^ <*0 *>) . ((len (a * (a,b In_Power n))) + 1)
by A16, A46, A48, PARTFUN1:def 8
.=
0
by FINSEQ_1:59
;
A55:
F2 /. i = F2 . i
by A17, PARTFUN1:def 8;
A56:
F2 /. i =
(<*0 *> ^ (b * (a,b In_Power n))) . ((1 + n) + 1)
by A17, A46, PARTFUN1:def 8
.=
(<*0 *> ^ (b * (a,b In_Power n))) . ((len <*0 *>) + j)
by A47, FINSEQ_1:56
.=
(b * (a,b In_Power n)) . j
by A50, FINSEQ_1:def 7
.=
b * (b |^ n)
by A51, A52, RVSUM_1:66
.=
b |^ (n + 1)
by Th11
;
(F1 + F2) . i =
0 + (F2 /. i)
by A53, A54, A55, RVSUM_1:27
.=
(a,b In_Power (n + 1)) . i
by A46, A56, Th40
;
hence
(F1 + F2) . i = (a,b In_Power (n + 1)) . i
;
:: thesis: verum
end;
hence
(F1 + F2) . i = (a,b In_Power (n + 1)) . i
by A11, A13, Th5, NAT_1:12;
:: thesis: verum
end;
len (a,b In_Power (n + 1)) = len (F1 + F2)
by A9, Def4;
hence
S1[
n + 1]
by A4, A8, A10, Th3;
:: thesis: verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
(a + b) |^ s = Sum (a,b In_Power s)
; :: thesis: verum