Metamath Proof Explorer

Theorem colineartriv1

Description: Trivial case of colinearity. Theorem 4.12 of Schwabhauser p. 37. (Contributed by Scott Fenton, 5-Oct-2013)

Ref Expression
Assertion colineartriv1 
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A Colinear <. A , B >. )

Proof

Step Hyp Ref Expression
1 btwntriv1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A Btwn <. A , B >. )
2 1 3mix1d 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A Btwn <. A , B >. \/ A Btwn <. B , A >. \/ B Btwn <. A , A >. ) )
3 simp1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> N e. NN )
4 simp2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
5 simp3 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
6 brcolinear 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( A Colinear <. A , B >. <-> ( A Btwn <. A , B >. \/ A Btwn <. B , A >. \/ B Btwn <. A , A >. ) ) )
7 3 4 4 5 6 syl13anc 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A Colinear <. A , B >. <-> ( A Btwn <. A , B >. \/ A Btwn <. B , A >. \/ B Btwn <. A , A >. ) ) )
8 2 7 mpbird 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A Colinear <. A , B >. )