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