Metamath Proof Explorer


Theorem segletr

Description: Segment less than is transitive. Theorem 5.8 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion segletr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Seg C D C D Seg E F A B Seg E F

Proof

Step Hyp Ref Expression
1 simprll N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N N
5 simpl23 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N C 𝔼 N
6 simprl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y 𝔼 N
7 simpl31 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N D 𝔼 N
8 simpl32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N E 𝔼 N
9 simprr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N z 𝔼 N
10 cgrxfr N C 𝔼 N y 𝔼 N D 𝔼 N E 𝔼 N z 𝔼 N y Btwn C D C D Cgr E z w 𝔼 N w Btwn E z C y D Cgr3 E w z
11 4 5 6 7 8 9 10 syl132anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y Btwn C D C D Cgr E z w 𝔼 N w Btwn E z C y D Cgr3 E w z
12 11 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 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 w 𝔼 N w Btwn E z C y D Cgr3 E w z
13 3 12 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z w 𝔼 N w Btwn E z C y D Cgr3 E w z
14 anass N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N
15 df-3an y 𝔼 N z 𝔼 N w 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N
16 15 anbi2i N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N
17 14 16 bitr4i N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N
18 simpl1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N N
19 simpl23 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N C 𝔼 N
20 simpr1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N y 𝔼 N
21 simpl31 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N D 𝔼 N
22 simpl32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N E 𝔼 N
23 simpr3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N w 𝔼 N
24 simpr2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N z 𝔼 N
25 brcgr3 N C 𝔼 N y 𝔼 N D 𝔼 N E 𝔼 N w 𝔼 N z 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N F 𝔼 N
31 simpr3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N A 𝔼 N
35 simpl22 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 N B 𝔼 N
36 simpr1r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z w 𝔼 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 A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z w 𝔼 N w Btwn E z C y D Cgr3 E w z w 𝔼 N w Btwn E F A B Cgr E w
47 13 46 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z w 𝔼 N w Btwn E F A B Cgr E w
48 47 exp31 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z w 𝔼 N w Btwn E F A B Cgr E w
49 48 rexlimdvv N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z w 𝔼 N w Btwn E F A B Cgr E w
50 simp1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N N
51 simp21 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A 𝔼 N
52 simp22 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N B 𝔼 N
53 simp23 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N C 𝔼 N
54 simp31 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N D 𝔼 N
55 brsegle N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B Seg C D y 𝔼 N y Btwn C D A B Cgr C y
56 50 51 52 53 54 55 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Seg C D y 𝔼 N y Btwn C D A B Cgr C y
57 simp32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N E 𝔼 N
58 simp33 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N F 𝔼 N
59 brsegle N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N C D Seg E F z 𝔼 N z Btwn E F C D Cgr E z
60 50 53 54 57 58 59 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N C D Seg E F z 𝔼 N z Btwn E F C D Cgr E z
61 56 60 anbi12d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Seg C D C D Seg E F y 𝔼 N y Btwn C D A B Cgr C y z 𝔼 N z Btwn E F C D Cgr E z
62 reeanv y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z y 𝔼 N y Btwn C D A B Cgr C y z 𝔼 N z Btwn E F C D Cgr E z
63 61 62 bitr4di N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Seg C D C D Seg E F y 𝔼 N z 𝔼 N y Btwn C D A B Cgr C y z Btwn E F C D Cgr E z
64 brsegle N A 𝔼 N B 𝔼 N E 𝔼 N F 𝔼 N A B Seg E F w 𝔼 N w Btwn E F A B Cgr E w
65 50 51 52 57 58 64 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Seg E F w 𝔼 N w Btwn E F A B Cgr E w
66 49 63 65 3imtr4d N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N E 𝔼 N F 𝔼 N A B Seg C D C D Seg E F A B Seg E F