let a, b, c be Complex; ( a <> b & a <> c & b <> c & angle (a,b,c) = 0 & not ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) implies ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
assume that
A1:
a <> b
and
A2:
a <> c
and
A3:
b <> c
and
A4:
angle (a,b,c) = 0
; ( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )
per cases
( angle (b,c,a) <> 0 or angle (c,a,b) <> 0 )
by A1, A2, A3, A4, Th81;
suppose A5:
angle (
b,
c,
a)
<> 0
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )A6:
0 <= angle (
b,
c,
a)
by Th68;
thus
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
verumproof
per cases
( angle (b,c,a) < PI or angle (b,c,a) = PI or angle (b,c,a) > PI )
by XXREAL_0:1;
suppose
angle (
b,
c,
a)
< PI
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )hence
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
by A2, A3, A4, A5, A6, Th82;
verum end; suppose
angle (
b,
c,
a)
= PI
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )hence
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
by A2, A3, Th84;
verum end; suppose
angle (
b,
c,
a)
> PI
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )hence
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
by A2, A3, A4, Th83, COMPTRIG:5;
verum end; end;
end; end; suppose A7:
angle (
c,
a,
b)
<> 0
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )A8:
0 <= angle (
c,
a,
b)
by Th68;
thus
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
verumproof
per cases
( angle (c,a,b) < PI or angle (c,a,b) = PI or angle (c,a,b) > PI )
by XXREAL_0:1;
suppose
angle (
c,
a,
b)
< PI
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )hence
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
by A1, A2, A4, A7, A8, Th82;
verum end; suppose
angle (
c,
a,
b)
= PI
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )hence
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
by A1, A2, Th84;
verum end; suppose
angle (
c,
a,
b)
> PI
;
( ( angle (b,c,a) = 0 & angle (c,a,b) = PI ) or ( angle (b,c,a) = PI & angle (c,a,b) = 0 ) )hence
( (
angle (
b,
c,
a)
= 0 &
angle (
c,
a,
b)
= PI ) or (
angle (
b,
c,
a)
= PI &
angle (
c,
a,
b)
= 0 ) )
by A1, A2, A4, Th83, COMPTRIG:5;
verum end; end;
end; end; end;