let u, v, w be non zero Element of (TOP-REAL 3); ( u `1 <> 0 & u `3 = 1 & v `1 = - (u `2) & v `2 = u `1 & v `3 = 0 & w `3 = 1 & |{u,v,w}| = 0 & 1 < ((u `1) ^2) + ((u `2) ^2) implies ((w `1) ^2) + ((w `2) ^2) <> 1 )
assume that
A0:
u `1 <> 0
and
A1:
u `3 = 1
and
A2:
v `1 = - (u `2)
and
A3:
v `2 = u `1
and
A4:
v `3 = 0
and
A5:
w `3 = 1
and
A6:
|{u,v,w}| = 0
and
A7:
1 < ((u `1) ^2) + ((u `2) ^2)
; ((w `1) ^2) + ((w `2) ^2) <> 1
A8:
((((u `1) ^2) + ((u `2) ^2)) - ((u `1) * (w `1))) - ((u `2) * (w `2)) = 0
by A1, A2, A3, A4, A5, A6, Th21;
assume A9:
((w `1) ^2) + ((w `2) ^2) = 1
; contradiction
reconsider x = w `1 , y = w `2 as Real ;
reconsider u1 = u `1 as non zero Real by A0;
reconsider r = sqrt (((u `1) ^2) + ((u `2) ^2)) as positive Real by A0, Th02;
reconsider u2 = u `2 as Real ;
A10:
r ^2 = ((u `1) ^2) + ((u `2) ^2)
by SQUARE_1:def 2;
then
u1 * x = (r ^2) - (u2 * y)
by A8;
then
(((((r ^2) ^2) / (u1 ^2)) - ((2 * (((r ^2) * u2) / (u1 * u1))) * y)) + (((u2 ^2) / (u1 ^2)) * (y ^2))) + (y ^2) = 1
by A9, Th03;
hence
contradiction
by A10, A7, Th09; verum