:: RVSUM_1 semantic presentation
begin
registration
let n be Nat;
cluster Relation-like NAT -defined Function-like natural-valued V60() n -element FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st
( b1 is n -element & b1 is natural-valued )
proof
take n |-> 0 ; ::_thesis: ( n |-> 0 is n -element & n |-> 0 is natural-valued )
thus ( n |-> 0 is n -element & n |-> 0 is natural-valued ) ; ::_thesis: verum
end;
end;
registration
cluster Relation-like NAT -defined Function-like real-valued V60() FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st b1 is real-valued
proof
the FinSequence of REAL is real-valued ;
hence ex b1 being FinSequence st b1 is real-valued ; ::_thesis: verum
end;
end;
definition
let F be real-valued Relation;
:: original: rng
redefine func rng F -> Subset of REAL;
coherence
rng F is Subset of REAL by VALUED_0:def_3;
end;
registration
let D be non empty set ;
let F be Function of REAL,D;
let F1 be real-valued FinSequence;
clusterF1 (#) F -> FinSequence-like ;
coherence
F * F1 is FinSequence-like
proof
consider n1 being Nat such that
A1: dom F1 = Seg n1 by FINSEQ_1:def_2;
take n1 ; :: according to FINSEQ_1:def_2 ::_thesis: dom (F * F1) = Seg n1
( dom F = REAL & rng F1 c= REAL ) by FUNCT_2:def_1;
hence dom (F * F1) = Seg n1 by A1, RELAT_1:27; ::_thesis: verum
end;
end;
registration
let r be real number ;
cluster<*r*> -> real-valued ;
coherence
<*r*> is real-valued
proof
reconsider p = r as Element of REAL by XREAL_0:def_1;
<*p*> is FinSequence-like ;
hence <*r*> is real-valued ; ::_thesis: verum
end;
end;
registration
let r1, r2 be real number ;
cluster<*r1,r2*> -> real-valued ;
coherence
<*r1,r2*> is real-valued
proof
reconsider p1 = r1, p2 = r2 as Element of REAL by XREAL_0:def_1;
<*p1,p2*> is FinSequence-like ;
hence <*r1,r2*> is real-valued ; ::_thesis: verum
end;
end;
registration
let r1, r2, r3 be real number ;
cluster<*r1,r2,r3*> -> real-valued ;
coherence
<*r1,r2,r3*> is real-valued
proof
reconsider p1 = r1, p2 = r2, p3 = r3 as Element of REAL by XREAL_0:def_1;
<*p1,p2,p3*> is FinSequence-like ;
hence <*r1,r2,r3*> is real-valued ; ::_thesis: verum
end;
end;
registration
let r1, r2, r3, r4 be real number ;
cluster<*r1,r2,r3,r4*> -> real-valued ;
coherence
<*r1,r2,r3,r4*> is real-valued
proof
reconsider p1 = r1, p2 = r2, p3 = r3, p4 = r4 as Element of REAL by XREAL_0:def_1;
<*p1,p2,p3,p4*> is FinSequence-like ;
hence <*r1,r2,r3,r4*> is real-valued ; ::_thesis: verum
end;
end;
registration
let j be Nat;
let r be real number ;
clusterj |-> r -> real-valued ;
coherence
j |-> r is real-valued ;
end;
registration
let f, g be real-valued FinSequence;
clusterf ^ g -> real-valued ;
coherence
f ^ g is real-valued
proof
rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
then rng (f ^ g) c= REAL by XBOOLE_1:8;
hence f ^ g is real-valued by VALUED_0:def_3; ::_thesis: verum
end;
end;
theorem :: RVSUM_1:1
0 is_a_unity_wrt addreal by BINOP_2:2, SETWISEO:14;
definition
redefine func diffreal equals :: RVSUM_1:def 1
addreal * ((id REAL),compreal);
compatibility
for b1 being Element of bool [:[:REAL,REAL:],REAL:] holds
( b1 = diffreal iff b1 = addreal * ((id REAL),compreal) )
proof
let b be BinOp of REAL; ::_thesis: ( b = diffreal iff b = addreal * ((id REAL),compreal) )
now__::_thesis:_for_r1,_r2_being_Element_of_REAL_holds_diffreal_._(r1,r2)_=_(addreal_*_((id_REAL),compreal))_._(r1,r2)
let r1, r2 be Element of REAL ; ::_thesis: diffreal . (r1,r2) = (addreal * ((id REAL),compreal)) . (r1,r2)
thus diffreal . (r1,r2) = r1 - r2 by BINOP_2:def_10
.= r1 + (- r2)
.= addreal . (r1,(- r2)) by BINOP_2:def_9
.= addreal . (r1,(compreal . r2)) by BINOP_2:def_7
.= (addreal * ((id REAL),compreal)) . (r1,r2) by FINSEQOP:82 ; ::_thesis: verum
end;
hence ( b = diffreal iff b = addreal * ((id REAL),compreal) ) by BINOP_1:2; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem defines diffreal RVSUM_1:def_1_:_
diffreal = addreal * ((id REAL),compreal);
definition
func sqrreal -> UnOp of REAL means :Def2: :: RVSUM_1:def 2
for r being real number holds it . r = r ^2 ;
existence
ex b1 being UnOp of REAL st
for r being real number holds b1 . r = r ^2
proof
deffunc H1( Element of REAL ) -> Element of REAL = $1 ^2 ;
consider G being Function of REAL,REAL such that
A1: for x being Element of REAL holds G . x = H1(x) from FUNCT_2:sch_4();
take G ; ::_thesis: for r being real number holds G . r = r ^2
let r be real number ; ::_thesis: G . r = r ^2
r in REAL by XREAL_0:def_1;
hence G . r = r ^2 by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being UnOp of REAL st ( for r being real number holds b1 . r = r ^2 ) & ( for r being real number holds b2 . r = r ^2 ) holds
b1 = b2
proof
let G1, G2 be UnOp of REAL; ::_thesis: ( ( for r being real number holds G1 . r = r ^2 ) & ( for r being real number holds G2 . r = r ^2 ) implies G1 = G2 )
assume that
A2: for r being real number holds G1 . r = r ^2 and
A3: for r being real number holds G2 . r = r ^2 ; ::_thesis: G1 = G2
now__::_thesis:_for_x_being_Element_of_REAL_holds_G1_._x_=_G2_._x
let x be Element of REAL ; ::_thesis: G1 . x = G2 . x
G1 . x = x ^2 by A2;
hence G1 . x = G2 . x by A3; ::_thesis: verum
end;
hence G1 = G2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines sqrreal RVSUM_1:def_2_:_
for b1 being UnOp of REAL holds
( b1 = sqrreal iff for r being real number holds b1 . r = r ^2 );
theorem :: RVSUM_1:2
1 is_a_unity_wrt multreal by BINOP_2:7, SETWISEO:14;
theorem Th3: :: RVSUM_1:3
multreal is_distributive_wrt addreal
proof
now__::_thesis:_for_x1,_x2,_x3_being_Element_of_REAL_holds_
(_multreal_._(x1,(addreal_._(x2,x3)))_=_addreal_._((multreal_._(x1,x2)),(multreal_._(x1,x3)))_&_multreal_._((addreal_._(x1,x2)),x3)_=_addreal_._((multreal_._(x1,x3)),(multreal_._(x2,x3)))_)
let x1, x2, x3 be Element of REAL ; ::_thesis: ( multreal . (x1,(addreal . (x2,x3))) = addreal . ((multreal . (x1,x2)),(multreal . (x1,x3))) & multreal . ((addreal . (x1,x2)),x3) = addreal . ((multreal . (x1,x3)),(multreal . (x2,x3))) )
thus multreal . (x1,(addreal . (x2,x3))) = multreal . (x1,(x2 + x3)) by BINOP_2:def_9
.= x1 * (x2 + x3) by BINOP_2:def_11
.= (x1 * x2) + (x1 * x3)
.= addreal . ((x1 * x2),(x1 * x3)) by BINOP_2:def_9
.= addreal . ((multreal . (x1,x2)),(x1 * x3)) by BINOP_2:def_11
.= addreal . ((multreal . (x1,x2)),(multreal . (x1,x3))) by BINOP_2:def_11 ; ::_thesis: multreal . ((addreal . (x1,x2)),x3) = addreal . ((multreal . (x1,x3)),(multreal . (x2,x3)))
thus multreal . ((addreal . (x1,x2)),x3) = multreal . ((x1 + x2),x3) by BINOP_2:def_9
.= (x1 + x2) * x3 by BINOP_2:def_11
.= (x1 * x3) + (x2 * x3)
.= addreal . ((x1 * x3),(x2 * x3)) by BINOP_2:def_9
.= addreal . ((multreal . (x1,x3)),(x2 * x3)) by BINOP_2:def_11
.= addreal . ((multreal . (x1,x3)),(multreal . (x2,x3))) by BINOP_2:def_11 ; ::_thesis: verum
end;
hence multreal is_distributive_wrt addreal by BINOP_1:11; ::_thesis: verum
end;
theorem :: RVSUM_1:4
sqrreal is_distributive_wrt multreal
proof
let x1 be Element of REAL ; :: according to BINOP_1:def_20 ::_thesis: for b1 being Element of REAL holds sqrreal . (multreal . (x1,b1)) = multreal . ((sqrreal . x1),(sqrreal . b1))
let x2 be Element of REAL ; ::_thesis: sqrreal . (multreal . (x1,x2)) = multreal . ((sqrreal . x1),(sqrreal . x2))
thus sqrreal . (multreal . (x1,x2)) = sqrreal . (x1 * x2) by BINOP_2:def_11
.= (x1 * x2) ^2 by Def2
.= (x1 ^2) * (x2 ^2)
.= multreal . ((x1 ^2),(x2 ^2)) by BINOP_2:def_11
.= multreal . ((sqrreal . x1),(x2 ^2)) by Def2
.= multreal . ((sqrreal . x1),(sqrreal . x2)) by Def2 ; ::_thesis: verum
end;
definition
let x be real number ;
funcx multreal -> UnOp of REAL equals :: RVSUM_1:def 3
multreal [;] (x,(id REAL));
coherence
multreal [;] (x,(id REAL)) is UnOp of REAL
proof
reconsider y = x as Real by XREAL_0:def_1;
multreal [;] (y,(id REAL)) is UnOp of REAL ;
hence multreal [;] (x,(id REAL)) is UnOp of REAL ; ::_thesis: verum
end;
end;
:: deftheorem defines multreal RVSUM_1:def_3_:_
for x being real number holds x multreal = multreal [;] (x,(id REAL));
Lm1: for r, r1 being real number holds (multreal [;] (r,(id REAL))) . r1 = r * r1
proof
let r, r1 be real number ; ::_thesis: (multreal [;] (r,(id REAL))) . r1 = r * r1
reconsider a = r, s = r1 as Element of REAL by XREAL_0:def_1;
thus (multreal [;] (r,(id REAL))) . r1 = multreal . (a,((id REAL) . s)) by FUNCOP_1:53
.= multreal . (a,s) by FUNCT_1:18
.= r * r1 by BINOP_2:def_11 ; ::_thesis: verum
end;
theorem :: RVSUM_1:5
for r, r1 being real number holds (r multreal) . r1 = r * r1 by Lm1;
theorem :: RVSUM_1:6
for r being real number holds r multreal is_distributive_wrt addreal
proof
let r be real number ; ::_thesis: r multreal is_distributive_wrt addreal
r in REAL by XREAL_0:def_1;
hence r multreal is_distributive_wrt addreal by Th3, FINSEQOP:54; ::_thesis: verum
end;
theorem Th7: :: RVSUM_1:7
compreal is_an_inverseOp_wrt addreal
proof
let x be Element of REAL ; :: according to FINSEQOP:def_1 ::_thesis: ( addreal . (x,(compreal . x)) = the_unity_wrt addreal & addreal . ((compreal . x),x) = the_unity_wrt addreal )
thus addreal . (x,(compreal . x)) = x + (compreal . x) by BINOP_2:def_9
.= x + (- x) by BINOP_2:def_7
.= the_unity_wrt addreal by BINOP_2:2 ; ::_thesis: addreal . ((compreal . x),x) = the_unity_wrt addreal
thus addreal . ((compreal . x),x) = (compreal . x) + x by BINOP_2:def_9
.= (- x) + x by BINOP_2:def_7
.= the_unity_wrt addreal by BINOP_2:2 ; ::_thesis: verum
end;
theorem Th8: :: RVSUM_1:8
addreal is having_an_inverseOp by Th7, FINSEQOP:def_2;
theorem Th9: :: RVSUM_1:9
the_inverseOp_wrt addreal = compreal by Th7, Th8, FINSEQOP:def_3;
theorem :: RVSUM_1:10
compreal is_distributive_wrt addreal by Th8, Th9, FINSEQOP:63;
Lm2: for F being real-valued FinSequence holds F is FinSequence of REAL
proof
let F be real-valued FinSequence; ::_thesis: F is FinSequence of REAL
thus rng F c= REAL ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
definition
let F1, F2 be real-valued FinSequence;
:: original: +
redefine funcF1 + F2 -> FinSequence of REAL equals :: RVSUM_1:def 4
addreal .: (F1,F2);
coherence
F1 + F2 is FinSequence of REAL by Lm2;
compatibility
for b1 being FinSequence of REAL holds
( b1 = F1 + F2 iff b1 = addreal .: (F1,F2) )
proof
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL ; ::_thesis: ( F = F1 + F2 iff F = addreal .: (F1,F2) )
dom addreal = [:REAL,REAL:] by FUNCT_2:def_1;
then [:(rng F3),(rng F4):] c= dom addreal by ZFMISC_1:96;
then A1: dom (addreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;
A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def_1;
thus ( F = F1 + F2 implies F = addreal .: (F1,F2) ) ::_thesis: ( F = addreal .: (F1,F2) implies F = F1 + F2 )
proof
assume A3: F = F1 + F2 ; ::_thesis: F = addreal .: (F1,F2)
for z being set st z in dom (addreal .: (F1,F2)) holds
F . z = addreal . ((F1 . z),(F2 . z))
proof
let z be set ; ::_thesis: ( z in dom (addreal .: (F1,F2)) implies F . z = addreal . ((F1 . z),(F2 . z)) )
assume z in dom (addreal .: (F1,F2)) ; ::_thesis: F . z = addreal . ((F1 . z),(F2 . z))
hence F . z = (F1 . z) + (F2 . z) by A2, A1, A3, VALUED_1:def_1
.= addreal . ((F1 . z),(F2 . z)) by BINOP_2:def_9 ;
::_thesis: verum
end;
hence F = addreal .: (F1,F2) by A2, A1, A3, FUNCOP_1:21; ::_thesis: verum
end;
assume A4: F = addreal .: (F1,F2) ; ::_thesis: F = F1 + F2
now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_
F_._c_=_(F1_._c)_+_(F2_._c)
let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) + (F2 . c) )
assume c in dom F ; ::_thesis: F . c = (F1 . c) + (F2 . c)
hence F . c = addreal . ((F1 . c),(F2 . c)) by A4, FUNCOP_1:22
.= (F1 . c) + (F2 . c) by BINOP_2:def_9 ;
::_thesis: verum
end;
hence F = F1 + F2 by A1, A4, VALUED_1:def_1; ::_thesis: verum
end;
commutativity
for b1 being FinSequence of REAL
for F1, F2 being real-valued FinSequence st b1 = addreal .: (F1,F2) holds
b1 = addreal .: (F2,F1)
proof
let F be FinSequence of REAL ; ::_thesis: for F1, F2 being real-valued FinSequence st F = addreal .: (F1,F2) holds
F = addreal .: (F2,F1)
let F1, F2 be real-valued FinSequence; ::_thesis: ( F = addreal .: (F1,F2) implies F = addreal .: (F2,F1) )
assume A5: F = addreal .: (F1,F2) ; ::_thesis: F = addreal .: (F2,F1)
reconsider F1 = F1, F2 = F2 as FinSequence of REAL by Lm2;
A6: dom addreal = [:REAL,REAL:] by FUNCT_2:def_1;
then A7: [:(rng F2),(rng F1):] c= dom addreal by ZFMISC_1:96;
[:(rng F1),(rng F2):] c= dom addreal by A6, ZFMISC_1:96;
then A8: dom (addreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69
.= dom (addreal .: (F2,F1)) by A7, FUNCOP_1:69 ;
for z being set st z in dom (addreal .: (F2,F1)) holds
F . z = addreal . ((F2 . z),(F1 . z))
proof
let z be set ; ::_thesis: ( z in dom (addreal .: (F2,F1)) implies F . z = addreal . ((F2 . z),(F1 . z)) )
assume z in dom (addreal .: (F2,F1)) ; ::_thesis: F . z = addreal . ((F2 . z),(F1 . z))
hence F . z = addreal . ((F1 . z),(F2 . z)) by A5, A8, FUNCOP_1:22
.= (F1 . z) + (F2 . z) by BINOP_2:def_9
.= addreal . ((F2 . z),(F1 . z)) by BINOP_2:def_9 ;
::_thesis: verum
end;
hence F = addreal .: (F2,F1) by A5, A8, FUNCOP_1:21; ::_thesis: verum
end;
end;
:: deftheorem defines + RVSUM_1:def_4_:_
for F1, F2 being real-valued FinSequence holds F1 + F2 = addreal .: (F1,F2);
definition
let i be Nat;
let R1, R2 be Element of i -tuples_on REAL;
:: original: +
redefine funcR1 + R2 -> Element of i -tuples_on REAL;
coherence
R1 + R2 is Element of i -tuples_on REAL by FINSEQ_2:120;
end;
theorem :: RVSUM_1:11
for s being set
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s)
proof
let s be set ; ::_thesis: for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s)
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s)
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)
percases ( not s in Seg i or s in Seg i ) ;
supposeA1: not s in Seg i ; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)
then A2: not s in dom R2 by FINSEQ_2:124;
A3: not s in dom R1 by A1, FINSEQ_2:124;
not s in dom (R1 + R2) by A1, FINSEQ_2:124;
hence (R1 + R2) . s = 0 + 0 by FUNCT_1:def_2
.= (R1 . s) + 0 by A3, FUNCT_1:def_2
.= (R1 . s) + (R2 . s) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
suppose s in Seg i ; ::_thesis: (R1 + R2) . s = (R1 . s) + (R2 . s)
then s in dom (R1 + R2) by FINSEQ_2:124;
hence (R1 + R2) . s = (R1 . s) + (R2 . s) by VALUED_1:def_1; ::_thesis: verum
end;
end;
end;
theorem :: RVSUM_1:12
for F being real-valued FinSequence holds (<*> REAL) + F = <*> REAL
proof
let F be real-valued FinSequence; ::_thesis: (<*> REAL) + F = <*> REAL
F is FinSequence of REAL by Lm2;
hence (<*> REAL) + F = <*> REAL by FINSEQ_2:73; ::_thesis: verum
end;
theorem :: RVSUM_1:13
for r1, r2 being real number holds <*r1*> + <*r2*> = <*(r1 + r2)*>
proof
let r1, r2 be real number ; ::_thesis: <*r1*> + <*r2*> = <*(r1 + r2)*>
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
<*s1*> + <*s2*> = <*(addreal . (s1,s2))*> by FINSEQ_2:74
.= <*(r1 + r2)*> by BINOP_2:def_9 ;
hence <*r1*> + <*r2*> = <*(r1 + r2)*> ; ::_thesis: verum
end;
theorem :: RVSUM_1:14
for i being Nat
for r1, r2 being real number holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)
proof
let i be Nat; ::_thesis: for r1, r2 being real number holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)
let r1, r2 be real number ; ::_thesis: (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
(i |-> s1) + (i |-> s2) = i |-> (addreal . (s1,s2)) by FINSEQOP:17
.= i |-> (r1 + r2) by BINOP_2:def_9 ;
hence (i |-> r1) + (i |-> r2) = i |-> (r1 + r2) ; ::_thesis: verum
end;
theorem :: RVSUM_1:15
for F1, F2, F3 being real-valued FinSequence holds F1 + (F2 + F3) = (F1 + F2) + F3 by RFUNCT_1:8;
theorem :: RVSUM_1:16
for i being Nat
for R being Element of i -tuples_on REAL holds R + (i |-> 0) = R by BINOP_2:2, FINSEQOP:56;
theorem :: RVSUM_1:17
for s being set
for F being real-valued FinSequence holds (- F) . s = - (F . s) by VALUED_1:8;
definition
let F be real-valued FinSequence;
:: original: -
redefine func - F -> FinSequence of REAL equals :: RVSUM_1:def 5
compreal * F;
coherence
- F is FinSequence of REAL by Lm2;
compatibility
for b1 being FinSequence of REAL holds
( b1 = - F iff b1 = compreal * F )
proof
let F1 be FinSequence of REAL ; ::_thesis: ( F1 = - F iff F1 = compreal * F )
A1: dom (- F) = dom F by VALUED_1:8;
A2: ( rng F c= REAL & dom compreal = REAL ) by FUNCT_2:def_1;
then A3: dom (compreal * F) = dom F by RELAT_1:27;
thus ( F1 = - F implies F1 = compreal * F ) ::_thesis: ( F1 = compreal * F implies F1 = - F )
proof
assume A4: F1 = - F ; ::_thesis: F1 = compreal * F
now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_
F1_._c_=_(compreal_*_F)_._c
let c be set ; ::_thesis: ( c in dom F1 implies F1 . c = (compreal * F) . c )
assume A5: c in dom F1 ; ::_thesis: F1 . c = (compreal * F) . c
thus F1 . c = - (F . c) by A4, VALUED_1:8
.= compreal . (F . c) by BINOP_2:def_7
.= (compreal * F) . c by A1, A4, A5, FUNCT_1:13 ; ::_thesis: verum
end;
hence F1 = compreal * F by A3, A4, FUNCT_1:2, VALUED_1:8; ::_thesis: verum
end;
assume A6: F1 = compreal * F ; ::_thesis: F1 = - F
now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_
(-_F)_._c_=_(compreal_*_F)_._c
let c be set ; ::_thesis: ( c in dom F1 implies (- F) . c = (compreal * F) . c )
assume A7: c in dom F1 ; ::_thesis: (- F) . c = (compreal * F) . c
thus (- F) . c = - (F . c) by VALUED_1:8
.= compreal . (F . c) by BINOP_2:def_7
.= (compreal * F) . c by A6, A7, FUNCT_1:12 ; ::_thesis: verum
end;
hence F1 = - F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; ::_thesis: verum
end;
end;
:: deftheorem defines - RVSUM_1:def_5_:_
for F being real-valued FinSequence holds - F = compreal * F;
definition
let i be Nat;
let R be Element of i -tuples_on REAL;
:: original: -
redefine func - R -> Element of i -tuples_on REAL;
coherence
- R is Element of i -tuples_on REAL by FINSEQ_2:113;
end;
theorem :: RVSUM_1:18
for s being set
for F being real-valued FinSequence holds (- F) . s = - (F . s) by VALUED_1:8;
theorem :: RVSUM_1:19
- (<*> REAL) = <*> REAL ;
theorem :: RVSUM_1:20
for r being real number holds - <*r*> = <*(- r)*>
proof
let r be real number ; ::_thesis: - <*r*> = <*(- r)*>
reconsider s = r as Element of REAL by XREAL_0:def_1;
- <*s*> = <*(compreal . s)*> by FINSEQ_2:35
.= <*(- r)*> by BINOP_2:def_7 ;
hence - <*r*> = <*(- r)*> ; ::_thesis: verum
end;
theorem Th21: :: RVSUM_1:21
for i being Nat
for r being real number holds - (i |-> r) = i |-> (- r)
proof
let i be Nat; ::_thesis: for r being real number holds - (i |-> r) = i |-> (- r)
let r be real number ; ::_thesis: - (i |-> r) = i |-> (- r)
reconsider s = r as Element of REAL by XREAL_0:def_1;
- (i |-> s) = i |-> (compreal . s) by FINSEQOP:16
.= i |-> (- r) by BINOP_2:def_7 ;
hence - (i |-> r) = i |-> (- r) ; ::_thesis: verum
end;
theorem :: RVSUM_1:22
for i being Nat
for R being Element of i -tuples_on REAL holds R + (- R) = i |-> 0 by Th8, Th9, BINOP_2:2, FINSEQOP:73;
theorem :: RVSUM_1:23
for i being Nat
for R1, R2 being Element of i -tuples_on REAL st R1 + R2 = i |-> 0 holds
R1 = - R2 by Th8, Th9, BINOP_2:2, FINSEQOP:74;
theorem :: RVSUM_1:24
for R1, R2 being complex-valued Function st - R1 = - R2 holds
R1 = R2
proof
let R1, R2 be complex-valued Function; ::_thesis: ( - R1 = - R2 implies R1 = R2 )
assume - R1 = - R2 ; ::_thesis: R1 = R2
hence R1 = - (- R2)
.= R2 ;
::_thesis: verum
end;
theorem :: RVSUM_1:25
for i being Nat
for R1, R, R2 being Element of i -tuples_on REAL st R1 + R = R2 + R holds
R1 = R2
proof
let i be Nat; ::_thesis: for R1, R, R2 being Element of i -tuples_on REAL st R1 + R = R2 + R holds
R1 = R2
let R1, R, R2 be Element of i -tuples_on REAL; ::_thesis: ( R1 + R = R2 + R implies R1 = R2 )
assume R1 + R = R2 + R ; ::_thesis: R1 = R2
then R1 + (R + (- R)) = (R2 + R) + (- R) by FINSEQOP:28;
then A1: R1 + (R + (- R)) = R2 + (R + (- R)) by FINSEQOP:28;
R + (- R) = i |-> 0 by Th8, Th9, BINOP_2:2, FINSEQOP:73;
then R1 = R2 + (i |-> 0) by A1, BINOP_2:2, FINSEQOP:56;
hence R1 = R2 by BINOP_2:2, FINSEQOP:56; ::_thesis: verum
end;
theorem Th26: :: RVSUM_1:26
for F1, F2 being real-valued FinSequence holds - (F1 + F2) = (- F1) + (- F2)
proof
let F1, F2 be real-valued FinSequence; ::_thesis: - (F1 + F2) = (- F1) + (- F2)
A1: dom (- (F1 + F2)) = dom (F1 + F2) by VALUED_1:8;
A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def_1;
A3: dom ((- F1) + (- F2)) = (dom (- F1)) /\ (dom (- F2)) by VALUED_1:def_1
.= (dom F1) /\ (dom (- F2)) by VALUED_1:8
.= (dom F1) /\ (dom F2) by VALUED_1:8 ;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(-_(F1_+_F2))_holds_
(-_(F1_+_F2))_._i_=_((-_F1)_+_(-_F2))_._i
let i be Nat; ::_thesis: ( i in dom (- (F1 + F2)) implies (- (F1 + F2)) . i = ((- F1) + (- F2)) . i )
assume A4: i in dom (- (F1 + F2)) ; ::_thesis: (- (F1 + F2)) . i = ((- F1) + (- F2)) . i
thus (- (F1 + F2)) . i = - ((F1 + F2) . i) by VALUED_1:8
.= - ((F1 . i) + (F2 . i)) by A1, A4, VALUED_1:def_1
.= (- (F1 . i)) + (- (F2 . i))
.= (- (F1 . i)) + ((- F2) . i) by VALUED_1:8
.= ((- F1) . i) + ((- F2) . i) by VALUED_1:8
.= ((- F1) + (- F2)) . i by A1, A2, A3, A4, VALUED_1:def_1 ; ::_thesis: verum
end;
hence - (F1 + F2) = (- F1) + (- F2) by A2, A3, FINSEQ_1:13, VALUED_1:8; ::_thesis: verum
end;
definition
let F1, F2 be real-valued FinSequence;
:: original: -
redefine funcF1 - F2 -> FinSequence of REAL equals :: RVSUM_1:def 6
diffreal .: (F1,F2);
coherence
F1 - F2 is FinSequence of REAL by Lm2;
compatibility
for b1 being FinSequence of REAL holds
( b1 = F1 - F2 iff b1 = diffreal .: (F1,F2) )
proof
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL ; ::_thesis: ( F = F1 - F2 iff F = diffreal .: (F1,F2) )
A1: dom (F1 - F2) = (dom F1) /\ (dom F2) by VALUED_1:12;
dom diffreal = [:REAL,REAL:] by FUNCT_2:def_1;
then A2: [:(rng F3),(rng F4):] c= dom diffreal by ZFMISC_1:96;
then A3: dom (diffreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;
thus ( F = F1 - F2 implies F = diffreal .: (F1,F2) ) ::_thesis: ( F = diffreal .: (F1,F2) implies F = F1 - F2 )
proof
assume A4: F = F1 - F2 ; ::_thesis: F = diffreal .: (F1,F2)
for z being set st z in dom (diffreal .: (F1,F2)) holds
F . z = diffreal . ((F1 . z),(F2 . z))
proof
let z be set ; ::_thesis: ( z in dom (diffreal .: (F1,F2)) implies F . z = diffreal . ((F1 . z),(F2 . z)) )
assume z in dom (diffreal .: (F1,F2)) ; ::_thesis: F . z = diffreal . ((F1 . z),(F2 . z))
hence F . z = (F1 . z) - (F2 . z) by A1, A3, A4, VALUED_1:13
.= diffreal . ((F1 . z),(F2 . z)) by BINOP_2:def_10 ;
::_thesis: verum
end;
hence F = diffreal .: (F1,F2) by A1, A3, A4, FUNCOP_1:21; ::_thesis: verum
end;
assume A5: F = diffreal .: (F1,F2) ; ::_thesis: F = F1 - F2
now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_
F_._c_=_(F1_._c)_-_(F2_._c)
let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) - (F2 . c) )
assume c in dom F ; ::_thesis: F . c = (F1 . c) - (F2 . c)
hence F . c = diffreal . ((F1 . c),(F2 . c)) by A5, FUNCOP_1:22
.= (F1 . c) - (F2 . c) by BINOP_2:def_10 ;
::_thesis: verum
end;
hence F = F1 - F2 by A1, A2, A5, FUNCOP_1:69, VALUED_1:14; ::_thesis: verum
end;
end;
:: deftheorem defines - RVSUM_1:def_6_:_
for F1, F2 being real-valued FinSequence holds F1 - F2 = diffreal .: (F1,F2);
definition
let i be Nat;
let R1, R2 be Element of i -tuples_on REAL;
:: original: -
redefine funcR1 - R2 -> Element of i -tuples_on REAL;
coherence
R1 - R2 is Element of i -tuples_on REAL by FINSEQ_2:120;
end;
theorem :: RVSUM_1:27
for s being set
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)
proof
let s be set ; ::_thesis: for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s)
percases ( not s in Seg i or s in Seg i ) ;
supposeA1: not s in Seg i ; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s)
then A2: not s in dom R2 by FINSEQ_2:124;
A3: not s in dom R1 by A1, FINSEQ_2:124;
not s in dom (R1 - R2) by A1, FINSEQ_2:124;
hence (R1 - R2) . s = 0 - 0 by FUNCT_1:def_2
.= (R1 . s) - 0 by A3, FUNCT_1:def_2
.= (R1 . s) - (R2 . s) by A2, FUNCT_1:def_2 ;
::_thesis: verum
end;
suppose s in Seg i ; ::_thesis: (R1 - R2) . s = (R1 . s) - (R2 . s)
then s in dom (R1 - R2) by FINSEQ_2:124;
hence (R1 - R2) . s = (R1 . s) - (R2 . s) by VALUED_1:13; ::_thesis: verum
end;
end;
end;
theorem :: RVSUM_1:28
for F being real-valued FinSequence holds
( (<*> REAL) - F = <*> REAL & F - (<*> REAL) = <*> REAL )
proof
let F be real-valued FinSequence; ::_thesis: ( (<*> REAL) - F = <*> REAL & F - (<*> REAL) = <*> REAL )
F is FinSequence of REAL by Lm2;
hence ( (<*> REAL) - F = <*> REAL & F - (<*> REAL) = <*> REAL ) by FINSEQ_2:73; ::_thesis: verum
end;
theorem :: RVSUM_1:29
for r1, r2 being real number holds <*r1*> - <*r2*> = <*(r1 - r2)*>
proof
let r1, r2 be real number ; ::_thesis: <*r1*> - <*r2*> = <*(r1 - r2)*>
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
<*s1*> - <*s2*> = <*(diffreal . (s1,s2))*> by FINSEQ_2:74
.= <*(r1 - r2)*> by BINOP_2:def_10 ;
hence <*r1*> - <*r2*> = <*(r1 - r2)*> ; ::_thesis: verum
end;
theorem :: RVSUM_1:30
for i being Nat
for r1, r2 being real number holds (i |-> r1) - (i |-> r2) = i |-> (r1 - r2)
proof
let i be Nat; ::_thesis: for r1, r2 being real number holds (i |-> r1) - (i |-> r2) = i |-> (r1 - r2)
let r1, r2 be real number ; ::_thesis: (i |-> r1) - (i |-> r2) = i |-> (r1 - r2)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
(i |-> s1) - (i |-> s2) = i |-> (diffreal . (s1,s2)) by FINSEQOP:17
.= i |-> (r1 - r2) by BINOP_2:def_10 ;
hence (i |-> r1) - (i |-> r2) = i |-> (r1 - r2) ; ::_thesis: verum
end;
theorem :: RVSUM_1:31
for F1, F2 being real-valued FinSequence holds F1 - F2 = F1 + (- F2) ;
theorem :: RVSUM_1:32
for i being Nat
for R being Element of i -tuples_on REAL holds R - (i |-> 0) = R
proof
let i be Nat; ::_thesis: for R being Element of i -tuples_on REAL holds R - (i |-> 0) = R
let R be Element of i -tuples_on REAL; ::_thesis: R - (i |-> 0) = R
thus R - (i |-> 0) = R + (i |-> (- 0)) by Th21
.= R by BINOP_2:2, FINSEQOP:56 ; ::_thesis: verum
end;
theorem :: RVSUM_1:33
for i being Nat
for R being Element of i -tuples_on REAL holds (i |-> 0) - R = - R by BINOP_2:2, FINSEQOP:56;
theorem :: RVSUM_1:34
for F1, F2 being real-valued FinSequence holds F1 - (- F2) = F1 + F2 ;
theorem :: RVSUM_1:35
for F1, F2 being real-valued FinSequence holds - (F1 - F2) = F2 - F1
proof
let F1, F2 be real-valued FinSequence; ::_thesis: - (F1 - F2) = F2 - F1
thus - (F1 - F2) = (- F1) + (- (- F2)) by Th26
.= F2 - F1 ; ::_thesis: verum
end;
theorem :: RVSUM_1:36
for F1, F2 being real-valued FinSequence holds - (F1 - F2) = (- F1) + F2
proof
let F1, F2 be real-valued FinSequence; ::_thesis: - (F1 - F2) = (- F1) + F2
thus - (F1 - F2) = (- F1) + (- (- F2)) by Th26
.= (- F1) + F2 ; ::_thesis: verum
end;
theorem :: RVSUM_1:37
for i being Nat
for R being Element of i -tuples_on REAL holds R - R = i |-> 0 by Th8, Th9, BINOP_2:2, FINSEQOP:73;
theorem :: RVSUM_1:38
for i being Nat
for R1, R2 being Element of i -tuples_on REAL st R1 - R2 = i |-> 0 holds
R1 = R2
proof
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL st R1 - R2 = i |-> 0 holds
R1 = R2
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: ( R1 - R2 = i |-> 0 implies R1 = R2 )
assume R1 - R2 = i |-> 0 ; ::_thesis: R1 = R2
then R1 = - (- R2) by Th8, Th9, BINOP_2:2, FINSEQOP:74;
hence R1 = R2 ; ::_thesis: verum
end;
theorem :: RVSUM_1:39
for F1, F2, F3 being real-valued FinSequence holds (F1 - F2) - F3 = F1 - (F2 + F3) by RFUNCT_1:20;
theorem :: RVSUM_1:40
for F1, F2, F3 being real-valued FinSequence holds F1 + (F2 - F3) = (F1 + F2) - F3 by RFUNCT_1:23;
theorem :: RVSUM_1:41
for F1, F2, F3 being real-valued FinSequence holds F1 - (F2 - F3) = (F1 - F2) + F3 by RFUNCT_1:22;
theorem :: RVSUM_1:42
for i being Nat
for R1, R being Element of i -tuples_on REAL holds R1 = (R1 + R) - R
proof
let i be Nat; ::_thesis: for R1, R being Element of i -tuples_on REAL holds R1 = (R1 + R) - R
let R1, R be Element of i -tuples_on REAL; ::_thesis: R1 = (R1 + R) - R
thus R1 = R1 + (i |-> 0) by BINOP_2:2, FINSEQOP:56
.= R1 + (R - R) by Th8, Th9, BINOP_2:2, FINSEQOP:73
.= (R1 + R) - R by RFUNCT_1:23 ; ::_thesis: verum
end;
theorem :: RVSUM_1:43
for i being Nat
for R1, R being Element of i -tuples_on REAL holds R1 = (R1 - R) + R
proof
let i be Nat; ::_thesis: for R1, R being Element of i -tuples_on REAL holds R1 = (R1 - R) + R
let R1, R be Element of i -tuples_on REAL; ::_thesis: R1 = (R1 - R) + R
thus R1 = R1 + (i |-> 0) by BINOP_2:2, FINSEQOP:56
.= R1 + ((- R) + R) by Th8, Th9, BINOP_2:2, FINSEQOP:73
.= (R1 - R) + R by FINSEQOP:28 ; ::_thesis: verum
end;
notation
let F be real-valued FinSequence;
let r be real number ;
synonym r * F for r (#) F;
end;
theorem :: RVSUM_1:44
for s being set
for r being real number
for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;
definition
let F be real-valued FinSequence;
let r be real number ;
:: original: *
redefine funcr * F -> FinSequence of REAL equals :: RVSUM_1:def 7
(r multreal) * F;
coherence
r * F is FinSequence of REAL by Lm2;
compatibility
for b1 being FinSequence of REAL holds
( b1 = r * F iff b1 = (r multreal) * F )
proof
let F1 be FinSequence of REAL ; ::_thesis: ( F1 = r * F iff F1 = (r multreal) * F )
A1: dom (r * F) = dom F by VALUED_1:def_5;
A2: ( rng F c= REAL & dom (r multreal) = REAL ) by FUNCT_2:def_1;
then A3: dom ((r multreal) * F) = dom F by RELAT_1:27;
thus ( F1 = r * F implies F1 = (r multreal) * F ) ::_thesis: ( F1 = (r multreal) * F implies F1 = r * F )
proof
assume A4: F1 = r * F ; ::_thesis: F1 = (r multreal) * F
now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_
F1_._c_=_((r_multreal)_*_F)_._c
let c be set ; ::_thesis: ( c in dom F1 implies F1 . c = ((r multreal) * F) . c )
assume A5: c in dom F1 ; ::_thesis: F1 . c = ((r multreal) * F) . c
hence F1 . c = r * (F . c) by A4, VALUED_1:def_5
.= (r multreal) . (F . c) by Lm1
.= ((r multreal) * F) . c by A1, A4, A5, FUNCT_1:13 ;
::_thesis: verum
end;
hence F1 = (r multreal) * F by A1, A3, A4, FUNCT_1:2; ::_thesis: verum
end;
assume A6: F1 = (r multreal) * F ; ::_thesis: F1 = r * F
now__::_thesis:_for_c_being_set_st_c_in_dom_F1_holds_
(r_*_F)_._c_=_((r_multreal)_*_F)_._c
let c be set ; ::_thesis: ( c in dom F1 implies (r * F) . c = ((r multreal) * F) . c )
assume A7: c in dom F1 ; ::_thesis: (r * F) . c = ((r multreal) * F) . c
thus (r * F) . c = r * (F . c) by VALUED_1:6
.= (r multreal) . (F . c) by Lm1
.= ((r multreal) * F) . c by A6, A7, FUNCT_1:12 ; ::_thesis: verum
end;
hence F1 = r * F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; ::_thesis: verum
end;
end;
:: deftheorem defines * RVSUM_1:def_7_:_
for F being real-valued FinSequence
for r being real number holds r * F = (r multreal) * F;
definition
let i be Nat;
let R be Element of i -tuples_on REAL;
let r be real number ;
:: original: *
redefine funcr * R -> Element of i -tuples_on REAL;
coherence
r * R is Element of i -tuples_on REAL by FINSEQ_2:113;
end;
theorem :: RVSUM_1:45
for s being set
for r being real number
for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;
theorem :: RVSUM_1:46
for r being real number holds r * (<*> REAL) = <*> REAL ;
theorem :: RVSUM_1:47
for r, r1 being real number holds r * <*r1*> = <*(r * r1)*>
proof
let r, r1 be real number ; ::_thesis: r * <*r1*> = <*(r * r1)*>
reconsider s = r, s1 = r1 as Element of REAL by XREAL_0:def_1;
s * <*s1*> = <*((multreal [;] (s,(id REAL))) . s1)*> by FINSEQ_2:35
.= <*(r * r1)*> by Lm1 ;
hence r * <*r1*> = <*(r * r1)*> ; ::_thesis: verum
end;
theorem Th48: :: RVSUM_1:48
for i being Nat
for r1, r2 being real number holds r1 * (i |-> r2) = i |-> (r1 * r2)
proof
let i be Nat; ::_thesis: for r1, r2 being real number holds r1 * (i |-> r2) = i |-> (r1 * r2)
let r1, r2 be real number ; ::_thesis: r1 * (i |-> r2) = i |-> (r1 * r2)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
s1 * (i |-> s2) = i |-> ((multreal [;] (s1,(id REAL))) . s2) by FINSEQOP:16
.= i |-> (r1 * r2) by Lm1 ;
hence r1 * (i |-> r2) = i |-> (r1 * r2) ; ::_thesis: verum
end;
theorem :: RVSUM_1:49
for r1, r2 being real number
for F being real-valued FinSequence holds (r1 * r2) * F = r1 * (r2 * F) by RFUNCT_1:17;
theorem :: RVSUM_1:50
for r1, r2 being real number
for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F)
proof
let r1, r2 be real number ; ::_thesis: for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F)
let F be real-valued FinSequence; ::_thesis: (r1 + r2) * F = (r1 * F) + (r2 * F)
A1: dom ((r1 + r2) * F) = dom F by VALUED_1:def_5;
A2: dom ((r1 * F) + (r2 * F)) = (dom (r1 * F)) /\ (dom (r2 * F)) by VALUED_1:def_1;
A3: dom (r1 * F) = dom F by VALUED_1:def_5;
A4: dom (r2 * F) = dom F by VALUED_1:def_5;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_((r1_+_r2)_*_F)_holds_
((r1_+_r2)_*_F)_._i_=_((r1_*_F)_+_(r2_*_F))_._i
let i be Nat; ::_thesis: ( i in dom ((r1 + r2) * F) implies ((r1 + r2) * F) . i = ((r1 * F) + (r2 * F)) . i )
assume A5: i in dom ((r1 + r2) * F) ; ::_thesis: ((r1 + r2) * F) . i = ((r1 * F) + (r2 * F)) . i
thus ((r1 + r2) * F) . i = (r1 + r2) * (F . i) by VALUED_1:6
.= (r1 * (F . i)) + (r2 * (F . i))
.= (r1 * (F . i)) + ((r2 * F) . i) by VALUED_1:6
.= ((r1 * F) . i) + ((r2 * F) . i) by VALUED_1:6
.= ((r1 * F) + (r2 * F)) . i by A1, A2, A3, A4, A5, VALUED_1:def_1 ; ::_thesis: verum
end;
hence (r1 + r2) * F = (r1 * F) + (r2 * F) by A1, A2, A3, A4, FINSEQ_1:13; ::_thesis: verum
end;
theorem :: RVSUM_1:51
for r being real number
for F1, F2 being real-valued FinSequence holds r * (F1 + F2) = (r * F1) + (r * F2) by RFUNCT_1:16;
theorem :: RVSUM_1:52
for F being real-valued FinSequence holds 1 * F = F by RFUNCT_1:21;
theorem :: RVSUM_1:53
for i being Nat
for R being Element of i -tuples_on REAL holds 0 * R = i |-> 0
proof
let i be Nat; ::_thesis: for R being Element of i -tuples_on REAL holds 0 * R = i |-> 0
let R be Element of i -tuples_on REAL; ::_thesis: 0 * R = i |-> 0
A1: rng R c= REAL ;
thus 0 * R = multreal [;] (0,((id REAL) * R)) by FUNCOP_1:34
.= multreal [;] (0,R) by A1, RELAT_1:53
.= i |-> 0 by Th3, Th8, BINOP_2:2, FINSEQOP:76 ; ::_thesis: verum
end;
theorem :: RVSUM_1:54
for F being real-valued FinSequence holds (- 1) * F = - F ;
notation
let F be real-valued FinSequence;
synonym sqr F for F ^2 ;
end;
definition
let F be real-valued FinSequence;
:: original: sqr
redefine func sqr F -> FinSequence of REAL equals :: RVSUM_1:def 8
sqrreal * F;
compatibility
for b1 being FinSequence of REAL holds
( b1 = sqr F iff b1 = sqrreal * F )
proof
let f be FinSequence of REAL ; ::_thesis: ( f = sqr F iff f = sqrreal * F )
sqr F = sqrreal * F
proof
dom sqrreal = REAL by FUNCT_2:def_1;
then A1: rng F c= dom sqrreal ;
A2: dom (sqr F) = dom F by VALUED_1:11
.= dom (sqrreal * F) by A1, RELAT_1:27 ;
hence len (sqr F) = len (sqrreal * F) by FINSEQ_3:29; :: according to FINSEQ_1:def_17 ::_thesis: for b1 being set holds
( not 1 <= b1 or not b1 <= len (sqr F) or (sqr F) . b1 = (sqrreal * F) . b1 )
let k be Nat; ::_thesis: ( not 1 <= k or not k <= len (sqr F) or (sqr F) . k = (sqrreal * F) . k )
assume ( 1 <= k & k <= len (sqr F) ) ; ::_thesis: (sqr F) . k = (sqrreal * F) . k
then A3: k in dom (sqr F) by FINSEQ_3:25;
thus (sqr F) . k = (F . k) ^2 by VALUED_1:11
.= sqrreal . (F . k) by Def2
.= (sqrreal * F) . k by A2, A3, FUNCT_1:12 ; ::_thesis: verum
end;
hence ( f = sqr F iff f = sqrreal * F ) ; ::_thesis: verum
end;
coherence
sqr F is FinSequence of REAL by Lm2;
end;
:: deftheorem defines sqr RVSUM_1:def_8_:_
for F being real-valued FinSequence holds sqr F = sqrreal * F;
definition
let i be Nat;
let R be Element of i -tuples_on REAL;
:: original: sqr
redefine func sqr R -> Element of i -tuples_on REAL;
coherence
sqr R is Element of i -tuples_on REAL by FINSEQ_2:113;
end;
theorem :: RVSUM_1:55
for r being real number holds sqr <*r*> = <*(r ^2)*>
proof
let r be real number ; ::_thesis: sqr <*r*> = <*(r ^2)*>
reconsider s = r as Element of REAL by XREAL_0:def_1;
sqr <*s*> = <*(sqrreal . s)*> by FINSEQ_2:35
.= <*(r ^2)*> by Def2 ;
hence sqr <*r*> = <*(r ^2)*> ; ::_thesis: verum
end;
theorem :: RVSUM_1:56
for i being Nat
for r being real number holds sqr (i |-> r) = i |-> (r ^2)
proof
let i be Nat; ::_thesis: for r being real number holds sqr (i |-> r) = i |-> (r ^2)
let r be real number ; ::_thesis: sqr (i |-> r) = i |-> (r ^2)
reconsider s = r as Element of REAL by XREAL_0:def_1;
sqr (i |-> s) = i |-> (sqrreal . s) by FINSEQOP:16
.= i |-> (r ^2) by Def2 ;
hence sqr (i |-> r) = i |-> (r ^2) ; ::_thesis: verum
end;
theorem Th57: :: RVSUM_1:57
for F being real-valued FinSequence holds sqr (- F) = sqr F
proof
let F be real-valued FinSequence; ::_thesis: sqr (- F) = sqr F
A1: dom (sqr (- F)) = dom (- F) by VALUED_1:11
.= dom F by VALUED_1:8 ;
A2: dom (sqr F) = dom F by VALUED_1:11;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_(sqr_(-_F))_holds_
(sqr_(-_F))_._j_=_(sqr_F)_._j
let j be Nat; ::_thesis: ( j in dom (sqr (- F)) implies (sqr (- F)) . j = (sqr F) . j )
assume j in dom (sqr (- F)) ; ::_thesis: (sqr (- F)) . j = (sqr F) . j
set r = F . j;
set r9 = (- F) . j;
thus (sqr (- F)) . j = ((- F) . j) ^2 by VALUED_1:11
.= (- (F . j)) ^2 by VALUED_1:8
.= (F . j) ^2
.= (sqr F) . j by VALUED_1:11 ; ::_thesis: verum
end;
hence sqr (- F) = sqr F by A1, A2, FINSEQ_1:13; ::_thesis: verum
end;
theorem Th58: :: RVSUM_1:58
for r being real number
for F being real-valued FinSequence holds sqr (r * F) = (r ^2) * (sqr F)
proof
let r be real number ; ::_thesis: for F being real-valued FinSequence holds sqr (r * F) = (r ^2) * (sqr F)
let F be real-valued FinSequence; ::_thesis: sqr (r * F) = (r ^2) * (sqr F)
A1: dom (r * F) = dom F by VALUED_1:def_5;
A2: dom ((r ^2) * (sqr F)) = dom (sqr F) by VALUED_1:def_5;
A3: dom (sqr F) = dom F by VALUED_1:11;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_(r_*_F))_holds_
(sqr_(r_*_F))_._i_=_((r_^2)_*_(sqr_F))_._i
let i be Nat; ::_thesis: ( i in dom (sqr (r * F)) implies (sqr (r * F)) . i = ((r ^2) * (sqr F)) . i )
assume i in dom (sqr (r * F)) ; ::_thesis: (sqr (r * F)) . i = ((r ^2) * (sqr F)) . i
thus (sqr (r * F)) . i = ((r * F) . i) ^2 by VALUED_1:11
.= (r * (F . i)) ^2 by VALUED_1:6
.= (r ^2) * ((F . i) ^2)
.= (r ^2) * ((sqr F) . i) by VALUED_1:11
.= ((r ^2) * (sqr F)) . i by VALUED_1:6 ; ::_thesis: verum
end;
hence sqr (r * F) = (r ^2) * (sqr F) by A1, A2, A3, FINSEQ_1:13, VALUED_1:11; ::_thesis: verum
end;
notation
let F1, F2 be real-valued FinSequence;
synonym mlt (F1,F2) for F1 (#) F2;
end;
definition
let F1, F2 be real-valued FinSequence;
:: original: mlt
redefine func mlt (F1,F2) -> FinSequence of REAL equals :: RVSUM_1:def 9
multreal .: (F1,F2);
coherence
mlt (F1,F2) is FinSequence of REAL by Lm2;
compatibility
for b1 being FinSequence of REAL holds
( b1 = mlt (F1,F2) iff b1 = multreal .: (F1,F2) )
proof
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
let F be FinSequence of REAL ; ::_thesis: ( F = mlt (F1,F2) iff F = multreal .: (F1,F2) )
dom multreal = [:REAL,REAL:] by FUNCT_2:def_1;
then [:(rng F3),(rng F4):] c= dom multreal by ZFMISC_1:96;
then A1: dom (multreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;
A2: dom (mlt (F1,F2)) = (dom F1) /\ (dom F2) by VALUED_1:def_4;
thus ( F = mlt (F1,F2) implies F = multreal .: (F1,F2) ) ::_thesis: ( F = multreal .: (F1,F2) implies F = mlt (F1,F2) )
proof
assume A3: F = mlt (F1,F2) ; ::_thesis: F = multreal .: (F1,F2)
for z being set st z in dom (multreal .: (F1,F2)) holds
F . z = multreal . ((F1 . z),(F2 . z))
proof
let z be set ; ::_thesis: ( z in dom (multreal .: (F1,F2)) implies F . z = multreal . ((F1 . z),(F2 . z)) )
assume z in dom (multreal .: (F1,F2)) ; ::_thesis: F . z = multreal . ((F1 . z),(F2 . z))
thus F . z = (F1 . z) * (F2 . z) by A3, VALUED_1:5
.= multreal . ((F1 . z),(F2 . z)) by BINOP_2:def_11 ; ::_thesis: verum
end;
hence F = multreal .: (F1,F2) by A2, A1, A3, FUNCOP_1:21; ::_thesis: verum
end;
assume A4: F = multreal .: (F1,F2) ; ::_thesis: F = mlt (F1,F2)
now__::_thesis:_for_c_being_set_st_c_in_dom_F_holds_
F_._c_=_(F1_._c)_*_(F2_._c)
let c be set ; ::_thesis: ( c in dom F implies F . c = (F1 . c) * (F2 . c) )
assume c in dom F ; ::_thesis: F . c = (F1 . c) * (F2 . c)
hence F . c = multreal . ((F1 . c),(F2 . c)) by A4, FUNCOP_1:22
.= (F1 . c) * (F2 . c) by BINOP_2:def_11 ;
::_thesis: verum
end;
hence F = mlt (F1,F2) by A1, A4, VALUED_1:def_4; ::_thesis: verum
end;
commutativity
for b1 being FinSequence of REAL
for F1, F2 being real-valued FinSequence st b1 = multreal .: (F1,F2) holds
b1 = multreal .: (F2,F1)
proof
let F be FinSequence of REAL ; ::_thesis: for F1, F2 being real-valued FinSequence st F = multreal .: (F1,F2) holds
F = multreal .: (F2,F1)
let F1, F2 be real-valued FinSequence; ::_thesis: ( F = multreal .: (F1,F2) implies F = multreal .: (F2,F1) )
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
A5: dom multreal = [:REAL,REAL:] by FUNCT_2:def_1;
then A6: [:(rng F4),(rng F3):] c= dom multreal by ZFMISC_1:96;
[:(rng F3),(rng F4):] c= dom multreal by A5, ZFMISC_1:96;
then A7: dom (multreal .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69
.= dom (multreal .: (F2,F1)) by A6, FUNCOP_1:69 ;
assume A8: F = multreal .: (F1,F2) ; ::_thesis: F = multreal .: (F2,F1)
for z being set st z in dom (multreal .: (F2,F1)) holds
F . z = multreal . ((F2 . z),(F1 . z))
proof
let z be set ; ::_thesis: ( z in dom (multreal .: (F2,F1)) implies F . z = multreal . ((F2 . z),(F1 . z)) )
assume A9: z in dom (multreal .: (F2,F1)) ; ::_thesis: F . z = multreal . ((F2 . z),(F1 . z))
set F1z = F1 . z;
set F2z = F2 . z;
thus F . z = multreal . ((F1 . z),(F2 . z)) by A8, A7, A9, FUNCOP_1:22
.= (F1 . z) * (F2 . z) by BINOP_2:def_11
.= multreal . ((F2 . z),(F1 . z)) by BINOP_2:def_11 ; ::_thesis: verum
end;
hence F = multreal .: (F2,F1) by A8, A7, FUNCOP_1:21; ::_thesis: verum
end;
end;
:: deftheorem defines mlt RVSUM_1:def_9_:_
for F1, F2 being real-valued FinSequence holds mlt (F1,F2) = multreal .: (F1,F2);
theorem :: RVSUM_1:59
for s being set
for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;
definition
let i be Nat;
let R1, R2 be Element of i -tuples_on REAL;
:: original: mlt
redefine func mlt (R1,R2) -> Element of i -tuples_on REAL;
coherence
mlt (R1,R2) is Element of i -tuples_on REAL by FINSEQ_2:120;
end;
theorem :: RVSUM_1:60
for s being set
for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;
theorem :: RVSUM_1:61
for F being real-valued FinSequence holds mlt ((<*> REAL),F) = <*> REAL
proof
let F be real-valued FinSequence; ::_thesis: mlt ((<*> REAL),F) = <*> REAL
F is FinSequence of REAL by Lm2;
hence mlt ((<*> REAL),F) = <*> REAL by FINSEQ_2:73; ::_thesis: verum
end;
theorem :: RVSUM_1:62
for r1, r2 being real number holds mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*>
proof
let r1, r2 be real number ; ::_thesis: mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*>
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
mlt (<*s1*>,<*s2*>) = <*(multreal . (s1,s2))*> by FINSEQ_2:74
.= <*(r1 * r2)*> by BINOP_2:def_11 ;
hence mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*> ; ::_thesis: verum
end;
theorem Th63: :: RVSUM_1:63
for i being Nat
for r being real number
for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R
proof
let i be Nat; ::_thesis: for r being real number
for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R
let r be real number ; ::_thesis: for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R
let R be Element of i -tuples_on REAL; ::_thesis: mlt ((i |-> r),R) = r * R
reconsider s = r as Element of REAL by XREAL_0:def_1;
mlt ((i |-> s),R) = multreal [;] (s,R) by FINSEQOP:20
.= r * R by FINSEQOP:22 ;
hence mlt ((i |-> r),R) = r * R ; ::_thesis: verum
end;
theorem :: RVSUM_1:64
for i being Nat
for r1, r2 being real number holds mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2)
proof
let i be Nat; ::_thesis: for r1, r2 being real number holds mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2)
let r1, r2 be real number ; ::_thesis: mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
mlt ((i |-> s1),(i |-> s2)) = s1 * (i |-> s2) by Th63
.= i |-> (r1 * r2) by Th48 ;
hence mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2) ; ::_thesis: verum
end;
theorem :: RVSUM_1:65
for r being real number
for F1, F2 being real-valued FinSequence holds r * (mlt (F1,F2)) = mlt ((r * F1),F2) by RFUNCT_1:12;
theorem :: RVSUM_1:66
for i being Nat
for r being real number
for R being Element of i -tuples_on REAL holds r * R = mlt ((i |-> r),R) by Th63;
theorem :: RVSUM_1:67
for F being real-valued FinSequence holds sqr F = mlt (F,F) ;
theorem Th68: :: RVSUM_1:68
for F1, F2 being real-valued FinSequence holds sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)
proof
let F1, F2 be real-valued FinSequence; ::_thesis: sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)
A1: dom (sqr (F1 + F2)) = dom (F1 + F2) by VALUED_1:11;
A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def_1;
A3: dom ((sqr F1) + (2 * (mlt (F1,F2)))) = (dom (sqr F1)) /\ (dom (2 * (mlt (F1,F2)))) by VALUED_1:def_1
.= (dom F1) /\ (dom (2 * (mlt (F1,F2)))) by VALUED_1:11
.= (dom F1) /\ (dom (mlt (F1,F2))) by VALUED_1:def_5
.= (dom F1) /\ ((dom F1) /\ (dom F2)) by VALUED_1:def_4
.= ((dom F1) /\ (dom F1)) /\ (dom F2) by XBOOLE_1:16
.= (dom F1) /\ (dom F2) ;
then A4: dom (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) = ((dom F1) /\ (dom F2)) /\ (dom (sqr F2)) by VALUED_1:def_1
.= ((dom F1) /\ (dom F2)) /\ (dom F2) by VALUED_1:11
.= (dom F1) /\ ((dom F2) /\ (dom F2)) by XBOOLE_1:16 ;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_(sqr_(F1_+_F2))_holds_
(sqr_(F1_+_F2))_._j_=_(((sqr_F1)_+_(2_*_(mlt_(F1,F2))))_+_(sqr_F2))_._j
let j be Nat; ::_thesis: ( j in dom (sqr (F1 + F2)) implies (sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j )
assume A5: j in dom (sqr (F1 + F2)) ; ::_thesis: (sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j
set r1r2 = (F1 + F2) . j;
set r1 = F1 . j;
set r2 = F2 . j;
set r192 = (sqr F1) . j;
set r292 = (sqr F2) . j;
set r1r2a = (mlt (F1,F2)) . j;
set 2r1r2 = (2 * (mlt (F1,F2))) . j;
set r1922r1r2 = ((sqr F1) + (2 * (mlt (F1,F2)))) . j;
thus (sqr (F1 + F2)) . j = ((F1 + F2) . j) ^2 by VALUED_1:11
.= ((F1 . j) + (F2 . j)) ^2 by A1, A5, VALUED_1:def_1
.= (((F1 . j) ^2) + ((2 * (F1 . j)) * (F2 . j))) + ((F2 . j) ^2)
.= (((sqr F1) . j) + (2 * ((F1 . j) * (F2 . j)))) + ((F2 . j) ^2) by VALUED_1:11
.= (((sqr F1) . j) + (2 * ((F1 . j) * (F2 . j)))) + ((sqr F2) . j) by VALUED_1:11
.= (((sqr F1) . j) + (2 * ((mlt (F1,F2)) . j))) + ((sqr F2) . j) by VALUED_1:5
.= (((sqr F1) . j) + ((2 * (mlt (F1,F2))) . j)) + ((sqr F2) . j) by VALUED_1:6
.= (((sqr F1) + (2 * (mlt (F1,F2)))) . j) + ((sqr F2) . j) by A1, A2, A3, A5, VALUED_1:def_1
.= (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j by A1, A2, A4, A5, VALUED_1:def_1 ; ::_thesis: verum
end;
hence sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2) by A2, A4, FINSEQ_1:13, VALUED_1:11; ::_thesis: verum
end;
theorem Th69: :: RVSUM_1:69
for F1, F2 being real-valued FinSequence holds sqr (F1 - F2) = ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2)
proof
let F1, F2 be real-valued FinSequence; ::_thesis: sqr (F1 - F2) = ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2)
thus sqr (F1 - F2) = ((sqr F1) + (2 * (mlt (F1,(- F2))))) + (sqr (- F2)) by Th68
.= ((sqr F1) + (2 * (mlt (F1,(- F2))))) + (sqr F2) by Th57
.= ((sqr F1) + (2 * ((- 1) * (mlt (F1,F2))))) + (sqr F2) by RFUNCT_1:12
.= ((sqr F1) + (((- 1) * 2) * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:17
.= ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2) by RFUNCT_1:17 ; ::_thesis: verum
end;
theorem :: RVSUM_1:70
for F1, F2 being real-valued FinSequence holds sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2))
proof
let F1, F2 be real-valued FinSequence; ::_thesis: sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2))
A1: dom (mlt (F1,F2)) = (dom F1) /\ (dom F2) by VALUED_1:def_4;
A2: dom (mlt ((sqr F1),(sqr F2))) = (dom (sqr F1)) /\ (dom (sqr F2)) by VALUED_1:def_4;
A3: dom (sqr F1) = dom F1 by VALUED_1:11;
A4: dom (sqr F2) = dom F2 by VALUED_1:11;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_(mlt_(F1,F2)))_holds_
(sqr_(mlt_(F1,F2)))_._i_=_(mlt_((sqr_F1),(sqr_F2)))_._i
let i be Nat; ::_thesis: ( i in dom (sqr (mlt (F1,F2))) implies (sqr (mlt (F1,F2))) . i = (mlt ((sqr F1),(sqr F2))) . i )
assume i in dom (sqr (mlt (F1,F2))) ; ::_thesis: (sqr (mlt (F1,F2))) . i = (mlt ((sqr F1),(sqr F2))) . i
thus (sqr (mlt (F1,F2))) . i = ((mlt (F1,F2)) . i) ^2 by VALUED_1:11
.= ((F1 . i) * (F2 . i)) ^2 by VALUED_1:5
.= ((F1 . i) ^2) * ((F2 . i) ^2)
.= ((sqr F1) . i) * ((F2 . i) ^2) by VALUED_1:11
.= ((sqr F1) . i) * ((sqr F2) . i) by VALUED_1:11
.= (mlt ((sqr F1),(sqr F2))) . i by VALUED_1:5 ; ::_thesis: verum
end;
hence sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2)) by A1, A2, A3, A4, FINSEQ_1:13, VALUED_1:11; ::_thesis: verum
end;
notation
let F be Relation;
synonym complex-yielding F for complex-valued ;
end;
registration
cluster -> complex-valued for FinSequence of COMPLEX ;
coherence
for b1 being FinSequence of COMPLEX holds b1 is complex-valued ;
cluster Relation-like NAT -defined Function-like complex-valued real-valued V60() FinSequence-like FinSubsequence-like for set ;
existence
ex b1 being FinSequence st
( b1 is real-valued & b1 is complex-valued )
proof
<*> REAL is real-valued ;
hence ex b1 being FinSequence st
( b1 is real-valued & b1 is complex-valued ) ; ::_thesis: verum
end;
end;
definition
let F be complex-valued FinSequence;
func Sum F -> complex number means :Def10: :: RVSUM_1:def 10
ex f being FinSequence of COMPLEX st
( f = F & it = addcomplex $$ f );
existence
ex b1 being complex number ex f being FinSequence of COMPLEX st
( f = F & b1 = addcomplex $$ f )
proof
rng F c= COMPLEX by VALUED_0:def_1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4;
take addcomplex $$ f ; ::_thesis: ex f being FinSequence of COMPLEX st
( f = F & addcomplex $$ f = addcomplex $$ f )
thus ex f being FinSequence of COMPLEX st
( f = F & addcomplex $$ f = addcomplex $$ f ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being complex number st ex f being FinSequence of COMPLEX st
( f = F & b1 = addcomplex $$ f ) & ex f being FinSequence of COMPLEX st
( f = F & b2 = addcomplex $$ f ) holds
b1 = b2 ;
end;
:: deftheorem Def10 defines Sum RVSUM_1:def_10_:_
for F being complex-valued FinSequence
for b2 being complex number holds
( b2 = Sum F iff ex f being FinSequence of COMPLEX st
( f = F & b2 = addcomplex $$ f ) );
registration
let F be real-valued FinSequence;
cluster Sum F -> complex real ;
coherence
Sum F is real
proof
set mc = addcomplex ;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Sum F = addcomplex $$ f by Def10;
set g = [#] (f,(the_unity_wrt addcomplex));
defpred S1[ Nat] means addcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt addcomplex)))) is real ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real
proof
percases ( k + 1 in dom f or not k + 1 in dom f ) ;
suppose k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real
then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20;
hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real by A1; ::_thesis: verum
end;
suppose not k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real
hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is real by BINOP_2:1, SETWOP_2:20; ::_thesis: verum
end;
end;
end;
then reconsider a = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1), b = addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex)))) as real number by A4;
not k + 1 in Seg k by FINSEQ_3:8;
then addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) = addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by SETWOP_2:2
.= b + a by BINOP_2:def_3 ;
hence S1[k + 1] by FINSEQ_1:9; ::_thesis: verum
end;
A5: ( addcomplex $$ f = addcomplex $$ ((findom f),([#] (f,(the_unity_wrt addcomplex)))) & ex n being Nat st dom f = Seg n ) by FINSEQ_1:def_2, SETWOP_2:def_2;
Seg 0 = {}. NAT ;
then A6: S1[ 0 ] by BINOP_2:1, SETWISEO:31;
for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3);
hence Sum F is real by A2, A5; ::_thesis: verum
end;
end;
theorem Th71: :: RVSUM_1:71
for F being FinSequence of REAL holds Sum F = addreal $$ F
proof
set g = addreal ;
set h = addcomplex ;
let F be FinSequence of REAL ; ::_thesis: Sum F = addreal $$ F
rng F c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4;
defpred S1[ Nat] means addreal $$ ((finSeg $1),([#] (F,(the_unity_wrt addreal)))) = addcomplex $$ ((finSeg $1),([#] (f,(the_unity_wrt addcomplex))));
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def_2;
A2: ( addreal $$ F = addreal $$ ((finSeg n),([#] (F,(the_unity_wrt addreal)))) & addcomplex $$ f = addcomplex $$ ((finSeg n),([#] (f,(the_unity_wrt addcomplex)))) ) by A1, SETWOP_2:def_2;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
set j = [#] (f,(the_unity_wrt addcomplex));
set i = [#] (F,(the_unity_wrt addreal));
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A5: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1)
proof
percases ( k + 1 in dom f or not k + 1 in dom f ) ;
supposeA6: k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1)
then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = F . (k + 1) by SETWOP_2:20
.= ([#] (F,(the_unity_wrt addreal))) . (k + 1) by A6, SETWOP_2:20 ;
hence ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) ; ::_thesis: verum
end;
supposeA7: not k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1)
then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = the_unity_wrt addcomplex by SETWOP_2:20
.= ([#] (F,(the_unity_wrt addreal))) . (k + 1) by A7, BINOP_2:1, BINOP_2:2, SETWOP_2:20 ;
hence ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) ; ::_thesis: verum
end;
end;
end;
A8: not k + 1 in Seg k by FINSEQ_3:8;
addreal $$ ((finSeg (k + 1)),([#] (F,(the_unity_wrt addreal)))) = addreal $$ (((finSeg k) \/ {.(k + 1).}),([#] (F,(the_unity_wrt addreal)))) by FINSEQ_1:9
.= addreal . ((addreal $$ ((finSeg k),([#] (F,(the_unity_wrt addreal))))),(([#] (F,(the_unity_wrt addreal))) . (k + 1))) by A8, SETWOP_2:2
.= (addreal $$ ((finSeg k),([#] (F,(the_unity_wrt addreal))))) + (([#] (F,(the_unity_wrt addreal))) . (k + 1)) by BINOP_2:def_9
.= addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by A4, A5, BINOP_2:def_3
.= addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) by A8, SETWOP_2:2
.= addcomplex $$ ((finSeg (k + 1)),([#] (f,(the_unity_wrt addcomplex)))) by FINSEQ_1:9 ;
hence S1[k + 1] ; ::_thesis: verum
end;
A9: Seg 0 = {}. NAT ;
then addreal $$ ((finSeg 0),([#] (F,(the_unity_wrt addreal)))) = the_unity_wrt addcomplex by BINOP_2:1, BINOP_2:2, SETWISEO:31
.= addcomplex $$ ((finSeg 0),([#] (f,(the_unity_wrt addcomplex)))) by A9, SETWISEO:31 ;
then A10: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A10, A3);
then addreal $$ F = addcomplex $$ f by A2;
hence Sum F = addreal $$ F by Def10; ::_thesis: verum
end;
definition
let F be FinSequence of COMPLEX ;
:: original: Sum
redefine func Sum F -> Element of COMPLEX equals :: RVSUM_1:def 11
addcomplex $$ F;
coherence
Sum F is Element of COMPLEX by XCMPLX_0:def_2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = Sum F iff b1 = addcomplex $$ F ) by Def10;
end;
:: deftheorem defines Sum RVSUM_1:def_11_:_
for F being FinSequence of COMPLEX holds Sum F = addcomplex $$ F;
definition
let F be FinSequence of REAL ;
:: original: Sum
redefine func Sum F -> Element of REAL equals :: RVSUM_1:def 12
addreal $$ F;
coherence
Sum F is Element of REAL by XREAL_0:def_1;
compatibility
for b1 being Element of REAL holds
( b1 = Sum F iff b1 = addreal $$ F ) by Th71;
end;
:: deftheorem defines Sum RVSUM_1:def_12_:_
for F being FinSequence of REAL holds Sum F = addreal $$ F;
theorem Th72: :: RVSUM_1:72
Sum (<*> REAL) = 0 by BINOP_2:2, FINSOP_1:10;
theorem :: RVSUM_1:73
for r being real number holds Sum <*r*> = r
proof
let r be real number ; ::_thesis: Sum <*r*> = r
reconsider r = r as Element of REAL by XREAL_0:def_1;
Sum <*r*> = r by FINSOP_1:11;
hence Sum <*r*> = r ; ::_thesis: verum
end;
theorem Th74: :: RVSUM_1:74
for r being real number
for F being real-valued FinSequence holds Sum (F ^ <*r*>) = (Sum F) + r
proof
let r be real number ; ::_thesis: for F being real-valued FinSequence holds Sum (F ^ <*r*>) = (Sum F) + r
let F be real-valued FinSequence; ::_thesis: Sum (F ^ <*r*>) = (Sum F) + r
reconsider s = r as Element of REAL by XREAL_0:def_1;
reconsider F1 = F as FinSequence of REAL by Lm2;
thus Sum (F ^ <*r*>) = Sum (F1 ^ <*s*>)
.= addreal . ((addreal $$ F1),s) by FINSOP_1:4
.= (Sum F1) + r by BINOP_2:def_9
.= (Sum F) + r ; ::_thesis: verum
end;
theorem Th75: :: RVSUM_1:75
for F1, F2 being real-valued FinSequence holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
proof
let F1, F2 be real-valued FinSequence; ::_thesis: Sum (F1 ^ F2) = (Sum F1) + (Sum F2)
reconsider F3 = F1, F4 = F2 as FinSequence of REAL by Lm2;
thus Sum (F1 ^ F2) = Sum (F3 ^ F4)
.= addreal . ((addreal $$ F3),(addreal $$ F4)) by FINSOP_1:5
.= (Sum F3) + (Sum F4) by BINOP_2:def_9
.= (Sum F1) + (Sum F2) ; ::_thesis: verum
end;
theorem :: RVSUM_1:76
for r being real number
for F being real-valued FinSequence holds Sum (<*r*> ^ F) = r + (Sum F)
proof
let r be real number ; ::_thesis: for F being real-valued FinSequence holds Sum (<*r*> ^ F) = r + (Sum F)
let F be real-valued FinSequence; ::_thesis: Sum (<*r*> ^ F) = r + (Sum F)
reconsider s = r as Element of REAL by XREAL_0:def_1;
thus Sum (<*r*> ^ F) = (Sum <*s*>) + (Sum F) by Th75
.= r + (Sum F) by FINSOP_1:11 ; ::_thesis: verum
end;
theorem Th77: :: RVSUM_1:77
for r1, r2 being real number holds Sum <*r1,r2*> = r1 + r2
proof
let r1, r2 be real number ; ::_thesis: Sum <*r1,r2*> = r1 + r2
reconsider s1 = r1 as Element of REAL by XREAL_0:def_1;
thus Sum <*r1,r2*> = (Sum <*s1*>) + r2 by Th74
.= r1 + r2 by FINSOP_1:11 ; ::_thesis: verum
end;
theorem Th78: :: RVSUM_1:78
for r1, r2, r3 being real number holds Sum <*r1,r2,r3*> = (r1 + r2) + r3
proof
let r1, r2, r3 be real number ; ::_thesis: Sum <*r1,r2,r3*> = (r1 + r2) + r3
thus Sum <*r1,r2,r3*> = (Sum <*r1,r2*>) + r3 by Th74
.= (r1 + r2) + r3 by Th77 ; ::_thesis: verum
end;
theorem :: RVSUM_1:79
for R being Element of 0 -tuples_on REAL holds Sum R = 0 by Th72;
theorem Th80: :: RVSUM_1:80
for i being Nat
for r being real number holds Sum (i |-> r) = i * r
proof
let i be Nat; ::_thesis: for r being real number holds Sum (i |-> r) = i * r
let r be real number ; ::_thesis: Sum (i |-> r) = i * r
reconsider r = r as Element of REAL by XREAL_0:def_1;
defpred S1[ Nat] means Sum ($1 |-> r) = $1 * r;
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: Sum (i |-> r) = i * r ; ::_thesis: S1[i + 1]
thus Sum ((i + 1) |-> r) = Sum ((i |-> r) ^ <*r*>) by FINSEQ_2:60
.= (i * r) + (1 * r) by A2, Th74
.= (i + 1) * r ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th72;
for i being Nat holds S1[i] from NAT_1:sch_2(A3, A1);
hence Sum (i |-> r) = i * r ; ::_thesis: verum
end;
theorem Th81: :: RVSUM_1:81
for i being Nat holds Sum (i |-> 0) = 0
proof
let i be Nat; ::_thesis: Sum (i |-> 0) = 0
thus Sum (i |-> 0) = i * 0 by Th80
.= 0 ; ::_thesis: verum
end;
theorem Th82: :: RVSUM_1:82
for i being Nat
for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2
proof
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 )
defpred S1[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL st ( for j being Nat st j in Seg $1 holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2;
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2 ; ::_thesis: S1[i + 1]
set n = i + 1;
let R1, R2 be Element of (i + 1) -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 )
assume A3: for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ; ::_thesis: Sum R1 <= Sum R2
consider R19 being Element of i -tuples_on REAL, x1 being Element of REAL such that
A4: R1 = R19 ^ <*x1*> by FINSEQ_2:117;
consider R29 being Element of i -tuples_on REAL, x2 being Element of REAL such that
A5: R2 = R29 ^ <*x2*> by FINSEQ_2:117;
for j being Nat st j in Seg i holds
R19 . j <= R29 . j
proof
let j be Nat; ::_thesis: ( j in Seg i implies R19 . j <= R29 . j )
assume A6: j in Seg i ; ::_thesis: R19 . j <= R29 . j
( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def_7, FINSEQ_1:def_3;
then A7: R29 . j = R2 . j by A5, A6, FINSEQ_1:def_7;
( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def_7, FINSEQ_1:def_3;
then R19 . j = R1 . j by A4, A6, FINSEQ_1:def_7;
hence R19 . j <= R29 . j by A3, A6, A7, FINSEQ_2:8; ::_thesis: verum
end;
then A8: Sum R19 <= Sum R29 by A2;
A9: R2 . (i + 1) = x2 by A5, FINSEQ_2:116;
R1 . (i + 1) = x1 by A4, FINSEQ_2:116;
then A10: x1 <= x2 by A3, A9, FINSEQ_1:4;
A11: Sum R2 = (Sum R29) + x2 by A5, Th74;
Sum R1 = (Sum R19) + x1 by A4, Th74;
hence Sum R1 <= Sum R2 by A10, A8, A11, XREAL_1:7; ::_thesis: verum
end;
A12: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch_2(A12, A1);
hence ( ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) implies Sum R1 <= Sum R2 ) ; ::_thesis: verum
end;
theorem Th83: :: RVSUM_1:83
for i being Nat
for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg i & R1 . j < R2 . j ) holds
Sum R1 < Sum R2
proof
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg i & R1 . j < R2 . j ) holds
Sum R1 < Sum R2
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg i & R1 . j < R2 . j ) implies Sum R1 < Sum R2 )
defpred S1[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL st ( for j being Nat st j in Seg $1 holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg $1 & R1 . j < R2 . j ) holds
Sum R1 < Sum R2;
now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_
for_R1,_R2_being_Element_of_(i_+_1)_-tuples_on_REAL_st_(_for_j_being_Nat_st_j_in_Seg_(i_+_1)_holds_
R1_._j_<=_R2_._j_)_&_ex_j_being_Nat_st_
(_j_in_Seg_(i_+_1)_&_R1_._j_<_R2_._j_)_holds_
Sum_R1_<_Sum_R2
let i be Nat; ::_thesis: ( S1[i] implies for R1, R2 being Element of (i + 1) -tuples_on REAL st ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) holds
Sum R1 < Sum R2 )
assume A1: S1[i] ; ::_thesis: for R1, R2 being Element of (i + 1) -tuples_on REAL st ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) holds
Sum R1 < Sum R2
let R1, R2 be Element of (i + 1) -tuples_on REAL; ::_thesis: ( ( for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) implies Sum R1 < Sum R2 )
assume A2: for j being Nat st j in Seg (i + 1) holds
R1 . j <= R2 . j ; ::_thesis: ( ex j being Nat st
( j in Seg (i + 1) & R1 . j < R2 . j ) implies Sum R1 < Sum R2 )
given j being Nat such that A3: j in Seg (i + 1) and
A4: R1 . j < R2 . j ; ::_thesis: Sum R1 < Sum R2
consider R19 being Element of i -tuples_on REAL, x1 being Element of REAL such that
A5: R1 = R19 ^ <*x1*> by FINSEQ_2:117;
consider R29 being Element of i -tuples_on REAL, x2 being Element of REAL such that
A6: R2 = R29 ^ <*x2*> by FINSEQ_2:117;
A7: for j being Nat st j in Seg i holds
R19 . j <= R29 . j
proof
let j be Nat; ::_thesis: ( j in Seg i implies R19 . j <= R29 . j )
assume A8: j in Seg i ; ::_thesis: R19 . j <= R29 . j
( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def_7, FINSEQ_1:def_3;
then A9: R29 . j = R2 . j by A6, A8, FINSEQ_1:def_7;
( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def_7, FINSEQ_1:def_3;
then R19 . j = R1 . j by A5, A8, FINSEQ_1:def_7;
hence R19 . j <= R29 . j by A2, A8, A9, FINSEQ_2:8; ::_thesis: verum
end;
A10: R2 . (i + 1) = x2 by A6, FINSEQ_2:116;
A11: R1 . (i + 1) = x1 by A5, FINSEQ_2:116;
now__::_thesis:_Sum_R1_<_Sum_R2
percases ( j in Seg i or j = i + 1 ) by A3, FINSEQ_2:7;
supposeA12: j in Seg i ; ::_thesis: Sum R1 < Sum R2
( Seg (len R29) = dom R29 & len R29 = i ) by CARD_1:def_7, FINSEQ_1:def_3;
then A13: R29 . j = R2 . j by A6, A12, FINSEQ_1:def_7;
A14: ( Sum R1 = (Sum R19) + x1 & Sum R2 = (Sum R29) + x2 ) by A5, A6, Th74;
A15: x1 <= x2 by A2, A11, A10, FINSEQ_1:4;
( Seg (len R19) = dom R19 & len R19 = i ) by CARD_1:def_7, FINSEQ_1:def_3;
then R19 . j = R1 . j by A5, A12, FINSEQ_1:def_7;
then Sum R19 < Sum R29 by A1, A4, A7, A12, A13;
hence Sum R1 < Sum R2 by A14, A15, XREAL_1:8; ::_thesis: verum
end;
supposeA16: j = i + 1 ; ::_thesis: Sum R1 < Sum R2
A17: Sum R2 = (Sum R29) + x2 by A6, Th74;
( Sum R19 <= Sum R29 & Sum R1 = (Sum R19) + x1 ) by A5, A7, Th74, Th82;
hence Sum R1 < Sum R2 by A4, A11, A10, A16, A17, XREAL_1:8; ::_thesis: verum
end;
end;
end;
hence Sum R1 < Sum R2 ; ::_thesis: verum
end;
then A18: for i being Nat st S1[i] holds
S1[i + 1] ;
A19: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch_2(A19, A18);
hence ( ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg i & R1 . j < R2 . j ) implies Sum R1 < Sum R2 ) ; ::_thesis: verum
end;
theorem Th84: :: RVSUM_1:84
for F being real-valued FinSequence st ( for i being Nat st i in dom F holds
0 <= F . i ) holds
0 <= Sum F
proof
let F be real-valued FinSequence; ::_thesis: ( ( for i being Nat st i in dom F holds
0 <= F . i ) implies 0 <= Sum F )
reconsider F1 = F as FinSequence of REAL by Lm2;
set i = len F;
set R1 = (len F) |-> 0;
reconsider R2 = F1 as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: Seg (len F) = dom F by FINSEQ_1:def_3;
assume A2: for i being Nat st i in dom F holds
0 <= F . i ; ::_thesis: 0 <= Sum F
for j being Nat st j in Seg (len F) holds
((len F) |-> 0) . j <= R2 . j by A2, A1;
then Sum ((len F) |-> 0) <= Sum R2 by Th82;
hence 0 <= Sum F by Th81; ::_thesis: verum
end;
theorem Th85: :: RVSUM_1:85
for F being real-valued FinSequence st ( for i being Nat st i in dom F holds
0 <= F . i ) & ex i being Nat st
( i in dom F & 0 < F . i ) holds
0 < Sum F
proof
let F be real-valued FinSequence; ::_thesis: ( ( for i being Nat st i in dom F holds
0 <= F . i ) & ex i being Nat st
( i in dom F & 0 < F . i ) implies 0 < Sum F )
reconsider F1 = F as FinSequence of REAL by Lm2;
set i = len F;
set R1 = (len F) |-> 0;
reconsider R2 = F1 as Element of (len F) -tuples_on REAL by FINSEQ_2:92;
A1: Seg (len F) = dom F by FINSEQ_1:def_3;
assume A2: for i being Nat st i in dom F holds
0 <= F . i ; ::_thesis: ( for i being Nat holds
( not i in dom F or not 0 < F . i ) or 0 < Sum F )
A3: for j being Nat st j in Seg (len F) holds
((len F) |-> 0) . j <= R2 . j by A2, A1;
given j being Nat such that A5: j in dom F and
A6: 0 < F . j ; ::_thesis: 0 < Sum F
((len F) |-> 0) . j = 0 ;
then Sum ((len F) |-> 0) < Sum R2 by A1, A3, A5, A6, Th83;
hence 0 < Sum F by Th81; ::_thesis: verum
end;
theorem Th86: :: RVSUM_1:86
for F being real-valued FinSequence holds 0 <= Sum (sqr F)
proof
let F be real-valued FinSequence; ::_thesis: 0 <= Sum (sqr F)
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_F)_holds_
0_<=_(sqr_F)_._i
let i be Nat; ::_thesis: ( i in dom (sqr F) implies 0 <= (sqr F) . i )
assume i in dom (sqr F) ; ::_thesis: 0 <= (sqr F) . i
0 <= (F . i) ^2 by XREAL_1:63;
hence 0 <= (sqr F) . i by VALUED_1:11; ::_thesis: verum
end;
hence 0 <= Sum (sqr F) by Th84; ::_thesis: verum
end;
theorem Th87: :: RVSUM_1:87
for r being real number
for F being real-valued FinSequence holds Sum (r * F) = r * (Sum F)
proof
let r be real number ; ::_thesis: for F being real-valued FinSequence holds Sum (r * F) = r * (Sum F)
let F be real-valued FinSequence; ::_thesis: Sum (r * F) = r * (Sum F)
reconsider F1 = F as FinSequence of REAL by Lm2;
reconsider s = r as Element of REAL by XREAL_0:def_1;
set rM = multreal [;] (s,(id REAL));
thus Sum (r * F) = (multreal [;] (s,(id REAL))) . (addreal $$ F1) by Th3, Th8, SETWOP_2:30
.= r * (Sum F1) by Lm1
.= r * (Sum F) ; ::_thesis: verum
end;
theorem Th88: :: RVSUM_1:88
for F being real-valued FinSequence holds Sum (- F) = - (Sum F)
proof
let F be real-valued FinSequence; ::_thesis: Sum (- F) = - (Sum F)
reconsider F1 = F as FinSequence of REAL by Lm2;
thus Sum (- F) = compreal . (addreal $$ F1) by Th8, Th9, SETWOP_2:31
.= - (Sum F1) by BINOP_2:def_7
.= - (Sum F) ; ::_thesis: verum
end;
theorem Th89: :: RVSUM_1:89
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)
proof
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: Sum (R1 + R2) = (Sum R1) + (Sum R2)
thus Sum (R1 + R2) = addreal . ((addreal $$ R1),(addreal $$ R2)) by SETWOP_2:35
.= (Sum R1) + (Sum R2) by BINOP_2:def_9 ; ::_thesis: verum
end;
theorem Th90: :: RVSUM_1:90
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
proof
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2)
thus Sum (R1 - R2) = (Sum R1) + (Sum (- R2)) by Th89
.= (Sum R1) + (- (Sum R2)) by Th88
.= (Sum R1) - (Sum R2) ; ::_thesis: verum
end;
theorem :: RVSUM_1:91
for i being Nat
for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds
R = i |-> 0
proof
let i be Nat; ::_thesis: for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds
R = i |-> 0
let R be Element of i -tuples_on REAL; ::_thesis: ( Sum (sqr R) = 0 implies R = i |-> 0 )
assume A1: Sum (sqr R) = 0 ; ::_thesis: R = i |-> 0
A2: len R = i by CARD_1:def_7;
A3: len (i |-> 0) = i by CARD_1:def_7;
assume R <> i |-> 0 ; ::_thesis: contradiction
then consider j being Nat such that
A4: j in dom R and
A5: R . j <> (i |-> 0) . j by A2, A3, FINSEQ_2:9;
set x = R . j;
set x9 = (sqr R) . j;
A6: dom R = Seg (len R) by FINSEQ_1:def_3;
R . j <> 0 by A5;
then 0 < (R . j) ^2 by SQUARE_1:12;
then A7: 0 < (sqr R) . j by VALUED_1:11;
A8: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(sqr_R)_holds_
0_<=_(sqr_R)_._k
let k be Nat; ::_thesis: ( k in dom (sqr R) implies 0 <= (sqr R) . k )
assume k in dom (sqr R) ; ::_thesis: 0 <= (sqr R) . k
set r = (sqr R) . k;
set x = R . k;
0 <= (R . k) ^2 by XREAL_1:63;
hence 0 <= (sqr R) . k by VALUED_1:11; ::_thesis: verum
end;
dom (sqr R) = Seg (len (sqr R)) by FINSEQ_1:def_3;
then j in dom (sqr R) by A4, A6, FINSEQ_2:33;
hence contradiction by A1, A8, A7, Th85; ::_thesis: verum
end;
theorem :: RVSUM_1:92
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
proof
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
defpred S1[ Nat] means for R1, R2 being Element of $1 -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2));
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A2: for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; ::_thesis: S1[i + 1]
let R1, R2 be Element of (i + 1) -tuples_on REAL; ::_thesis: (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
consider R19 being Element of i -tuples_on REAL, x1 being Element of REAL such that
A3: R1 = R19 ^ <*x1*> by FINSEQ_2:117;
consider R29 being Element of i -tuples_on REAL, x2 being Element of REAL such that
A4: R2 = R29 ^ <*x2*> by FINSEQ_2:117;
A5: for r being real number
for R being Element of i -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2)
proof
let r be real number ; ::_thesis: for R being Element of i -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2)
let R be Element of i -tuples_on REAL; ::_thesis: Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2)
reconsider s = r as Element of REAL by XREAL_0:def_1;
sqr (R ^ <*s*>) = (sqrreal * R) ^ <*(sqrreal . s)*> by FINSEQOP:8
.= (sqr R) ^ <*(r ^2)*> by Def2 ;
hence Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2) by Th74; ::_thesis: verum
end;
then A6: (Sum (sqr R29)) + (x2 ^2) = Sum (sqr R2) by A4;
((Sum (mlt (R19,R29))) ^2) + 0 <= (Sum (sqr R19)) * (Sum (sqr R29)) by A2;
then A7: 0 <= ((Sum (sqr R19)) * (Sum (sqr R29))) - ((Sum (mlt (R19,R29))) ^2) by XREAL_1:19;
mlt ((R19 ^ <*x1*>),(R29 ^ <*x2*>)) = (multreal .: (R19,R29)) ^ <*(multreal . (x1,x2))*> by FINSEQOP:10
.= (mlt (R19,R29)) ^ <*(x1 * x2)*> by BINOP_2:def_11 ;
then A8: Sum (mlt ((R19 ^ <*x1*>),(R29 ^ <*x2*>))) = (Sum (mlt (R19,R29))) + (x1 * x2) by Th74;
A9: (2 * (x1 * x2)) * (Sum (mlt (R19,R29))) = 2 * ((x1 * x2) * (Sum (mlt (R19,R29))))
.= 2 * (Sum ((x1 * x2) * (mlt (R19,R29)))) by Th87
.= 2 * (Sum (x1 * (x2 * (mlt (R19,R29))))) by RFUNCT_1:17
.= 2 * (Sum (x1 * (mlt (R29,(x2 * R19))))) by RFUNCT_1:12
.= 2 * (Sum (mlt ((x1 * R29),(x2 * R19)))) by FINSEQOP:26 ;
A10: - (((Sum (mlt (R19,R29))) + (x1 * x2)) ^2) = (- ((x1 * x2) ^2)) + (- (((2 * (x1 * x2)) * (Sum (mlt (R19,R29)))) + ((Sum (mlt (R19,R29))) ^2)))
.= (- ((x1 ^2) * (x2 ^2))) + ((- ((Sum (mlt (R19,R29))) ^2)) + (- (2 * (Sum (mlt ((x1 * R29),(x2 * R19))))))) by A9 ;
A11: 0 <= Sum (sqr ((x1 * R29) - (x2 * R19))) by Th86;
A12: ((Sum (sqr R19)) + (x1 ^2)) * ((Sum (sqr R29)) + (x2 ^2)) = (((Sum (sqr R19)) * (Sum (sqr R29))) + (((x1 ^2) * (Sum (sqr R29))) + ((Sum (sqr R19)) * (x2 ^2)))) + ((x1 ^2) * (x2 ^2))
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum ((x1 ^2) * (sqr R29))) + ((Sum (sqr R19)) * (x2 ^2)))) + ((x1 ^2) * (x2 ^2)) by Th87
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + ((x2 ^2) * (Sum (sqr R19))))) + ((x1 ^2) * (x2 ^2)) by Th58
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + (Sum ((x2 ^2) * (sqr R19))))) + ((x1 ^2) * (x2 ^2)) by Th87
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + ((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19))))) + ((x1 ^2) * (x2 ^2)) by Th58 ;
A13: ((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19)))) + (- (2 * (Sum (mlt ((x1 * R29),(x2 * R19)))))) = ((Sum (sqr (x1 * R29))) - (2 * (Sum (mlt ((x1 * R29),(x2 * R19)))))) + (Sum (sqr (x2 * R19)))
.= ((Sum (sqr (x1 * R29))) - (Sum (2 * (mlt ((x1 * R29),(x2 * R19)))))) + (Sum (sqr (x2 * R19))) by Th87
.= (Sum ((sqr (x1 * R29)) - (2 * (mlt ((x1 * R29),(x2 * R19)))))) + (Sum (sqr (x2 * R19))) by Th90
.= Sum (((sqr (x1 * R29)) - (2 * (mlt ((x1 * R29),(x2 * R19))))) + (sqr (x2 * R19))) by Th89 ;
(Sum (sqr R19)) + (x1 ^2) = Sum (sqr R1) by A3, A5;
then ((Sum (sqr R1)) * (Sum (sqr R2))) - ((Sum (mlt (R1,R2))) ^2) = (((Sum (sqr R19)) + (x1 ^2)) * ((Sum (sqr R29)) + (x2 ^2))) + (- (((Sum (mlt (R19,R29))) + (x1 * x2)) ^2)) by A3, A4, A8, A6
.= (((Sum (sqr R19)) * (Sum (sqr R29))) + (- ((Sum (mlt (R19,R29))) ^2))) + (((Sum (sqr (x1 * R29))) + (Sum (sqr (x2 * R19)))) + (- (2 * (Sum (mlt ((x1 * R29),(x2 * R19))))))) by A12, A10
.= (((Sum (sqr R19)) * (Sum (sqr R29))) - ((Sum (mlt (R19,R29))) ^2)) + (Sum (sqr ((x1 * R29) - (x2 * R19)))) by A13, Th69 ;
then ((Sum (mlt (R1,R2))) ^2) + 0 <= (Sum (sqr R1)) * (Sum (sqr R2)) by A7, A11, XREAL_1:19;
hence (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; ::_thesis: verum
end;
A14: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch_2(A14, A1);
hence (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; ::_thesis: verum
end;
definition
let F be complex-valued FinSequence;
func Product F -> complex number means :Def13: :: RVSUM_1:def 13
ex f being FinSequence of COMPLEX st
( f = F & it = multcomplex $$ f );
existence
ex b1 being complex number ex f being FinSequence of COMPLEX st
( f = F & b1 = multcomplex $$ f )
proof
rng F c= COMPLEX by VALUED_0:def_1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4;
take multcomplex $$ f ; ::_thesis: ex f being FinSequence of COMPLEX st
( f = F & multcomplex $$ f = multcomplex $$ f )
thus ex f being FinSequence of COMPLEX st
( f = F & multcomplex $$ f = multcomplex $$ f ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being complex number st ex f being FinSequence of COMPLEX st
( f = F & b1 = multcomplex $$ f ) & ex f being FinSequence of COMPLEX st
( f = F & b2 = multcomplex $$ f ) holds
b1 = b2 ;
end;
:: deftheorem Def13 defines Product RVSUM_1:def_13_:_
for F being complex-valued FinSequence
for b2 being complex number holds
( b2 = Product F iff ex f being FinSequence of COMPLEX st
( f = F & b2 = multcomplex $$ f ) );
registration
let F be real-valued FinSequence;
cluster Product F -> complex real ;
coherence
Product F is real
proof
set mc = multcomplex ;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Product F = multcomplex $$ f by Def13;
set g = [#] (f,(the_unity_wrt multcomplex));
defpred S1[ Nat] means multcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt multcomplex)))) is real ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def_12;
([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real
proof
percases ( k + 1 in dom f or not k + 1 in dom f ) ;
suppose k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real
then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20;
hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real by A1; ::_thesis: verum
end;
suppose not k + 1 in dom f ; ::_thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real
hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real by BINOP_2:6, SETWOP_2:20; ::_thesis: verum
end;
end;
end;
then reconsider a = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1), b = multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex)))) as real number by A4;
not k + 1 in Seg k by FINSEQ_3:8;
then multcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt multcomplex)))) = multcomplex . ((multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex))))),(([#] (f,(the_unity_wrt multcomplex))) . (k + 1))) by SETWOP_2:2
.= b * a by BINOP_2:def_5 ;
hence S1[k + 1] by FINSEQ_1:9; ::_thesis: verum
end;
A5: ( multcomplex $$ f = multcomplex $$ ((findom f),([#] (f,(the_unity_wrt multcomplex)))) & ex n being Nat st dom f = Seg n ) by FINSEQ_1:def_2, SETWOP_2:def_2;
Seg 0 = {}. NAT ;
then A6: S1[ 0 ] by BINOP_2:6, SETWISEO:31;
for n being Nat holds S1[n] from NAT_1:sch_2(A6, A3);
hence Product F is real by A2, A5; ::_thesis: verum
end;
end;
theorem Th93: :: RVSUM_1:93
for F being FinSequence of REAL holds Product F = multreal $$ F
proof
set g = multreal ;
set h = multcomplex ;
let F be FinSequence of REAL ; ::_thesis: Product F = multreal $$ F
rng F c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def_4;
defpred S1[ Nat] means multreal $$ ((finSeg $1),([#] (F,(the_unity_wrt multreal)))) = multcomplex $$ ((finSeg $1),([#] (f,(the_unity_wrt multcomplex))));
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def_2;
A2: ( multreal $$ F = multreal $$ ((finSeg n),([#] (F,(the_unity_wrt multreal)))) & multcomplex $$ f = multcomplex $$ ((finSeg n),([#] (f,(the_unity_wrt multcomplex)))) ) by A1, SETWOP_2:def_2;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
set j = [#] (f,(the_unity_wrt multcomplex));
set i = [#] (F,(the_unity_wrt multreal));
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
A5: ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1)
proof
percases ( k + 1 in dom f or not k + 1 in dom f ) ;
supposeA6: k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1)
then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = F . (k + 1) by SETWOP_2:20
.= ([#] (F,(the_unity_wrt multreal))) . (k + 1) by A6, SETWOP_2:20 ;
hence ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) ; ::_thesis: verum
end;
supposeA7: not k + 1 in dom f ; ::_thesis: ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1)
then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = the_unity_wrt multcomplex by SETWOP_2:20
.= ([#] (F,(the_unity_wrt multreal))) . (k + 1) by A7, BINOP_2:6, BINOP_2:7, SETWOP_2:20 ;
hence ([#] (F,(the_unity_wrt multreal))) . (k + 1) = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) ; ::_thesis: verum
end;
end;
end;
A8: not k + 1 in Seg k by FINSEQ_3:8;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
multreal $$ ((finSeg (k + 1)),([#] (F,(the_unity_wrt multreal)))) = multreal $$ (((finSeg k) \/ {.(k + 1).}),([#] (F,(the_unity_wrt multreal)))) by FINSEQ_1:9
.= multreal . ((multreal $$ ((finSeg k),([#] (F,(the_unity_wrt multreal))))),(([#] (F,(the_unity_wrt multreal))) . (k + 1))) by A8, SETWOP_2:2
.= (multreal $$ ((finSeg k),([#] (F,(the_unity_wrt multreal))))) * (([#] (F,(the_unity_wrt multreal))) . (k + 1)) by BINOP_2:def_11
.= multcomplex . ((multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex))))),(([#] (f,(the_unity_wrt multcomplex))) . (k + 1))) by A4, A5, BINOP_2:def_5
.= multcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt multcomplex)))) by A8, SETWOP_2:2
.= multcomplex $$ ((finSeg (k + 1)),([#] (f,(the_unity_wrt multcomplex)))) by FINSEQ_1:9 ;
hence S1[k + 1] ; ::_thesis: verum
end;
A9: Seg 0 = {}. NAT ;
then multreal $$ ((finSeg 0),([#] (F,(the_unity_wrt multreal)))) = the_unity_wrt multcomplex by BINOP_2:6, BINOP_2:7, SETWISEO:31
.= multcomplex $$ ((finSeg 0),([#] (f,(the_unity_wrt multcomplex)))) by A9, SETWISEO:31 ;
then A10: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A10, A3);
then multreal $$ F = multcomplex $$ f by A2;
hence Product F = multreal $$ F by Def13; ::_thesis: verum
end;
definition
let F be FinSequence of COMPLEX ;
:: original: Product
redefine func Product F -> Element of COMPLEX equals :: RVSUM_1:def 14
multcomplex $$ F;
coherence
Product F is Element of COMPLEX by XCMPLX_0:def_2;
compatibility
for b1 being Element of COMPLEX holds
( b1 = Product F iff b1 = multcomplex $$ F ) by Def13;
end;
:: deftheorem defines Product RVSUM_1:def_14_:_
for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F;
definition
let F be FinSequence of REAL ;
:: original: Product
redefine func Product F -> Element of REAL equals :: RVSUM_1:def 15
multreal $$ F;
coherence
Product F is Element of REAL by XREAL_0:def_1;
compatibility
for b1 being Element of REAL holds
( b1 = Product F iff b1 = multreal $$ F ) by Th93;
end;
:: deftheorem defines Product RVSUM_1:def_15_:_
for F being FinSequence of REAL holds Product F = multreal $$ F;
Lm3: for F being empty FinSequence holds Product F = 1
proof
Product (<*> REAL) = 1 by BINOP_2:7, FINSOP_1:10;
hence for F being empty FinSequence holds Product F = 1 ; ::_thesis: verum
end;
theorem Th94: :: RVSUM_1:94
Product (<*> REAL) = 1 by Lm3;
registration
let r be complex number ;
cluster<*r*> -> complex-valued ;
coherence
<*r*> is complex-yielding
proof
reconsider p = r as Element of COMPLEX by XCMPLX_0:def_2;
reconsider f = <*p*> as FinSequence of COMPLEX ;
f is FinSequence-like ;
hence <*r*> is complex-yielding ; ::_thesis: verum
end;
end;
registration
let r1, r2 be complex number ;
cluster<*r1,r2*> -> complex-valued ;
coherence
<*r1,r2*> is complex-yielding
proof
reconsider p1 = r1, p2 = r2 as Element of COMPLEX by XCMPLX_0:def_2;
reconsider f = <*p1,p2*> as FinSequence of COMPLEX ;
f is FinSequence-like ;
hence <*r1,r2*> is complex-yielding ; ::_thesis: verum
end;
end;
registration
let r1, r2, r3 be complex number ;
cluster<*r1,r2,r3*> -> complex-valued ;
coherence
<*r1,r2,r3*> is complex-yielding
proof
reconsider p1 = r1, p2 = r2, p3 = r3 as Element of COMPLEX by XCMPLX_0:def_2;
reconsider f = <*p1,p2,p3*> as FinSequence of COMPLEX ;
f is FinSequence-like ;
hence <*r1,r2,r3*> is complex-yielding ; ::_thesis: verum
end;
end;
theorem Th95: :: RVSUM_1:95
for r being complex number holds Product <*r*> = r
proof
let r be complex number ; ::_thesis: Product <*r*> = r
reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def_2;
reconsider F = <*r9*> as FinSequence of COMPLEX ;
multcomplex $$ F = r by FINSOP_1:11;
hence Product <*r*> = r by Def13; ::_thesis: verum
end;
registration
let f, g be complex-valued FinSequence;
clusterf ^ g -> complex-valued ;
coherence
f ^ g is complex-yielding
proof
A1: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
( rng f c= COMPLEX & rng g c= COMPLEX ) by VALUED_0:def_1;
then rng (f ^ g) c= COMPLEX by A1, XBOOLE_1:8;
hence f ^ g is complex-yielding by VALUED_0:def_1; ::_thesis: verum
end;
end;
theorem Th96: :: RVSUM_1:96
for F being complex-valued FinSequence
for r being complex number holds Product (F ^ <*r*>) = (Product F) * r
proof
let F be complex-valued FinSequence; ::_thesis: for r being complex number holds Product (F ^ <*r*>) = (Product F) * r
let r be complex number ; ::_thesis: Product (F ^ <*r*>) = (Product F) * r
reconsider p = r as Element of COMPLEX by XCMPLX_0:def_2;
( rng F c= COMPLEX & rng (F ^ <*p*>) c= COMPLEX ) by VALUED_0:def_1;
then reconsider Fr = F ^ <*r*>, Ff = F as FinSequence of COMPLEX by FINSEQ_1:def_4;
thus Product (F ^ <*r*>) = multcomplex $$ Fr by Def13
.= multcomplex . ((Product Ff),p) by FINSOP_1:4
.= (Product F) * r by BINOP_2:def_5 ; ::_thesis: verum
end;
theorem Th97: :: RVSUM_1:97
for F1, F2 being complex-valued FinSequence holds Product (F1 ^ F2) = (Product F1) * (Product F2)
proof
let F1, F2 be complex-valued FinSequence; ::_thesis: Product (F1 ^ F2) = (Product F1) * (Product F2)
A1: rng (F1 ^ F2) c= COMPLEX by VALUED_0:def_1;
( rng F1 c= COMPLEX & rng F2 c= COMPLEX ) by VALUED_0:def_1;
then reconsider FF = F1 ^ F2, f1 = F1, f2 = F2 as FinSequence of COMPLEX by A1, FINSEQ_1:def_4;
thus Product (F1 ^ F2) = multcomplex $$ FF by Def13
.= multcomplex . ((Product f1),(Product f2)) by FINSOP_1:5
.= (Product F1) * (Product F2) by BINOP_2:def_5 ; ::_thesis: verum
end;
theorem :: RVSUM_1:98
for r being real number
for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F)
proof
let r be real number ; ::_thesis: for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F)
let F be real-valued FinSequence; ::_thesis: Product (<*r*> ^ F) = r * (Product F)
thus Product (<*r*> ^ F) = (Product <*r*>) * (Product F) by Th97
.= r * (Product F) by Th95 ; ::_thesis: verum
end;
theorem Th99: :: RVSUM_1:99
for r1, r2 being complex number holds Product <*r1,r2*> = r1 * r2
proof
let r1, r2 be complex number ; ::_thesis: Product <*r1,r2*> = r1 * r2
thus Product <*r1,r2*> = (Product <*r1*>) * r2 by Th96
.= r1 * r2 by Th95 ; ::_thesis: verum
end;
theorem :: RVSUM_1:100
for r1, r2, r3 being complex number holds Product <*r1,r2,r3*> = (r1 * r2) * r3
proof
let r1, r2, r3 be complex number ; ::_thesis: Product <*r1,r2,r3*> = (r1 * r2) * r3
thus Product <*r1,r2,r3*> = (Product <*r1,r2*>) * r3 by Th96
.= (r1 * r2) * r3 by Th99 ; ::_thesis: verum
end;
theorem :: RVSUM_1:101
for R being Element of 0 -tuples_on REAL holds Product R = 1 by Lm3;
theorem :: RVSUM_1:102
for i being Nat holds Product (i |-> 1) = 1
proof
let i be Nat; ::_thesis: Product (i |-> 1) = 1
Product (i |-> (the_unity_wrt multreal)) = the_unity_wrt multreal by SETWOP_2:25;
hence Product (i |-> 1) = 1 by BINOP_2:7; ::_thesis: verum
end;
Lm4: for p being complex-valued FinSequence st len p <> 0 holds
ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*>
proof
let p be complex-valued FinSequence; ::_thesis: ( len p <> 0 implies ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*> )
assume len p <> 0 ; ::_thesis: ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*>
then consider q being FinSequence, d being set such that
A1: p = q ^ <*d*> by CARD_1:27, FINSEQ_1:46;
rng p c= COMPLEX by VALUED_0:def_1;
then A2: p is FinSequence of COMPLEX by FINSEQ_1:def_4;
for i being Nat st i in dom q holds
q . i in COMPLEX
proof
let i be Nat; ::_thesis: ( i in dom q implies q . i in COMPLEX )
assume i in dom q ; ::_thesis: q . i in COMPLEX
then ( p . i = q . i & i in dom p ) by A1, FINSEQ_1:def_7, FINSEQ_2:15;
hence q . i in COMPLEX by A2, FINSEQ_2:11; ::_thesis: verum
end;
then A3: q is FinSequence of COMPLEX by FINSEQ_2:12;
len p = (len q) + 1 by A1, FINSEQ_2:16;
then p . (len p) = d by A1, FINSEQ_1:42;
hence ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*> by A1, A3; ::_thesis: verum
end;
theorem :: RVSUM_1:103
for F being complex-valued FinSequence holds
( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 )
proof
defpred S1[ Nat] means for F being complex-valued FinSequence st len F = $1 holds
( ex k being Nat st
( k in Seg $1 & F . k = 0 ) iff Product F = 0 );
let F be complex-valued FinSequence; ::_thesis: ( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 )
A1: Seg (len F) = dom F by FINSEQ_1:def_3;
A2: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A3: for F being complex-valued FinSequence st len F = i holds
( ex k being Nat st
( k in Seg i & F . k = 0 ) iff Product F = 0 ) ; ::_thesis: S1[i + 1]
let F be complex-valued FinSequence; ::_thesis: ( len F = i + 1 implies ( ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) iff Product F = 0 ) )
assume A4: len F = i + 1 ; ::_thesis: ( ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) iff Product F = 0 )
then consider F9 being complex-valued FinSequence, x being complex number such that
A5: F = F9 ^ <*x*> by Lm4;
A6: len F = (len F9) + 1 by A5, FINSEQ_2:16;
A7: Product F = (Product F9) * x by A5, Th96;
thus ( ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) implies Product F = 0 ) ::_thesis: ( Product F = 0 implies ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) )
proof
given k being Nat such that A8: k in Seg (i + 1) and
A9: F . k = 0 ; ::_thesis: Product F = 0
now__::_thesis:_Product_F_=_0
percases ( k in Seg i or k = i + 1 ) by A8, FINSEQ_2:7;
supposeA10: k in Seg i ; ::_thesis: Product F = 0
Seg (len F9) = dom F9 by FINSEQ_1:def_3;
then F9 . k = F . k by A4, A5, A6, A10, FINSEQ_1:def_7;
then Product F9 = 0 by A3, A4, A6, A9, A10;
hence Product F = 0 by A7; ::_thesis: verum
end;
suppose k = i + 1 ; ::_thesis: Product F = 0
then x = 0 by A4, A5, A6, A9, FINSEQ_1:42;
hence Product F = 0 by A7; ::_thesis: verum
end;
end;
end;
hence Product F = 0 ; ::_thesis: verum
end;
assume A11: Product F = 0 ; ::_thesis: ex k being Nat st
( k in Seg (i + 1) & F . k = 0 )
percases ( Product F9 = 0 or x = 0 ) by A7, A11;
suppose Product F9 = 0 ; ::_thesis: ex k being Nat st
( k in Seg (i + 1) & F . k = 0 )
then consider k being Nat such that
A12: k in Seg i and
A13: F9 . k = 0 by A3, A4, A6;
Seg (len F9) = dom F9 by FINSEQ_1:def_3;
then F . k = 0 by A4, A5, A6, A12, A13, FINSEQ_1:def_7;
hence ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) by A12, FINSEQ_2:8; ::_thesis: verum
end;
suppose x = 0 ; ::_thesis: ex k being Nat st
( k in Seg (i + 1) & F . k = 0 )
then F . (i + 1) = 0 by A4, A5, A6, FINSEQ_1:42;
hence ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) by FINSEQ_1:4; ::_thesis: verum
end;
end;
end;
A14: S1[ 0 ]
proof
let F be complex-valued FinSequence; ::_thesis: ( len F = 0 implies ( ex k being Nat st
( k in Seg 0 & F . k = 0 ) iff Product F = 0 ) )
assume len F = 0 ; ::_thesis: ( ex k being Nat st
( k in Seg 0 & F . k = 0 ) iff Product F = 0 )
then F = <*> COMPLEX ;
hence ( ex k being Nat st
( k in Seg 0 & F . k = 0 ) iff Product F = 0 ) by Th94; ::_thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch_2(A14, A2);
hence ( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 ) by A1; ::_thesis: verum
end;
theorem :: RVSUM_1:104
for i, j being Nat
for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))
proof
let i, j be Nat; ::_thesis: for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))
let r be real number ; ::_thesis: Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))
reconsider s = r as Element of REAL by XREAL_0:def_1;
Product ((i + j) |-> s) = multreal . ((multreal $$ (i |-> s)),(multreal $$ (j |-> s))) by SETWOP_2:26
.= (Product (i |-> s)) * (Product (j |-> s)) by BINOP_2:def_11 ;
hence Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r)) ; ::_thesis: verum
end;
theorem :: RVSUM_1:105
for i, j being Nat
for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))
proof
let i, j be Nat; ::_thesis: for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))
let r be real number ; ::_thesis: Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))
reconsider r = r as Element of REAL by XREAL_0:def_1;
Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) by SETWOP_2:27;
hence Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) ; ::_thesis: verum
end;
theorem :: RVSUM_1:106
for i being Nat
for r1, r2 being real number holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))
proof
let i be Nat; ::_thesis: for r1, r2 being real number holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))
let r1, r2 be real number ; ::_thesis: Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def_1;
Product (i |-> (s1 * s2)) = multreal $$ (i |-> (multreal . (s1,s2))) by BINOP_2:def_11
.= multreal . ((multreal $$ (i |-> s1)),(multreal $$ (i |-> s2))) by SETWOP_2:36
.= (Product (i |-> s1)) * (Product (i |-> s2)) by BINOP_2:def_11 ;
hence Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2)) ; ::_thesis: verum
end;
theorem Th107: :: RVSUM_1:107
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)
proof
let i be Nat; ::_thesis: for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)
let R1, R2 be Element of i -tuples_on REAL; ::_thesis: Product (mlt (R1,R2)) = (Product R1) * (Product R2)
thus Product (mlt (R1,R2)) = multreal . ((multreal $$ R1),(multreal $$ R2)) by SETWOP_2:35
.= (Product R1) * (Product R2) by BINOP_2:def_11 ; ::_thesis: verum
end;
theorem :: RVSUM_1:108
for i being Nat
for r being real number
for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)
proof
let i be Nat; ::_thesis: for r being real number
for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)
let r be real number ; ::_thesis: for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)
let R be Element of i -tuples_on REAL; ::_thesis: Product (r * R) = (Product (i |-> r)) * (Product R)
reconsider s = r as Element of REAL by XREAL_0:def_1;
thus Product (r * R) = Product (mlt ((i |-> s),R)) by Th63
.= (Product (i |-> r)) * (Product R) by Th107 ; ::_thesis: verum
end;
theorem :: RVSUM_1:109
for i being Nat
for R being Element of i -tuples_on REAL holds Product (sqr R) = (Product R) ^2 by Th107;
begin
theorem :: RVSUM_1:110
for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F ;
theorem :: RVSUM_1:111
for i, j being Nat
for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))
proof
let i, j be Nat; ::_thesis: for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))
let z be Element of COMPLEX ; ::_thesis: Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))
thus Product ((i + j) |-> z) = multcomplex . ((multcomplex $$ (i |-> z)),(multcomplex $$ (j |-> z))) by SETWOP_2:26
.= (Product (i |-> z)) * (Product (j |-> z)) by BINOP_2:def_5 ; ::_thesis: verum
end;
theorem :: RVSUM_1:112
for i, j being Nat
for z being Element of COMPLEX holds Product ((i * j) |-> z) = Product (j |-> (Product (i |-> z))) by SETWOP_2:27;
theorem :: RVSUM_1:113
for i being Nat
for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))
proof
let i be Nat; ::_thesis: for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))
let z1, z2 be Element of COMPLEX ; ::_thesis: Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))
thus Product (i |-> (z1 * z2)) = multcomplex $$ (i |-> (multcomplex . (z1,z2))) by BINOP_2:def_5
.= multcomplex . ((multcomplex $$ (i |-> z1)),(multcomplex $$ (i |-> z2))) by SETWOP_2:36
.= (Product (i |-> z1)) * (Product (i |-> z2)) by BINOP_2:def_5 ; ::_thesis: verum
end;
begin
theorem Th114: :: RVSUM_1:114
for x being real-valued FinSequence holds len (- x) = len x
proof
let x be real-valued FinSequence; ::_thesis: len (- x) = len x
dom (- x) = dom x by VALUED_1:8;
hence len (- x) = len x by FINSEQ_3:29; ::_thesis: verum
end;
theorem Th115: :: RVSUM_1:115
for x1, x2 being real-valued FinSequence st len x1 = len x2 holds
len (x1 + x2) = len x1
proof
let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies len (x1 + x2) = len x1 )
set n = len x1;
A1: x2 is FinSequence of REAL by Lm2;
x1 is FinSequence of REAL by Lm2;
then reconsider z1 = x1 as Element of (len x1) -tuples_on REAL by FINSEQ_2:92;
assume len x1 = len x2 ; ::_thesis: len (x1 + x2) = len x1
then reconsider z2 = x2 as Element of (len x1) -tuples_on REAL by A1, FINSEQ_2:92;
dom (z1 + z2) = Seg (len x1) by FINSEQ_2:124;
hence len (x1 + x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th116: :: RVSUM_1:116
for x1, x2 being real-valued FinSequence st len x1 = len x2 holds
len (x1 - x2) = len x1
proof
let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies len (x1 - x2) = len x1 )
set n = len x1;
A1: x2 is FinSequence of REAL by Lm2;
x1 is FinSequence of REAL by Lm2;
then reconsider z1 = x1 as Element of (len x1) -tuples_on REAL by FINSEQ_2:92;
assume len x1 = len x2 ; ::_thesis: len (x1 - x2) = len x1
then reconsider z2 = x2 as Element of (len x1) -tuples_on REAL by A1, FINSEQ_2:92;
dom (z1 - z2) = Seg (len x1) by FINSEQ_2:124;
hence len (x1 - x2) = len x1 by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th117: :: RVSUM_1:117
for a being real number
for x being real-valued FinSequence holds len (a * x) = len x
proof
let a be real number ; ::_thesis: for x being real-valued FinSequence holds len (a * x) = len x
let x be real-valued FinSequence; ::_thesis: len (a * x) = len x
set n = len x;
x is FinSequence of REAL by Lm2;
then reconsider z = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;
len (a * z) = len x by CARD_1:def_7;
hence len (a * x) = len x ; ::_thesis: verum
end;
theorem Th118: :: RVSUM_1:118
for x, y, z being real-valued FinSequence st len x = len y & len y = len z holds
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
proof
let x, y, z be real-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) )
A1: ( x is FinSequence of REAL & y is FinSequence of REAL & z is FinSequence of REAL ) by Lm2;
assume ( len x = len y & len y = len z ) ; ::_thesis: mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on REAL by A1, FINSEQ_2:92;
A2: dom (mlt ((x + y),z)) = Seg (len (mlt ((x2 + y2),z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ;
A3: dom (mlt (x,z)) = Seg (len (mlt (x2,z2))) by FINSEQ_1:def_3
.= Seg (len x) by CARD_1:def_7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def_7
.= dom ((mlt (x2,z2)) + (mlt (y2,z2))) by FINSEQ_1:def_3 ;
for i being Nat st i in dom (mlt ((x + y),z)) holds
(mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i
proof
let i be Nat; ::_thesis: ( i in dom (mlt ((x + y),z)) implies (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i )
assume A4: i in dom (mlt ((x + y),z)) ; ::_thesis: (mlt ((x + y),z)) . i = ((mlt (x,z)) + (mlt (y,z))) . i
set a = x . i;
set b = y . i;
set d = (x + y) . i;
set e = z . i;
len (x2 + y2) = len x by CARD_1:def_7;
then dom (x2 + y2) = Seg (len x) by FINSEQ_1:def_3
.= Seg (len (mlt (x2,z2))) by CARD_1:def_7
.= dom (mlt (x,z)) by FINSEQ_1:def_3 ;
then A5: (x + y) . i = (x . i) + (y . i) by A2, A3, A4, VALUED_1:def_1;
thus (mlt ((x + y),z)) . i = ((x + y) . i) * (z . i) by VALUED_1:5
.= ((x . i) * (z . i)) + ((y . i) * (z . i)) by A5
.= ((mlt (x,z)) . i) + ((y . i) * (z . i)) by VALUED_1:5
.= ((mlt (x,z)) . i) + ((mlt (y,z)) . i) by VALUED_1:5
.= ((mlt (x,z)) + (mlt (y,z))) . i by A2, A4, VALUED_1:def_1 ; ::_thesis: verum
end;
hence mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z)) by A2, FINSEQ_1:13; ::_thesis: verum
end;
begin
definition
let x1, x2 be real-valued FinSequence;
func|(x1,x2)| -> real number equals :: RVSUM_1:def 16
Sum (mlt (x1,x2));
correctness
coherence
Sum (mlt (x1,x2)) is real number ;
;
commutativity
for b1 being real number
for x1, x2 being real-valued FinSequence st b1 = Sum (mlt (x1,x2)) holds
b1 = Sum (mlt (x2,x1)) ;
end;
:: deftheorem defines |( RVSUM_1:def_16_:_
for x1, x2 being real-valued FinSequence holds |(x1,x2)| = Sum (mlt (x1,x2));
definition
let x1, x2 be real-valued FinSequence;
:: original: |(
redefine func|(x1,x2)| -> Element of REAL ;
correctness
coherence
|(x1,x2)| is Element of REAL ;
;
commutativity
for x1, x2 being real-valued FinSequence holds |(x1,x2)| = |(x2,x1)| ;
end;
theorem Th119: :: RVSUM_1:119
for x being real-valued FinSequence holds |(x,x)| >= 0
proof
let x be real-valued FinSequence; ::_thesis: |(x,x)| >= 0
set n = len x;
x is FinSequence of REAL by Lm2;
then reconsider w = x as Element of (len x) -tuples_on REAL by FINSEQ_2:92;
|(x,x)| = Sum (sqr w) ;
hence |(x,x)| >= 0 by Th86; ::_thesis: verum
end;
theorem Th120: :: RVSUM_1:120
for x, y, z being real-valued FinSequence st len x = len y & len y = len z holds
|((x + y),z)| = |(x,z)| + |(y,z)|
proof
let x, y, z be real-valued FinSequence; ::_thesis: ( len x = len y & len y = len z implies |((x + y),z)| = |(x,z)| + |(y,z)| )
A1: ( x is FinSequence of REAL & y is FinSequence of REAL & z is FinSequence of REAL ) by Lm2;
assume A2: ( len x = len y & len y = len z ) ; ::_thesis: |((x + y),z)| = |(x,z)| + |(y,z)|
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on REAL by A1, FINSEQ_2:92;
|((x + y),z)| = Sum ((mlt (x,z)) + (mlt (y,z))) by A2, Th118
.= (Sum (mlt (x2,z2))) + (Sum (mlt (y2,z2))) by Th89
.= |(x,z)| + |(y,z)| ;
hence |((x + y),z)| = |(x,z)| + |(y,z)| ; ::_thesis: verum
end;
theorem Th121: :: RVSUM_1:121
for x, y being real-valued FinSequence
for a being real number st len x = len y holds
|((a * x),y)| = a * |(x,y)|
proof
let x, y be real-valued FinSequence; ::_thesis: for a being real number st len x = len y holds
|((a * x),y)| = a * |(x,y)|
let a be real number ; ::_thesis: ( len x = len y implies |((a * x),y)| = a * |(x,y)| )
reconsider a2 = a as Element of REAL by XREAL_0:def_1;
A1: ( x is FinSequence of REAL & y is FinSequence of REAL ) by Lm2;
assume len x = len y ; ::_thesis: |((a * x),y)| = a * |(x,y)|
then reconsider x2 = x, y2 = y as Element of (len x) -tuples_on REAL by A1, FINSEQ_2:92;
|((a * x),y)| = Sum (a2 * (mlt (x2,y2))) by FINSEQOP:26
.= a * |(x,y)| by Th87 ;
hence |((a * x),y)| = a * |(x,y)| ; ::_thesis: verum
end;
theorem Th122: :: RVSUM_1:122
for x1, x2 being real-valued FinSequence st len x1 = len x2 holds
|((- x1),x2)| = - |(x1,x2)|
proof
let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies |((- x1),x2)| = - |(x1,x2)| )
assume len x1 = len x2 ; ::_thesis: |((- x1),x2)| = - |(x1,x2)|
then |((- x1),x2)| = (- 1) * |(x1,x2)| by Th121;
hence |((- x1),x2)| = - |(x1,x2)| ; ::_thesis: verum
end;
theorem :: RVSUM_1:123
for x1, x2 being real-valued FinSequence st len x1 = len x2 holds
|((- x1),(- x2))| = |(x1,x2)|
proof
let x1, x2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 implies |((- x1),(- x2))| = |(x1,x2)| )
assume A1: len x1 = len x2 ; ::_thesis: |((- x1),(- x2))| = |(x1,x2)|
then len (- x2) = len x1 by Th114;
then |((- x1),(- x2))| = - |(x1,(- x2))| by Th122
.= - (- |(x1,x2)|) by A1, Th122 ;
hence |((- x1),(- x2))| = |(x1,x2)| ; ::_thesis: verum
end;
theorem Th124: :: RVSUM_1:124
for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds
|((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
proof
let x1, x2, x3 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len x3 implies |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len x3 ; ::_thesis: |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
len (- x2) = len x2 by Th114;
then |((x1 - x2),x3)| = |(x1,x3)| + |((- x2),x3)| by A1, A2, Th120
.= |(x1,x3)| + (- |(x2,x3)|) by A2, Th122 ;
hence |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| ; ::_thesis: verum
end;
theorem :: RVSUM_1:125
for x, y being real number
for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds
|(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)
proof
let x, y be real number ; ::_thesis: for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds
|(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)
let x1, x2, x3 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len x3 implies |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) )
assume that
A1: len x1 = len x2 and
A2: len x2 = len x3 ; ::_thesis: |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)
( len (x * x1) = len x1 & len (y * x2) = len x2 ) by Th117;
then |(((x * x1) + (y * x2)),x3)| = |((x * x1),x3)| + |((y * x2),x3)| by A1, A2, Th120
.= (x * |(x1,x3)|) + |((y * x2),x3)| by A1, A2, Th121
.= (x * |(x1,x3)|) + (y * |(x2,x3)|) by A2, Th121 ;
hence |(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|) ; ::_thesis: verum
end;
theorem Th126: :: RVSUM_1:126
for x1, x2, y1, y2 being real-valued FinSequence st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
proof
let x1, x2, y1, y2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 implies |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len y1 and
A3: len y1 = len y2 ; ::_thesis: |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
|((x1 + x2),y2)| = |(x1,y2)| + |(x2,y2)| by A1, A2, A3, Th120;
then A4: |((x1 + x2),y1)| + |((x1 + x2),y2)| = (|(x1,y1)| + |(x2,y1)|) + (|(x1,y2)| + |(x2,y2)|) by A1, A2, Th120;
len (x1 + x2) = len x1 by A1, Th115;
hence |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| by A1, A2, A3, A4, Th120; ::_thesis: verum
end;
theorem Th127: :: RVSUM_1:127
for x1, x2, y1, y2 being real-valued FinSequence st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
proof
let x1, x2, y1, y2 be real-valued FinSequence; ::_thesis: ( len x1 = len x2 & len x2 = len y1 & len y1 = len y2 implies |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| )
assume that
A1: len x1 = len x2 and
A2: len x2 = len y1 and
A3: len y1 = len y2 ; ::_thesis: |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
|(x1,(y1 - y2))| = |(x1,y1)| - |(x1,y2)| by A1, A2, A3, Th124;
then A4: |(x1,(y1 - y2))| - |(x2,(y1 - y2))| = (|(x1,y1)| - |(x1,y2)|) - (|(x2,y1)| - |(x2,y2)|) by A2, A3, Th124;
len (y1 - y2) = len y1 by A3, Th116;
hence |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| by A1, A2, A4, Th124; ::_thesis: verum
end;
theorem :: RVSUM_1:128
for x, y being real-valued FinSequence st len x = len y holds
|((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| )
A1: (|(x,x)| + |(x,y)|) + |(x,y)| = |(x,x)| + (2 * |(x,y)|) ;
assume len x = len y ; ::_thesis: |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|
hence |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by A1, Th126; ::_thesis: verum
end;
theorem :: RVSUM_1:129
for x, y being real-valued FinSequence st len x = len y holds
|((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
proof
let x, y be real-valued FinSequence; ::_thesis: ( len x = len y implies |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| )
assume len x = len y ; ::_thesis: |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
then |((x - y),(x - y))| = ((|(x,x)| - |(x,y)|) - |(y,x)|) + |(y,y)| by Th127
.= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| ;
hence |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| ; ::_thesis: verum
end;
theorem Th130: :: RVSUM_1:130
for n being Nat
for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
proof
let n be Nat; ::_thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
let p1, p2, p3 be Element of n -tuples_on REAL; ::_thesis: |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
reconsider f1 = p1, f2 = p2, f3 = p3 as real-valued FinSequence ;
len f2 = n by CARD_1:def_7;
then ( len f1 = len f2 & len f2 = len f3 ) by CARD_1:def_7;
hence |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)| by Th120; ::_thesis: verum
end;
theorem Th131: :: RVSUM_1:131
for n being Nat
for p1, p2 being Element of n -tuples_on REAL
for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
proof
let n be Nat; ::_thesis: for p1, p2 being Element of n -tuples_on REAL
for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
let p1, p2 be Element of n -tuples_on REAL; ::_thesis: for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|
let x be real number ; ::_thesis: |((x * p1),p2)| = x * |(p1,p2)|
reconsider f1 = p1, f2 = p2 as real-valued FinSequence ;
( len f1 = n & len f2 = n ) by CARD_1:def_7;
hence |((x * p1),p2)| = x * |(p1,p2)| by Th121; ::_thesis: verum
end;
theorem Th132: :: RVSUM_1:132
for n being Nat
for p1, p2 being Element of n -tuples_on REAL holds |((- p1),p2)| = - |(p1,p2)|
proof
let n be Nat; ::_thesis: for p1, p2 being Element of n -tuples_on REAL holds |((- p1),p2)| = - |(p1,p2)|
let p1, p2 be Element of n -tuples_on REAL; ::_thesis: |((- p1),p2)| = - |(p1,p2)|
|((- p1),p2)| = |(((- 1) * p1),p2)|
.= (- 1) * |(p1,p2)| by Th131 ;
hence |((- p1),p2)| = - |(p1,p2)| ; ::_thesis: verum
end;
theorem :: RVSUM_1:133
for n being Nat
for p1, p2 being Element of n -tuples_on REAL holds |((- p1),(- p2))| = |(p1,p2)|
proof
let n be Nat; ::_thesis: for p1, p2 being Element of n -tuples_on REAL holds |((- p1),(- p2))| = |(p1,p2)|
let p1, p2 be Element of n -tuples_on REAL; ::_thesis: |((- p1),(- p2))| = |(p1,p2)|
|((- p1),(- p2))| = - |(p1,(- p2))| by Th132
.= - (- |(p1,p2)|) by Th132 ;
hence |((- p1),(- p2))| = |(p1,p2)| ; ::_thesis: verum
end;
theorem Th134: :: RVSUM_1:134
for n being Nat
for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
proof
let n be Nat; ::_thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
let p1, p2, p3 be Element of n -tuples_on REAL; ::_thesis: |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|
|((p1 - p2),p3)| = |(p1,p3)| + |((- p2),p3)| by Th130
.= |(p1,p3)| + (- |(p2,p3)|) by Th132 ;
hence |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)| ; ::_thesis: verum
end;
theorem :: RVSUM_1:135
for n being Nat
for x, y being real number
for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
proof
let n be Nat; ::_thesis: for x, y being real number
for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
let x, y be real number ; ::_thesis: for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
let p1, p2, p3 be Element of n -tuples_on REAL; ::_thesis: |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)
|(((x * p1) + (y * p2)),p3)| = |((x * p1),p3)| + |((y * p2),p3)| by Th130
.= (x * |(p1,p3)|) + |((y * p2),p3)| by Th131
.= (x * |(p1,p3)|) + (y * |(p2,p3)|) by Th131 ;
hence |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|) ; ::_thesis: verum
end;
theorem Th136: :: RVSUM_1:136
for n being Nat
for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
proof
let n be Nat; ::_thesis: for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
let p1, p2, q1, q2 be Element of n -tuples_on REAL; ::_thesis: |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|
A1: ( |((p1 + p2),q1)| = |(p1,q1)| + |(p2,q1)| & |((p1 + p2),q2)| = |(p1,q2)| + |(p2,q2)| ) by Th130;
|((p1 + p2),(q1 + q2))| = |((p1 + p2),q1)| + |((p1 + p2),q2)| by Th130
.= ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| by A1 ;
hence |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum
end;
theorem Th137: :: RVSUM_1:137
for n being Nat
for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
proof
let n be Nat; ::_thesis: for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
let p1, p2, q1, q2 be Element of n -tuples_on REAL; ::_thesis: |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|
A1: ( |(p1,(q1 - q2))| = |(p1,q1)| - |(p1,q2)| & |(p2,(q1 - q2))| = |(p2,q1)| - |(p2,q2)| ) by Th134;
|((p1 - p2),(q1 - q2))| = |(p1,(q1 - q2))| - |(p2,(q1 - q2))| by Th134
.= ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| by A1 ;
hence |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)| ; ::_thesis: verum
end;
theorem :: RVSUM_1:138
for n being Nat
for p, q being Element of n -tuples_on REAL holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
proof
let n be Nat; ::_thesis: for p, q being Element of n -tuples_on REAL holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
let p, q be Element of n -tuples_on REAL; ::_thesis: |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|
(|(p,p)| + |(p,q)|) + |(p,q)| = |(p,p)| + (2 * |(p,q)|) ;
hence |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)| by Th136; ::_thesis: verum
end;
theorem Th139: :: RVSUM_1:139
for n being Nat
for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
proof
let n be Nat; ::_thesis: for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
let p, q be Element of n -tuples_on REAL; ::_thesis: |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|
|((p - q),(p - q))| = ((|(p,p)| - |(p,q)|) - |(p,q)|) + |(q,q)| by Th137
.= (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ;
hence |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| ; ::_thesis: verum
end;
theorem :: RVSUM_1:140
for n being Nat
for p, q being Element of n -tuples_on REAL holds |(p,q)| <= |(p,p)| + |(q,q)|
proof
let n be Nat; ::_thesis: for p, q being Element of n -tuples_on REAL holds |(p,q)| <= |(p,p)| + |(q,q)|
let p, q be Element of n -tuples_on REAL; ::_thesis: |(p,q)| <= |(p,p)| + |(q,q)|
( 0 <= |(p,p)| & 0 <= |(q,q)| ) by Th119;
then A1: 0 / 2 <= (|(p,p)| + |(q,q)|) / 2 ;
|((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)| by Th139
.= (|(p,p)| + |(q,q)|) - (2 * |(p,q)|) ;
then 2 * |(p,q)| <= (|(p,p)| + |(q,q)|) - 0 by Th119, XREAL_1:11;
then (2 * |(p,q)|) / 2 <= (|(p,p)| + |(q,q)|) / 2 by XREAL_1:72;
then 0 + |(p,q)| <= ((|(p,p)| + |(q,q)|) / 2) + ((|(p,p)| + |(q,q)|) / 2) by A1, XREAL_1:7;
hence |(p,q)| <= |(p,p)| + |(q,q)| ; ::_thesis: verum
end;
definition
let p, q be real-valued FinSequence;
predp,q are_orthogonal means :Def17: :: RVSUM_1:def 17
|(p,q)| = 0 ;
symmetry
for p, q being real-valued FinSequence st |(p,q)| = 0 holds
|(q,p)| = 0 ;
end;
:: deftheorem Def17 defines are_orthogonal RVSUM_1:def_17_:_
for p, q being real-valued FinSequence holds
( p,q are_orthogonal iff |(p,q)| = 0 );
theorem :: RVSUM_1:141
for n being Nat
for a being real number
for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds
a * p,q are_orthogonal
proof
let n be Nat; ::_thesis: for a being real number
for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds
a * p,q are_orthogonal
let a be real number ; ::_thesis: for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds
a * p,q are_orthogonal
let p, q be Element of n -tuples_on REAL; ::_thesis: ( p,q are_orthogonal implies a * p,q are_orthogonal )
assume p,q are_orthogonal ; ::_thesis: a * p,q are_orthogonal
then |(p,q)| = 0 by Def17;
then a * |(p,q)| = 0 ;
then |((a * p),q)| = 0 by Th131;
hence a * p,q are_orthogonal by Def17; ::_thesis: verum
end;
theorem :: RVSUM_1:142
for r1, r2, r3, r4 being real number holds Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4
proof
let r1, r2, r3, r4 be real number ; ::_thesis: Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4
thus Sum <*r1,r2,r3,r4*> = (Sum <*r1,r2,r3*>) + r4 by Th74
.= ((r1 + r2) + r3) + r4 by Th78 ; ::_thesis: verum
end;
theorem Th143: :: RVSUM_1:143
for f being FinSequence of REAL holds
( len f = len (sqr f) & dom f = dom (sqr f) )
proof
let f be FinSequence of REAL ; ::_thesis: ( len f = len (sqr f) & dom f = dom (sqr f) )
( rng f c= REAL & dom sqrreal = REAL ) by FUNCT_2:def_1;
hence len f = len (sqrreal * f) by FINSEQ_2:29
.= len (sqr f) ;
::_thesis: dom f = dom (sqr f)
hence dom f = dom (sqr f) by FINSEQ_3:29; ::_thesis: verum
end;
theorem :: RVSUM_1:144
for f, g being FinSequence of REAL holds sqr (f ^ g) = (sqr f) ^ (sqr g)
proof
let f, g be FinSequence of REAL ; ::_thesis: sqr (f ^ g) = (sqr f) ^ (sqr g)
A1: len f = len (sqr f) by Th143;
A2: len (sqr (f ^ g)) = len (f ^ g) by Th143;
A3: ( len g = len (sqr g) & len (f ^ g) = (len f) + (len g) ) by Th143, FINSEQ_1:22;
A4: for i being Nat st 1 <= i & i <= len (sqr (f ^ g)) holds
(sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len (sqr (f ^ g)) implies (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i )
assume that
A5: 1 <= i and
A6: i <= len (sqr (f ^ g)) ; ::_thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i
A7: i in dom (f ^ g) by A2, A5, A6, FINSEQ_3:25;
percases ( i in dom f or not i in dom f ) ;
supposeA8: i in dom f ; ::_thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i
then A9: i in dom (sqr f) by Th143;
thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i
.= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= sqrreal . (f . i) by A8, FINSEQ_1:def_7
.= (f . i) ^2 by Def2
.= (sqr f) . i by VALUED_1:11
.= ((sqr f) ^ (sqr g)) . i by A9, FINSEQ_1:def_7 ; ::_thesis: verum
end;
suppose not i in dom f ; ::_thesis: (sqr (f ^ g)) . i = ((sqr f) ^ (sqr g)) . i
then A10: len f < i by A5, FINSEQ_3:25;
then reconsider j = i - (len f) as Element of NAT by INT_1:5;
A11: i <= len (f ^ g) by A6, Th143;
A12: i <= len ((sqr f) ^ (sqr g)) by A1, A3, A2, A6, FINSEQ_1:22;
thus (sqr (f ^ g)) . i = (sqrreal * (f ^ g)) . i
.= sqrreal . ((f ^ g) . i) by A7, FUNCT_1:13
.= sqrreal . (g . j) by A10, A11, FINSEQ_1:24
.= (g . j) ^2 by Def2
.= (sqr g) . j by VALUED_1:11
.= ((sqr f) ^ (sqr g)) . i by A1, A10, A12, FINSEQ_1:24 ; ::_thesis: verum
end;
end;
end;
len (sqr (f ^ g)) = len ((sqr f) ^ (sqr g)) by A1, A3, A2, FINSEQ_1:22;
hence sqr (f ^ g) = (sqr f) ^ (sqr g) by A4, FINSEQ_1:14; ::_thesis: verum
end;
theorem :: RVSUM_1:145
for F being real-valued FinSequence holds F is FinSequence of REAL
proof
let F be real-valued FinSequence; ::_thesis: F is FinSequence of REAL
thus rng F c= REAL ; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;