Description: Construct a point on a half-line, at a given distance of its origin. (Contributed by Thierry Arnoux, 1-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ishlg.p | |
|
ishlg.i | |
||
ishlg.k | |
||
ishlg.a | |
||
ishlg.b | |
||
ishlg.c | |
||
hlln.1 | |
||
hltr.d | |
||
hlcgrex.m | |
||
hlcgrex.1 | |
||
hlcgrex.2 | |
||
Assertion | hlcgrex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ishlg.p | |
|
2 | ishlg.i | |
|
3 | ishlg.k | |
|
4 | ishlg.a | |
|
5 | ishlg.b | |
|
6 | ishlg.c | |
|
7 | hlln.1 | |
|
8 | hltr.d | |
|
9 | hlcgrex.m | |
|
10 | hlcgrex.1 | |
|
11 | hlcgrex.2 | |
|
12 | 7 | ad2antrr | |
13 | simplr | |
|
14 | 4 | ad2antrr | |
15 | 5 | ad2antrr | |
16 | 6 | ad2antrr | |
17 | 1 9 2 12 13 14 15 16 | axtgsegcon | |
18 | 12 | ad2antrr | |
19 | 15 | ad2antrr | |
20 | 16 | ad2antrr | |
21 | simplr | |
|
22 | 14 | ad2antrr | |
23 | simprr | |
|
24 | 1 9 2 18 22 21 19 20 23 | tgcgrcoml | |
25 | 24 | eqcomd | |
26 | 11 | ad4antr | |
27 | 1 9 2 18 19 20 21 22 25 26 | tgcgrneq | |
28 | 10 | ad4antr | |
29 | 13 | ad2antrr | |
30 | 8 | ad4antr | |
31 | simpllr | |
|
32 | 31 | simprd | |
33 | 32 | necomd | |
34 | simprl | |
|
35 | 31 | simpld | |
36 | 1 9 2 18 30 22 29 35 | tgbtwncom | |
37 | 1 2 18 29 22 21 30 33 34 36 | tgbtwnconn2 | |
38 | 1 2 3 21 30 22 18 | ishlg | |
39 | 27 28 37 38 | mpbir3and | |
40 | 39 23 | jca | |
41 | 40 | ex | |
42 | 41 | reximdva | |
43 | 17 42 | mpd | |
44 | 1 | fvexi | |
45 | 44 | a1i | |
46 | 45 5 6 11 | nehash2 | |
47 | 1 9 2 7 8 4 46 | tgbtwndiff | |
48 | 43 47 | r19.29a | |