Metamath Proof Explorer

Theorem outsideofrflx

Description: Reflexivity of outsideness. Theorem 6.5 of Schwabhauser p. 44. (Contributed by Scott Fenton, 18-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofrflx 
|- ( ( N e. NN /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( A =/= P -> P OutsideOf <. A , A >. ) )

Proof

Step Hyp Ref Expression
1 axbtwnid 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( P Btwn <. A , A >. -> P = A ) )
2 eqcom 
 |-  ( P = A <-> A = P )
3 1 2 syl6ib 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( P Btwn <. A , A >. -> A = P ) )
4 3 necon3ad 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( A =/= P -> -. P Btwn <. A , A >. ) )
5 colineartriv2 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> P Colinear <. A , A >. )
6 4 5 jctild 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( A =/= P -> ( P Colinear <. A , A >. /\ -. P Btwn <. A , A >. ) ) )
7 broutsideof 
 |-  ( P OutsideOf <. A , A >. <-> ( P Colinear <. A , A >. /\ -. P Btwn <. A , A >. ) )
8 6 7 syl6ibr 
 |-  ( ( N e. NN /\ P e. ( EE ` N ) /\ A e. ( EE ` N ) ) -> ( A =/= P -> P OutsideOf <. A , A >. ) )