let i be natural Number ; :: 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))
A0: i is Nat by TARSKI:1;
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 c being Nat st S1[c] holds
S1[c + 1]
proof
let c be Nat; :: thesis: ( S1[c] implies S1[c + 1] )
assume A2: for R1, R2 being Element of c -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2)) ; :: thesis: S1[c + 1]
let R1, R2 be Element of (c + 1) -tuples_on REAL; :: thesis: (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))
consider R19 being Element of c -tuples_on REAL, x1 being Element of REAL such that
A3: R1 = R19 ^ <*x1*> by FINSEQ_2:117;
consider R29 being Element of c -tuples_on REAL, x2 being Element of REAL such that
A4: R2 = R29 ^ <*x2*> by FINSEQ_2:117;
A5: for r being Real
for R being Element of c -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2)
proof
let r be Real; :: thesis: for R being Element of c -tuples_on REAL holds Sum (sqr (R ^ <*r*>)) = (Sum (sqr R)) + (r ^2)
let R be Element of c -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 (R29 ^ <*x2*>))
.= 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)) by A0; :: thesis: verum