Metamath Proof Explorer

Theorem btwncolinear1

Description: Betweenness implies colinearity. (Contributed by Scott Fenton, 7-Oct-2013)

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

Proof

Step	Hyp	Ref	Expression
1		3mix3	\|- ( C Btwn <. A , B >. -> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) )
2		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 >. ) ) )
3	1 2	syl5ibr	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> A Colinear <. B , C >. ) )

Step

Hyp

Ref

Expression

3mix3

 |-  ( C Btwn <. A , B >. -> ( A Btwn <. B , C >. \/ B Btwn <. C , A >. \/ C Btwn <. A , B >. ) )

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 >. ) ) )

1 2

syl5ibr

 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( C Btwn <. A , B >. -> A Colinear <. B , C >. ) )