Metamath Proof Explorer


Theorem brsegle2

Description: Alternate characterization of segment comparison. Theorem 5.5 of Schwabhauser p. 41-42. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion brsegle2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B Seg C D x 𝔼 N B Btwn A x A x Cgr C D

Proof

Step Hyp Ref Expression
1 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
2 simprl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y y Btwn C D
3 simpl1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N N
4 simpl3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N C 𝔼 N
5 simpl3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N D 𝔼 N
6 simpr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y 𝔼 N
7 btwncolinear2 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D C Colinear y D
8 3 4 5 6 7 syl13anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D C Colinear y D
9 8 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y y Btwn C D C Colinear y D
10 2 9 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C Colinear y D
11 simpl2l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N A 𝔼 N
12 simpl2r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N B 𝔼 N
13 simprr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y A B Cgr C y
14 3 11 12 4 6 13 cgrcomand N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B
15 simpl2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N A 𝔼 N B 𝔼 N
16 lineext N C 𝔼 N y 𝔼 N D 𝔼 N A 𝔼 N B 𝔼 N C Colinear y D C y Cgr A B x 𝔼 N C y D Cgr3 A B x
17 3 4 6 5 15 16 syl131anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N C Colinear y D C y Cgr A B x 𝔼 N C y D Cgr3 A B x
18 17 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C Colinear y D C y Cgr A B x 𝔼 N C y D Cgr3 A B x
19 10 14 18 mp2and N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y x 𝔼 N C y D Cgr3 A B x
20 an32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N x 𝔼 N N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N
21 simpll1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N N
22 simpl3l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N C 𝔼 N
23 22 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N C 𝔼 N
24 simpr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y 𝔼 N
25 simpl3r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N D 𝔼 N
26 25 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N D 𝔼 N
27 simpl2l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N A 𝔼 N
28 27 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N A 𝔼 N
29 simpl2r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B 𝔼 N
30 29 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B 𝔼 N
31 simplr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N x 𝔼 N
32 brcgr3 N C 𝔼 N y 𝔼 N D 𝔼 N A 𝔼 N B 𝔼 N x 𝔼 N C y D Cgr3 A B x C y Cgr A B C D Cgr A x y D Cgr B x
33 21 23 24 26 28 30 31 32 syl133anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N C y D Cgr3 A B x C y Cgr A B C D Cgr A x y D Cgr B x
34 33 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y D Cgr3 A B x C y Cgr A B C D Cgr A x y D Cgr B x
35 simp2l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x y Btwn C D
36 simp3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x C y Cgr A B C D Cgr A x y D Cgr B x
37 33 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x C y D Cgr3 A B x C y Cgr A B C D Cgr A x y D Cgr B x
38 36 37 mpbird N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x C y D Cgr3 A B x
39 btwnxfr N C 𝔼 N y 𝔼 N D 𝔼 N A 𝔼 N B 𝔼 N x 𝔼 N y Btwn C D C y D Cgr3 A B x B Btwn A x
40 21 23 24 26 28 30 31 39 syl133anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D C y D Cgr3 A B x B Btwn A x
41 40 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x y Btwn C D C y D Cgr3 A B x B Btwn A x
42 35 38 41 mp2and N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x B Btwn A x
43 simp32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x C D Cgr A x
44 cgrcom N C 𝔼 N D 𝔼 N A 𝔼 N x 𝔼 N C D Cgr A x A x Cgr C D
45 21 23 26 28 31 44 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N C D Cgr A x A x Cgr C D
46 45 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x C D Cgr A x A x Cgr C D
47 43 46 mpbid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x A x Cgr C D
48 42 47 jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x B Btwn A x A x Cgr C D
49 48 3expia N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y Cgr A B C D Cgr A x y D Cgr B x B Btwn A x A x Cgr C D
50 34 49 sylbid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y C y D Cgr3 A B x B Btwn A x A x Cgr C D
51 20 50 sylanb N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N x 𝔼 N y Btwn C D A B Cgr C y C y D Cgr3 A B x B Btwn A x A x Cgr C D
52 51 an32s N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y x 𝔼 N C y D Cgr3 A B x B Btwn A x A x Cgr C D
53 52 reximdva N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y x 𝔼 N C y D Cgr3 A B x x 𝔼 N B Btwn A x A x Cgr C D
54 19 53 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y x 𝔼 N B Btwn A x A x Cgr C D
55 54 rexlimdva2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y x 𝔼 N B Btwn A x A x Cgr C D
56 simprl N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D B Btwn A x
57 simpll1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D N
58 27 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D A 𝔼 N
59 simplr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D x 𝔼 N
60 29 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D B 𝔼 N
61 btwncolinear1 N A 𝔼 N x 𝔼 N B 𝔼 N B Btwn A x A Colinear x B
62 57 58 59 60 61 syl13anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D B Btwn A x A Colinear x B
63 56 62 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D A Colinear x B
64 simprr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D
65 simpl1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N N
66 simpr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N x 𝔼 N
67 simpl3 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N C 𝔼 N D 𝔼 N
68 lineext N A 𝔼 N x 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A Colinear x B A x Cgr C D y 𝔼 N A x B Cgr3 C D y
69 65 27 66 29 67 68 syl131anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N A Colinear x B A x Cgr C D y 𝔼 N A x B Cgr3 C D y
70 69 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D A Colinear x B A x Cgr C D y 𝔼 N A x B Cgr3 C D y
71 63 64 70 mp2and N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D y 𝔼 N A x B Cgr3 C D y
72 27 66 29 3jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N A 𝔼 N x 𝔼 N B 𝔼 N
73 72 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N A 𝔼 N x 𝔼 N B 𝔼 N
74 brcgr3 N A 𝔼 N x 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N A x B Cgr3 C D y A x Cgr C D A B Cgr C y x B Cgr D y
75 21 73 23 26 24 74 syl113anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N A x B Cgr3 C D y A x Cgr C D A B Cgr C y x B Cgr D y
76 75 adantr N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x B Cgr3 C D y A x Cgr C D A B Cgr C y x B Cgr D y
77 simp2l N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y B Btwn A x
78 simp32 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y A B Cgr C y
79 simp2r N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y A x Cgr C D
80 simp33 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y x B Cgr D y
81 cgrcomlr N x 𝔼 N B 𝔼 N D 𝔼 N y 𝔼 N x B Cgr D y B x Cgr y D
82 21 31 30 26 24 81 syl122anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N x B Cgr D y B x Cgr y D
83 82 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y x B Cgr D y B x Cgr y D
84 80 83 mpbid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y B x Cgr y D
85 78 79 84 3jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y A B Cgr C y A x Cgr C D B x Cgr y D
86 brcgr3 N A 𝔼 N B 𝔼 N x 𝔼 N C 𝔼 N y 𝔼 N D 𝔼 N A B x Cgr3 C y D A B Cgr C y A x Cgr C D B x Cgr y D
87 21 28 30 31 23 24 26 86 syl133anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N A B x Cgr3 C y D A B Cgr C y A x Cgr C D B x Cgr y D
88 87 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y A B x Cgr3 C y D A B Cgr C y A x Cgr C D B x Cgr y D
89 85 88 mpbird N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y A B x Cgr3 C y D
90 btwnxfr N A 𝔼 N B 𝔼 N x 𝔼 N C 𝔼 N y 𝔼 N D 𝔼 N B Btwn A x A B x Cgr3 C y D y Btwn C D
91 21 28 30 31 23 24 26 90 syl133anc N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A B x Cgr3 C y D y Btwn C D
92 91 3ad2ant1 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y B Btwn A x A B x Cgr3 C y D y Btwn C D
93 77 89 92 mp2and N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y y Btwn C D
94 93 78 jca N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y y Btwn C D A B Cgr C y
95 94 3expia N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x Cgr C D A B Cgr C y x B Cgr D y y Btwn C D A B Cgr C y
96 76 95 sylbid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N y 𝔼 N B Btwn A x A x Cgr C D A x B Cgr3 C D y y Btwn C D A B Cgr C y
97 96 an32s N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D y 𝔼 N A x B Cgr3 C D y y Btwn C D A B Cgr C y
98 97 reximdva N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D y 𝔼 N A x B Cgr3 C D y y 𝔼 N y Btwn C D A B Cgr C y
99 71 98 mpd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D y 𝔼 N y Btwn C D A B Cgr C y
100 99 rexlimdva2 N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N x 𝔼 N B Btwn A x A x Cgr C D y 𝔼 N y Btwn C D A B Cgr C y
101 55 100 impbid N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N y 𝔼 N y Btwn C D A B Cgr C y x 𝔼 N B Btwn A x A x Cgr C D
102 1 101 bitrd N A 𝔼 N B 𝔼 N C 𝔼 N D 𝔼 N A B Seg C D x 𝔼 N B Btwn A x A x Cgr C D