Description: Given a nondegenerate ray, there is a unique point congruent to the segment B C lying on the ray A R . Theorem 6.11 of Schwabhauser p. 44. (Contributed by Scott Fenton, 23-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | outsideofeu | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | segcon2 | |
|
2 | 1 | adantr | |
3 | simpl1 | |
|
4 | simpl2l | |
|
5 | simpr | |
|
6 | simpl2r | |
|
7 | broutsideof2 | |
|
8 | 3 4 5 6 7 | syl13anc | |
9 | 8 | adantr | |
10 | simp3 | |
|
11 | simpllr | |
|
12 | 11 | adantl | |
13 | simprlr | |
|
14 | simp2l | |
|
15 | 14 | anim1i | |
16 | simpl3 | |
|
17 | cgrdegen | |
|
18 | 3 15 16 17 | syl3anc | |
19 | 18 | adantr | |
20 | 13 19 | mpd | |
21 | 20 | necon3bid | |
22 | 12 21 | mpbird | |
23 | 22 | necomd | |
24 | simplll | |
|
25 | 24 | adantl | |
26 | simprr | |
|
27 | 23 25 26 | 3jca | |
28 | 27 | expr | |
29 | 10 28 | impbid2 | |
30 | 9 29 | bitrd | |
31 | orcom | |
|
32 | 30 31 | bitrdi | |
33 | 32 | expr | |
34 | 33 | pm5.32rd | |
35 | 34 | an32s | |
36 | 35 | rexbidva | |
37 | 2 36 | mpbird | |
38 | simpl1 | |
|
39 | simpl2l | |
|
40 | simpl2r | |
|
41 | simpl3l | |
|
42 | 39 40 41 | 3jca | |
43 | simpl3r | |
|
44 | simprl | |
|
45 | simprr | |
|
46 | 43 44 45 | 3jca | |
47 | 38 42 46 | 3jca | |
48 | simpr | |
|
49 | outsideofeq | |
|
50 | 49 | imp | |
51 | 47 48 50 | syl2an | |
52 | 51 | an4s | |
53 | 52 | exp32 | |
54 | 53 | ralrimivv | |
55 | opeq1 | |
|
56 | 55 | breq2d | |
57 | opeq2 | |
|
58 | 57 | breq1d | |
59 | 56 58 | anbi12d | |
60 | 59 | reu4 | |
61 | 37 54 60 | sylanbrc | |
62 | 61 | ex | |