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 x' being Element of REAL n st
( x = x' & ex a1', a2', a3' being Real st
( (a1' + a2') + a3' = 1 & x' = ((a1' * x1) + (a2' * x2)) + (a3' * x3) ) ) by A1;
then consider a1', a2', a3' being Real such that
A4: (a1' + a2') + a3' = 1 and
A5: x = ((a1' * x1) + (a2' * x2)) + (a3' * x3) ;
A6: ((a1 - a1') + (a2 - a2')) + (a3 - a3') <> 0 by A3, A4;
set t = ((a1 - a1') + (a2 - a2')) + (a3 - a3');
A7: (((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) + ((a2 - a2') / (((a1 - a1') + (a2 - a2')) + (a3 - a3')))) + ((a3 - a3') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) = (((a1 - a1') + (a2 - a2')) + (a3 - a3')) / (((a1 - a1') + (a2 - a2')) + (a3 - a3')) by XCMPLX_1:64
.= 1 by A6, XCMPLX_1:60 ;
A8: 0* n = (((a1 * x1) + (a2 * x2)) + (a3 * x3)) - (((a1' * x1) + (a2' * x2)) + (a3' * x3)) by A2, A5, Th7
.= (((a1 - a1') * x1) + ((a2 - a2') * x2)) + ((a3 - a3') * x3) by Th31 ;
0* n = (1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (0* n) by EUCLID_4:2
.= ((((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a1 - a1')) * x1) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a2 - a2')) * x2)) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a3 - a3')) * x3) by A8, Th27
.= ((((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x1) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a2 - a2')) * x2)) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a3 - a3')) * x3) by XCMPLX_1:100
.= ((((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x1) + (((a2 - a2') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x2)) + (((1 / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * (a3 - a3')) * x3) by XCMPLX_1:100
.= ((((a1 - a1') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x1) + (((a2 - a2') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x2)) + (((a3 - a3') / (((a1 - a1') + (a2 - a2')) + (a3 - a3'))) * x3) by XCMPLX_1:100 ;
hence 0* n in plane x1,x2,x3 by A7; :: thesis: verum