Step |
Hyp |
Ref |
Expression |
1 |
|
simprll |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> y Btwn <. C , D >. ) |
2 |
|
simprrr |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> <. C , D >. Cgr <. E , z >. ) |
3 |
1 2
|
jca |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> ( y Btwn <. C , D >. /\ <. C , D >. Cgr <. E , z >. ) ) |
4 |
|
simpl1 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> N e. NN ) |
5 |
|
simpl23 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> C e. ( EE ` N ) ) |
6 |
|
simprl |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> y e. ( EE ` N ) ) |
7 |
|
simpl31 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> D e. ( EE ` N ) ) |
8 |
|
simpl32 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> E e. ( EE ` N ) ) |
9 |
|
simprr |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> z e. ( EE ` N ) ) |
10 |
|
cgrxfr |
|- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> ( ( y Btwn <. C , D >. /\ <. C , D >. Cgr <. E , z >. ) -> E. w e. ( EE ` N ) ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) ) ) |
11 |
4 5 6 7 8 9 10
|
syl132anc |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> ( ( y Btwn <. C , D >. /\ <. C , D >. Cgr <. E , z >. ) -> E. w e. ( EE ` N ) ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) ) ) |
12 |
11
|
adantr |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> ( ( y Btwn <. C , D >. /\ <. C , D >. Cgr <. E , z >. ) -> E. w e. ( EE ` N ) ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) ) ) |
13 |
3 12
|
mpd |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> E. w e. ( EE ` N ) ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) ) |
14 |
|
anass |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ w e. ( EE ` N ) ) <-> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) /\ w e. ( EE ` N ) ) ) ) |
15 |
|
df-3an |
|- ( ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) <-> ( ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) /\ w e. ( EE ` N ) ) ) |
16 |
15
|
anbi2i |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) <-> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) /\ w e. ( EE ` N ) ) ) ) |
17 |
14 16
|
bitr4i |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ w e. ( EE ` N ) ) <-> ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) ) |
18 |
|
simpl1 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> N e. NN ) |
19 |
|
simpl23 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> C e. ( EE ` N ) ) |
20 |
|
simpr1 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> y e. ( EE ` N ) ) |
21 |
|
simpl31 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> D e. ( EE ` N ) ) |
22 |
|
simpl32 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> E e. ( EE ` N ) ) |
23 |
|
simpr3 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> w e. ( EE ` N ) ) |
24 |
|
simpr2 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> z e. ( EE ` N ) ) |
25 |
|
brcgr3 |
|- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ y e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ w e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) -> ( <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. <-> ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) |
26 |
18 19 20 21 22 23 24 25
|
syl133anc |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> ( <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. <-> ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) |
27 |
26
|
anbi2d |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> ( ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) <-> ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) |
28 |
27
|
adantr |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> ( ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) <-> ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) |
29 |
|
df-3an |
|- ( ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) <-> ( ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) |
30 |
|
simpl33 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> F e. ( EE ` N ) ) |
31 |
|
simpr3l |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> w Btwn <. E , z >. ) |
32 |
|
simpr2l |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> z Btwn <. E , F >. ) |
33 |
18 22 23 24 30 31 32
|
btwnexchand |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> w Btwn <. E , F >. ) |
34 |
|
simpl21 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> A e. ( EE ` N ) ) |
35 |
|
simpl22 |
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) -> B e. ( EE ` N ) ) |
36 |
|
simpr1r |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> <. A , B >. Cgr <. C , y >. ) |
37 |
|
simp3r1 |
|- ( ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) -> <. C , y >. Cgr <. E , w >. ) |
38 |
37
|
adantl |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> <. C , y >. Cgr <. E , w >. ) |
39 |
18 34 35 19 20 22 23 36 38
|
cgrtrand |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> <. A , B >. Cgr <. E , w >. ) |
40 |
33 39
|
jca |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) |
41 |
29 40
|
sylan2br |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) /\ ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) ) ) -> ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) |
42 |
41
|
expr |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> ( ( w Btwn <. E , z >. /\ ( <. C , y >. Cgr <. E , w >. /\ <. C , D >. Cgr <. E , z >. /\ <. y , D >. Cgr <. w , z >. ) ) -> ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
43 |
28 42
|
sylbid |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) /\ w e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> ( ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) -> ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
44 |
17 43
|
sylanb |
|- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ w e. ( EE ` N ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> ( ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) -> ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
45 |
44
|
an32s |
|- ( ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) /\ w e. ( EE ` N ) ) -> ( ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) -> ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
46 |
45
|
reximdva |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> ( E. w e. ( EE ` N ) ( w Btwn <. E , z >. /\ <. C , <. y , D >. >. Cgr3 <. E , <. w , z >. >. ) -> E. w e. ( EE ` N ) ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
47 |
13 46
|
mpd |
|- ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) ) /\ ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) -> E. w e. ( EE ` N ) ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) |
48 |
47
|
exp31 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( y e. ( EE ` N ) /\ z e. ( EE ` N ) ) -> ( ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) -> E. w e. ( EE ` N ) ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) ) |
49 |
48
|
rexlimdvv |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( E. y e. ( EE ` N ) E. z e. ( EE ` N ) ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) -> E. w e. ( EE ` N ) ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
50 |
|
simp1 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> N e. NN ) |
51 |
|
simp21 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> A e. ( EE ` N ) ) |
52 |
|
simp22 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> B e. ( EE ` N ) ) |
53 |
|
simp23 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> C e. ( EE ` N ) ) |
54 |
|
simp31 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> D e. ( EE ` N ) ) |
55 |
|
brsegle |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) |
56 |
50 51 52 53 54 55
|
syl122anc |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. C , D >. <-> E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) ) ) |
57 |
|
simp32 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> E e. ( EE ` N ) ) |
58 |
|
simp33 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> F e. ( EE ` N ) ) |
59 |
|
brsegle |
|- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. C , D >. Seg<_ <. E , F >. <-> E. z e. ( EE ` N ) ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) |
60 |
50 53 54 57 58 59
|
syl122anc |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. C , D >. Seg<_ <. E , F >. <-> E. z e. ( EE ` N ) ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) |
61 |
56 60
|
anbi12d |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Seg<_ <. C , D >. /\ <. C , D >. Seg<_ <. E , F >. ) <-> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ E. z e. ( EE ` N ) ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) ) |
62 |
|
reeanv |
|- ( E. y e. ( EE ` N ) E. z e. ( EE ` N ) ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) <-> ( E. y e. ( EE ` N ) ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ E. z e. ( EE ` N ) ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) |
63 |
61 62
|
bitr4di |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Seg<_ <. C , D >. /\ <. C , D >. Seg<_ <. E , F >. ) <-> E. y e. ( EE ` N ) E. z e. ( EE ` N ) ( ( y Btwn <. C , D >. /\ <. A , B >. Cgr <. C , y >. ) /\ ( z Btwn <. E , F >. /\ <. C , D >. Cgr <. E , z >. ) ) ) ) |
64 |
|
brsegle |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. E , F >. <-> E. w e. ( EE ` N ) ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
65 |
50 51 52 57 58 64
|
syl122anc |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. E , F >. <-> E. w e. ( EE ` N ) ( w Btwn <. E , F >. /\ <. A , B >. Cgr <. E , w >. ) ) ) |
66 |
49 63 65
|
3imtr4d |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Seg<_ <. C , D >. /\ <. C , D >. Seg<_ <. E , F >. ) -> <. A , B >. Seg<_ <. E , F >. ) ) |