let a, b, c, d, e, f be Element of F_Real; :: thesis: ( ( qfconic (a,b,c,d,e,f,|[1,0,0]|) = 0 implies a = 0 ) & ( qfconic (a,b,c,d,e,f,|[0,1,0]|) = 0 implies b = 0 ) & ( qfconic (a,b,c,d,e,f,|[0,0,1]|) = 0 implies c = 0 ) & ( qfconic (0,0,0,d,e,f,|[1,1,1]|) = 0 implies (d + e) + f = 0 ) )
hereby :: thesis: ( ( qfconic (a,b,c,d,e,f,|[0,1,0]|) = 0 implies b = 0 ) & ( qfconic (a,b,c,d,e,f,|[0,0,1]|) = 0 implies c = 0 ) & ( qfconic (0,0,0,d,e,f,|[1,1,1]|) = 0 implies (d + e) + f = 0 ) )
assume A1: qfconic (a,b,c,d,e,f,|[1,0,0]|) = 0 ; :: thesis: a = 0
( |[1,0,0]| . 1 = |[1,0,0]| `1 & |[1,0,0]| . 2 = |[1,0,0]| `2 & |[1,0,0]| . 3 = |[1,0,0]| `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then ( |[1,0,0]| . 1 = 1 & |[1,0,0]| . 2 = 0 & |[1,0,0]| . 3 = 0 ) by EUCLID_5:2;
hence a = 0 by A1; :: thesis: verum
end;
hereby :: thesis: ( ( qfconic (a,b,c,d,e,f,|[0,0,1]|) = 0 implies c = 0 ) & ( qfconic (0,0,0,d,e,f,|[1,1,1]|) = 0 implies (d + e) + f = 0 ) )
assume A2: qfconic (a,b,c,d,e,f,|[0,1,0]|) = 0 ; :: thesis: b = 0
( |[0,1,0]| . 1 = |[0,1,0]| `1 & |[0,1,0]| . 2 = |[0,1,0]| `2 & |[0,1,0]| . 3 = |[0,1,0]| `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then ( |[0,1,0]| . 1 = 0 & |[0,1,0]| . 2 = 1 & |[0,1,0]| . 3 = 0 ) by EUCLID_5:2;
hence b = 0 by A2; :: thesis: verum
end;
hereby :: thesis: ( qfconic (0,0,0,d,e,f,|[1,1,1]|) = 0 implies (d + e) + f = 0 )
assume A3: qfconic (a,b,c,d,e,f,|[0,0,1]|) = 0 ; :: thesis: c = 0
( |[0,0,1]| . 1 = |[0,0,1]| `1 & |[0,0,1]| . 2 = |[0,0,1]| `2 & |[0,0,1]| . 3 = |[0,0,1]| `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then ( |[0,0,1]| . 1 = 0 & |[0,0,1]| . 2 = 0 & |[0,0,1]| . 3 = 1 ) by EUCLID_5:2;
hence c = 0 by A3; :: thesis: verum
end;
hereby :: thesis: verum
assume A4: qfconic (0,0,0,d,e,f,|[1,1,1]|) = 0 ; :: thesis: (d + e) + f = 0
( |[1,1,1]| . 1 = |[1,1,1]| `1 & |[1,1,1]| . 2 = |[1,1,1]| `2 & |[1,1,1]| . 3 = |[1,1,1]| `3 ) by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;
then ( |[1,1,1]| . 1 = 1 & |[1,1,1]| . 2 = 1 & |[1,1,1]| . 3 = 1 ) by EUCLID_5:2;
hence (d + e) + f = 0 by A4; :: thesis: verum
end;