let a1, a2, a3 be Real; :: thesis: for n being Element of NAT
for x, x1, x2, x3 being Element of REAL n st x in plane x1,x2,x3 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds
0* n in plane x1,x2,x3
let n be Element of NAT ; :: thesis: for x, x1, x2, x3 being Element of REAL n st x in plane x1,x2,x3 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 holds
0* n in plane x1,x2,x3
let x, x1, x2, x3 be Element of REAL n; :: thesis: ( x in plane x1,x2,x3 & x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) & not (a1 + a2) + a3 = 1 implies 0* n in plane x1,x2,x3 )
assume that
A1: x in plane x1,x2,x3 and
A2: x = ((a1 * x1) + (a2 * x2)) + (a3 * x3) and
A3: not (a1 + a2) + a3 = 1 ; :: thesis: 0* n in plane x1,x2,x3
ex x9 being Element of REAL n st
( x = x9 & ex a19, a29, a39 being Real st
( (a19 + a29) + a39 = 1 & x9 = ((a19 * x1) + (a29 * x2)) + (a39 * x3) ) ) by A1;
then consider a19, a29, a39 being Real such that
A4: (a19 + a29) + a39 = 1 and
A5: x = ((a19 * x1) + (a29 * x2)) + (a39 * x3) ;
A6: ((a1 - a19) + (a2 - a29)) + (a3 - a39) <> 0 by A3, A4;
set t = ((a1 - a19) + (a2 - a29)) + (a3 - a39);
A7: (((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) + ((a2 - a29) / (((a1 - a19) + (a2 - a29)) + (a3 - a39)))) + ((a3 - a39) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) = (((a1 - a19) + (a2 - a29)) + (a3 - a39)) / (((a1 - a19) + (a2 - a29)) + (a3 - a39)) by XCMPLX_1:64
.= 1 by A6, XCMPLX_1:60 ;
A8: 0* n = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((a19 * x1) + (a29 * x2)) + (a39 * x3)) by A2, A5, Th7
.= (((a1 - a19) * x1) + ((a2 - a29) * x2)) + ((a3 - a39) * x3) by Th31 ;
0* n = (1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (0* n) by EUCLID_4:2
.= ((((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a1 - a19)) * x1) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a2 - a29)) * x2)) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a3 - a39)) * x3) by A8, Th27
.= ((((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x1) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a2 - a29)) * x2)) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a3 - a39)) * x3) by XCMPLX_1:100
.= ((((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x1) + (((a2 - a29) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x2)) + (((1 / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * (a3 - a39)) * x3) by XCMPLX_1:100
.= ((((a1 - a19) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x1) + (((a2 - a29) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x2)) + (((a3 - a39) / (((a1 - a19) + (a2 - a29)) + (a3 - a39))) * x3) by XCMPLX_1:100 ;
hence 0* n in plane x1,x2,x3 by A7; :: thesis: verum