Metamath Proof Explorer

Theorem fscgr

Description: Congruence law for the general five segment configuration. Theorem 4.16 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion fscgr 
|- ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. A , B >. , <. C , D >. >. FiveSeg <. <. E , F >. , <. G , H >. >. /\ A =/= B ) -> <. C , D >. Cgr <. G , H >. ) )

Proof

Step Hyp Ref Expression
1 brfs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. FiveSeg <. <. E , F >. , <. G , H >. >. <-> ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
2 1 anbi1d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. A , B >. , <. C , D >. >. FiveSeg <. <. E , F >. , <. G , H >. >. /\ A =/= B ) <-> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) /\ A =/= B ) ) )
3 simp11 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> N e. NN )
4 simp12 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
5 simp13 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
6 simp21 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
7 brcolinear 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
8 3 4 5 6 7 syl13anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. <-> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) ) )
9 simp23 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
10 simp31 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
11 simp32 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> G e. ( EE ` N ) )
12 cgr3permute2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. <-> <. B , <. A , C >. >. Cgr3 <. F , <. E , G >. >. ) )
13 3 4 5 6 9 10 11 12 syl133anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. <-> <. B , <. A , C >. >. Cgr3 <. F , <. E , G >. >. ) )
14 ancom 
 |-  ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) <-> ( <. B , D >. Cgr <. F , H >. /\ <. A , D >. Cgr <. E , H >. ) )
15 14 a1i 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) <-> ( <. B , D >. Cgr <. F , H >. /\ <. A , D >. Cgr <. E , H >. ) ) )
16 13 15 3anbi23d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) <-> ( A Btwn <. B , C >. /\ <. B , <. A , C >. >. Cgr3 <. F , <. E , G >. >. /\ ( <. B , D >. Cgr <. F , H >. /\ <. A , D >. Cgr <. E , H >. ) ) ) )
17 simp22 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
18 simp33 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> H e. ( EE ` N ) )
19 brofs2 
 |-  ( ( ( N e. NN /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. B , A >. , <. C , D >. >. OuterFiveSeg <. <. F , E >. , <. G , H >. >. <-> ( A Btwn <. B , C >. /\ <. B , <. A , C >. >. Cgr3 <. F , <. E , G >. >. /\ ( <. B , D >. Cgr <. F , H >. /\ <. A , D >. Cgr <. E , H >. ) ) ) )
20 3 5 4 6 17 10 9 11 18 19 syl333anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. B , A >. , <. C , D >. >. OuterFiveSeg <. <. F , E >. , <. G , H >. >. <-> ( A Btwn <. B , C >. /\ <. B , <. A , C >. >. Cgr3 <. F , <. E , G >. >. /\ ( <. B , D >. Cgr <. F , H >. /\ <. A , D >. Cgr <. E , H >. ) ) ) )
21 16 20 bitr4d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) <-> <. <. B , A >. , <. C , D >. >. OuterFiveSeg <. <. F , E >. , <. G , H >. >. ) )
22 necom 
 |-  ( A =/= B <-> B =/= A )
23 22 a1i 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( A =/= B <-> B =/= A ) )
24 21 23 anbi12d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( A Btwn <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) /\ A =/= B ) <-> ( <. <. B , A >. , <. C , D >. >. OuterFiveSeg <. <. F , E >. , <. G , H >. >. /\ B =/= A ) ) )
25 5segofs 
 |-  ( ( ( N e. NN /\ B e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ F e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. B , A >. , <. C , D >. >. OuterFiveSeg <. <. F , E >. , <. G , H >. >. /\ B =/= A ) -> <. C , D >. Cgr <. G , H >. ) )
