Metamath Proof Explorer

Theorem endofsegid

Description: If A , B , and C fall in order on a line, and A B and A C are congruent, then C = B . (Contributed by Scott Fenton, 7-Oct-2013)

Ref Expression
Assertion endofsegid 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. A , B >. ) -> C = B ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> N e. NN )
2 simpr1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
3 simpr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
4 simpr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
5 cgrcom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. A , B >. <-> <. A , B >. Cgr <. A , C >. ) )
6 1 2 3 2 4 5 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. A , B >. <-> <. A , B >. Cgr <. A , C >. ) )
7 6 biimpd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. A , B >. -> <. A , B >. Cgr <. A , C >. ) )
8 idd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. A , B >. -> <. A , C >. Cgr <. A , B >. ) )
9 axcgrrflx 
 |-  ( ( N e. NN /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> <. B , C >. Cgr <. C , B >. )
10 9 3adant3r1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. B , C >. Cgr <. C , B >. )
11 10 a1d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. A , B >. -> <. B , C >. Cgr <. C , B >. ) )
12 7 8 11 3jcad 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. A , B >. -> ( <. A , B >. Cgr <. A , C >. /\ <. A , C >. Cgr <. A , B >. /\ <. B , C >. Cgr <. C , B >. ) ) )
13 3ancomb 
 |-  ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ B e. ( EE ` N ) ) <-> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
14 brcgr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. A , <. C , B >. >. <-> ( <. A , B >. Cgr <. A , C >. /\ <. A , C >. Cgr <. A , B >. /\ <. B , C >. Cgr <. C , B >. ) ) )
15 13 14 syl3an3br 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. A , <. C , B >. >. <-> ( <. A , B >. Cgr <. A , C >. /\ <. A , C >. Cgr <. A , B >. /\ <. B , C >. Cgr <. C , B >. ) ) )
16 15 3anidm23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. A , <. C , B >. >. <-> ( <. A , B >. Cgr <. A , C >. /\ <. A , C >. Cgr <. A , B >. /\ <. B , C >. Cgr <. C , B >. ) ) )
17 12 16 sylibrd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , C >. Cgr <. A , B >. -> <. A , <. B , C >. >. Cgr3 <. A , <. C , B >. >. ) )
18 btwnxfr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. C , B >. >. ) -> C Btwn <. A , B >. ) )
19 13 18 syl3an3br 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. C , B >. >. ) -> C Btwn <. A , B >. ) )
20 19 3anidm23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , <. B , C >. >. Cgr3 <. A , <. C , B >. >. ) -> C Btwn <. A , B >. ) )
21 17 20 sylan2d 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. A , B >. ) -> C Btwn <. A , B >. ) )
22 simpl 
 |-  ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. A , B >. ) -> B Btwn <. A , C >. )
23 22 a1i 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. A , B >. ) -> B Btwn <. A , C >. ) )
24 21 23 jcad 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. A , B >. ) -> ( C Btwn <. A , B >. /\ B Btwn <. A , C >. ) ) )
25 3anrot 
 |-  ( ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) <-> ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
26 btwnswapid2 
 |-  ( ( N e. NN /\ ( C e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ B Btwn <. A , C >. ) -> C = B ) )
27 25 26 sylan2br 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( C Btwn <. A , B >. /\ B Btwn <. A , C >. ) -> C = B ) )
28 24 27 syld 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( B Btwn <. A , C >. /\ <. A , C >. Cgr <. A , B >. ) -> C = B ) )