Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> N e. NN ) |
2 |
|
simp2r |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> B e. ( EE ` N ) ) |
3 |
|
simp3r |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> D e. ( EE ` N ) ) |
4 |
|
simp2l |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> A e. ( EE ` N ) ) |
5 |
|
necom |
|- ( B =/= C <-> C =/= B ) |
6 |
5
|
a1i |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( B =/= C <-> C =/= B ) ) |
7 |
|
simp3l |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> C e. ( EE ` N ) ) |
8 |
|
btwncom |
|- ( ( N e. NN /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) ) |
9 |
1 2 4 7 8
|
syl13anc |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( B Btwn <. A , C >. <-> B Btwn <. C , A >. ) ) |
10 |
|
btwncom |
|- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ B e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. B , D >. <-> C Btwn <. D , B >. ) ) |
11 |
1 7 2 3 10
|
syl13anc |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( C Btwn <. B , D >. <-> C Btwn <. D , B >. ) ) |
12 |
6 9 11
|
3anbi123d |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) <-> ( C =/= B /\ B Btwn <. C , A >. /\ C Btwn <. D , B >. ) ) ) |
13 |
|
3ancomb |
|- ( ( C =/= B /\ B Btwn <. C , A >. /\ C Btwn <. D , B >. ) <-> ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) ) |
14 |
12 13
|
syl6bb |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) <-> ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) ) ) |
15 |
14
|
biimpa |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) ) |
16 |
|
btwnouttr2 |
|- ( ( N e. NN /\ ( D e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) -> B Btwn <. D , A >. ) ) |
17 |
1 3 7 2 4 16
|
syl122anc |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) -> B Btwn <. D , A >. ) ) |
18 |
17
|
adantr |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> ( ( C =/= B /\ C Btwn <. D , B >. /\ B Btwn <. C , A >. ) -> B Btwn <. D , A >. ) ) |
19 |
15 18
|
mpd |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> B Btwn <. D , A >. ) |
20 |
1 2 3 4 19
|
btwncomand |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) /\ ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) ) -> B Btwn <. A , D >. ) |
21 |
20
|
ex |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( ( B =/= C /\ B Btwn <. A , C >. /\ C Btwn <. B , D >. ) -> B Btwn <. A , D >. ) ) |