26 3 5 4 6 17 10 9 11 18 25 syl333anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. B , A >. , <. C , D >. >. OuterFiveSeg <. <. F , E >. , <. G , H >. >. /\ B =/= A ) -> <. C , D >. Cgr <. G , H >. ) )
27 24 26 sylbid 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( A Btwn <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) /\ A =/= B ) -> <. C , D >. Cgr <. G , H >. ) )
28 27 expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) )
29 28 3expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( A Btwn <. B , C >. -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. -> ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) ) ) )
30 btwncom 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( B Btwn <. C , A >. <-> B Btwn <. A , C >. ) )
31 3 5 6 4 30 syl13anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( B Btwn <. C , A >. <-> B Btwn <. A , C >. ) )
32 31 3anbi1d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( B Btwn <. C , A >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) <-> ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
33 brofs2 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. <-> ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
34 32 33 bitr4d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( B Btwn <. C , A >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) <-> <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. ) )
35 34 anbi1d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , A >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) /\ A =/= B ) <-> ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. /\ A =/= B ) ) )
36 5segofs 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. A , B >. , <. C , D >. >. OuterFiveSeg <. <. E , F >. , <. G , H >. >. /\ A =/= B ) -> <. C , D >. Cgr <. G , H >. ) )
37 35 36 sylbid 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( B Btwn <. C , A >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) /\ A =/= B ) -> <. C , D >. Cgr <. G , H >. ) )
38 37 expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( B Btwn <. C , A >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) )
39 38 3expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( B Btwn <. C , A >. -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. -> ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) ) ) )
40 cgr3permute1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) /\ G e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. <-> <. A , <. C , B >. >. Cgr3 <. E , <. G , F >. >. ) )
41 3 4 5 6 9 10 11 40 syl133anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. <-> <. A , <. C , B >. >. Cgr3 <. E , <. G , F >. >. ) )
42 41 3anbi2d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) <-> ( C Btwn <. A , B >. /\ <. A , <. C , B >. >. Cgr3 <. E , <. G , F >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
43 brifs2 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ F e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. B , D >. >. InnerFiveSeg <. <. E , G >. , <. F , H >. >. <-> ( C Btwn <. A , B >. /\ <. A , <. C , B >. >. Cgr3 <. E , <. G , F >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
44 3 4 6 5 17 9 11 10 18 43 syl333anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. B , D >. >. InnerFiveSeg <. <. E , G >. , <. F , H >. >. <-> ( C Btwn <. A , B >. /\ <. A , <. C , B >. >. Cgr3 <. E , <. G , F >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) ) )
45 42 44 bitr4d 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) <-> <. <. A , C >. , <. B , D >. >. InnerFiveSeg <. <. E , G >. , <. F , H >. >. ) )
46 ifscgr 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( G e. ( EE ` N ) /\ F e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. B , D >. >. InnerFiveSeg <. <. E , G >. , <. F , H >. >. -> <. C , D >. Cgr <. G , H >. ) )
47 3 4 6 5 17 9 11 10 18 46 syl333anc 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( <. <. A , C >. , <. B , D >. >. InnerFiveSeg <. <. E , G >. , <. F , H >. >. -> <. C , D >. Cgr <. G , H >. ) )
48 45 47 sylbid 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) -> <. C , D >. Cgr <. G , H >. ) )
49 48 a1dd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) )
50 49 3expd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. -> ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) ) ) )
51 29 39 50 3jaod 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. -> ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) ) ) )
52 8 51 sylbid 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( A Colinear <. B , C >. -> ( <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. -> ( ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) ) ) )
53 52 3impd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) -> ( A =/= B -> <. C , D >. Cgr <. G , H >. ) ) )
54 53 impd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( ( A Colinear <. B , C >. /\ <. A , <. B , C >. >. Cgr3 <. E , <. F , G >. >. /\ ( <. A , D >. Cgr <. E , H >. /\ <. B , D >. Cgr <. F , H >. ) ) /\ A =/= B ) -> <. C , D >. Cgr <. G , H >. ) )
55 2 54 sylbid 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) /\ E e. ( EE ` N ) ) /\ ( F e. ( EE ` N ) /\ G e. ( EE ` N ) /\ H e. ( EE ` N ) ) ) -> ( ( <. <. A , B >. , <. C , D >. >. FiveSeg <. <. E , F >. , <. G , H >. >. /\ A =/= B ) -> <. C , D >. Cgr <. G , H >. ) )