let a, b, c, d, e, f be Element of F_Real; ( ( 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 ( ( 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
;
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;
verum
end;
hereby ( ( 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
;
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;
verum
end;
hereby ( 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
;
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;
verum
end;
hereby verum
assume A4:
qfconic (
0,
0,
0,
d,
e,
f,
|[1,1,1]|)
= 0
;
(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;
verum
end;