Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π β β) |
2 | | simpr 485 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π₯ β (πΌβπ)) |
3 | | simpl21 1251 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π β (πΌβπ)) |
4 | | simpl22 1252 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π β (πΌβπ)) |
5 | | brcolinear 35019 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (π₯ Colinear β¨π, πβ© β (π₯ Btwn β¨π, πβ© β¨ π Btwn β¨π, π₯β© β¨ π Btwn β¨π₯, πβ©))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1372 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π₯ Colinear β¨π, πβ© β (π₯ Btwn β¨π, πβ© β¨ π Btwn β¨π, π₯β© β¨ π Btwn β¨π₯, πβ©))) |
7 | 6 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Colinear β¨π, πβ© β (π₯ Btwn β¨π, πβ© β¨ π Btwn β¨π, π₯β© β¨ π Btwn β¨π₯, πβ©))) |
8 | | olc 866 |
. . . . . . . . . . . . . 14
β’ (π₯ Btwn β¨π, πβ© β (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) |
9 | 8 | orcd 871 |
. . . . . . . . . . . . 13
β’ (π₯ Btwn β¨π, πβ© β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Btwn β¨π, πβ© β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
11 | | simpl3l 1228 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π β π) |
12 | 11 | necomd 2996 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π β π) |
13 | 12 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) β π β π) |
14 | | simprl 769 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) β π Btwn β¨π, π
β©) |
15 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) β π Btwn β¨π, π₯β©) |
16 | 13, 14, 15 | 3jca 1128 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) β (π β π β§ π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) |
17 | | simpl23 1253 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π
β (πΌβπ)) |
18 | | btwnconn2 35062 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ)) β§ (π
β (πΌβπ) β§ π₯ β (πΌβπ))) β ((π β π β§ π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©) β (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
19 | 1, 4, 3, 17, 2, 18 | syl122anc 1379 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((π β π β§ π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©) β (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) β ((π β π β§ π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©) β (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
21 | 16, 20 | mpd 15 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) β (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)) |
22 | 21 | olcd 872 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π Btwn β¨π, π₯β©)) β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
23 | 22 | expr 457 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π Btwn β¨π, π₯β© β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
24 | | btwncom 34974 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ (π β (πΌβπ) β§ π₯ β (πΌβπ) β§ π β (πΌβπ))) β (π Btwn β¨π₯, πβ© β π Btwn β¨π, π₯β©)) |
25 | 1, 4, 2, 3, 24 | syl13anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π Btwn β¨π₯, πβ© β π Btwn β¨π, π₯β©)) |
26 | | orc 865 |
. . . . . . . . . . . . . . 15
β’ (π Btwn β¨π, π₯β© β (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) |
27 | 26 | orcd 871 |
. . . . . . . . . . . . . 14
β’ (π Btwn β¨π, π₯β© β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
28 | 25, 27 | syl6bi 252 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π Btwn β¨π₯, πβ© β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π Btwn β¨π₯, πβ© β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
30 | 10, 23, 29 | 3jaod 1428 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β ((π₯ Btwn β¨π, πβ© β¨ π Btwn β¨π, π₯β© β¨ π Btwn β¨π₯, πβ©) β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
31 | 7, 30 | sylbid 239 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Colinear β¨π, πβ© β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
32 | | olc 866 |
. . . . . . . . . 10
β’ (((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)) β (π₯ = π β¨ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
33 | 31, 32 | syl6 35 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Colinear β¨π, πβ© β (π₯ = π β¨ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))))) |
34 | | colineartriv1 35027 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β (πΌβπ) β§ π β (πΌβπ)) β π Colinear β¨π, πβ©) |
35 | 1, 3, 4, 34 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π Colinear β¨π, πβ©) |
36 | | breq1 5150 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π₯ Colinear β¨π, πβ© β π Colinear β¨π, πβ©)) |
37 | 35, 36 | syl5ibrcom 246 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π₯ = π β π₯ Colinear β¨π, πβ©)) |
38 | 37 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ = π β π₯ Colinear β¨π, πβ©)) |
39 | | btwncolinear3 35031 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π₯ β (πΌβπ) β§ π β (πΌβπ))) β (π Btwn β¨π, π₯β© β π₯ Colinear β¨π, πβ©)) |
40 | 1, 3, 2, 4, 39 | syl13anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π Btwn β¨π, π₯β© β π₯ Colinear β¨π, πβ©)) |
41 | | btwncolinear5 35033 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π₯ β (πΌβπ))) β (π₯ Btwn β¨π, πβ© β π₯ Colinear β¨π, πβ©)) |
42 | 1, 3, 4, 2, 41 | syl13anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π₯ Btwn β¨π, πβ© β π₯ Colinear β¨π, πβ©)) |
43 | 40, 42 | jaod 857 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β π₯ Colinear β¨π, πβ©)) |
44 | 43 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β π₯ Colinear β¨π, πβ©)) |
45 | | simpl3r 1229 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β π β π
) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β π β π
) |
47 | | simprl 769 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β π Btwn β¨π, π
β©) |
48 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β π
Btwn β¨π, π₯β©) |
49 | 46, 47, 48 | 3jca 1128 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β (π β π
β§ π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) |
50 | | btwnouttr 34984 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ)) β§ (π
β (πΌβπ) β§ π₯ β (πΌβπ))) β ((π β π
β§ π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©) β π Btwn β¨π, π₯β©)) |
51 | 1, 4, 3, 17, 2, 50 | syl122anc 1379 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((π β π
β§ π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©) β π Btwn β¨π, π₯β©)) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β ((π β π
β§ π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©) β π Btwn β¨π, π₯β©)) |
53 | 49, 52 | mpd 15 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β π Btwn β¨π, π₯β©) |
54 | | btwncolinear4 35032 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π β (πΌβπ) β§ π₯ β (πΌβπ) β§ π β (πΌβπ))) β (π Btwn β¨π, π₯β© β π₯ Colinear β¨π, πβ©)) |
55 | 1, 4, 2, 3, 54 | syl13anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π Btwn β¨π, π₯β© β π₯ Colinear β¨π, πβ©)) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β (π Btwn β¨π, π₯β© β π₯ Colinear β¨π, πβ©)) |
57 | 53, 56 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π
Btwn β¨π, π₯β©)) β π₯ Colinear β¨π, πβ©) |
58 | 57 | expr 457 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π
Btwn β¨π, π₯β© β π₯ Colinear β¨π, πβ©)) |
59 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π₯ Btwn β¨π, π
β©)) β π₯ Btwn β¨π, π
β©) |
60 | 1, 2, 3, 17, 59 | btwncomand 34975 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π₯ Btwn β¨π, π
β©)) β π₯ Btwn β¨π
, πβ©) |
61 | | simprl 769 |
. . . . . . . . . . . . . . . 16
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π₯ Btwn β¨π, π
β©)) β π Btwn β¨π, π
β©) |
62 | 1, 3, 4, 17, 61 | btwncomand 34975 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π₯ Btwn β¨π, π
β©)) β π Btwn β¨π
, πβ©) |
63 | 1, 17, 2, 3, 4, 60,
62 | btwnexch3and 34981 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π₯ Btwn β¨π, π
β©)) β π Btwn β¨π₯, πβ©) |
64 | | btwncolinear2 35030 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π₯ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (π Btwn β¨π₯, πβ© β π₯ Colinear β¨π, πβ©)) |
65 | 1, 2, 4, 3, 64 | syl13anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (π Btwn β¨π₯, πβ© β π₯ Colinear β¨π, πβ©)) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π₯ Btwn β¨π, π
β©)) β (π Btwn β¨π₯, πβ© β π₯ Colinear β¨π, πβ©)) |
67 | 63, 66 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ (π Btwn β¨π, π
β© β§ π₯ Btwn β¨π, π
β©)) β π₯ Colinear β¨π, πβ©) |
68 | 67 | expr 457 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Btwn β¨π, π
β© β π₯ Colinear β¨π, πβ©)) |
69 | 58, 68 | jaod 857 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β ((π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©) β π₯ Colinear β¨π, πβ©)) |
70 | 44, 69 | jaod 857 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)) β π₯ Colinear β¨π, πβ©)) |
71 | 38, 70 | jaod 857 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β ((π₯ = π β¨ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) β π₯ Colinear β¨π, πβ©)) |
72 | 33, 71 | impbid 211 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Colinear β¨π, πβ© β (π₯ = π β¨ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))))) |
73 | | pm5.63 1018 |
. . . . . . . . 9
β’ ((π₯ = π β¨ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) β (π₯ = π β¨ (Β¬ π₯ = π β§ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))))) |
74 | | df-ne 2941 |
. . . . . . . . . . . 12
β’ (π₯ β π β Β¬ π₯ = π) |
75 | 74 | anbi1i 624 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) β (Β¬ π₯ = π β§ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
76 | | andi 1006 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) β ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
77 | 75, 76 | bitr3i 276 |
. . . . . . . . . 10
β’ ((Β¬
π₯ = π β§ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) β ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
78 | 77 | orbi2i 911 |
. . . . . . . . 9
β’ ((π₯ = π β¨ (Β¬ π₯ = π β§ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) β (π₯ = π β¨ ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))))) |
79 | 73, 78 | bitri 274 |
. . . . . . . 8
β’ ((π₯ = π β¨ ((π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©) β¨ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) β (π₯ = π β¨ ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))))) |
80 | 72, 79 | bitrdi 286 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Colinear β¨π, πβ© β (π₯ = π β¨ ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))))) |
81 | | broutsideof2 35082 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π₯ β (πΌβπ))) β (πOutsideOfβ¨π, π₯β© β (π β π β§ π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) |
82 | 1, 3, 4, 2, 81 | syl13anc 1372 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (πOutsideOfβ¨π, π₯β© β (π β π β§ π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) |
83 | | 3simpc 1150 |
. . . . . . . . . . . 12
β’ ((π β π β§ π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©))) |
84 | | simpl3l 1228 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) β π β π) |
85 | 84 | necomd 2996 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) β π β π) |
86 | | simprrl 779 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) β π₯ β π) |
87 | | simprrr 780 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) β (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) |
88 | 85, 86, 87 | 3jca 1128 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) β (π β π β§ π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©))) |
89 | 88 | expr 457 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β (π β π β§ π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) |
90 | 83, 89 | impbid2 225 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((π β π β§ π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) |
91 | 82, 90 | bitrd 278 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (πOutsideOfβ¨π, π₯β© β (π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)))) |
92 | | broutsideof2 35082 |
. . . . . . . . . . . 12
β’ ((π β β β§ (π β (πΌβπ) β§ π
β (πΌβπ) β§ π₯ β (πΌβπ))) β (πOutsideOfβ¨π
, π₯β© β (π
β π β§ π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
93 | 1, 3, 17, 2, 92 | syl13anc 1372 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (πOutsideOfβ¨π
, π₯β© β (π
β π β§ π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
94 | | 3simpc 1150 |
. . . . . . . . . . . 12
β’ ((π
β π β§ π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)) β (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
95 | | simpl3r 1229 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) β π β π
) |
96 | 95 | necomd 2996 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) β π
β π) |
97 | | simprrl 779 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) β π₯ β π) |
98 | | simprrr 780 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) β (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)) |
99 | 96, 97, 98 | 3jca 1128 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ (π₯ β (πΌβπ) β§ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) β (π
β π β§ π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))) |
100 | 99 | expr 457 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)) β (π
β π β§ π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
101 | 94, 100 | impbid2 225 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((π
β π β§ π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)) β (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
102 | 93, 101 | bitrd 278 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β (πOutsideOfβ¨π
, π₯β© β (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))) |
103 | 91, 102 | orbi12d 917 |
. . . . . . . . 9
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β ((πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©) β ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))))) |
104 | 103 | adantr 481 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β ((πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©) β ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©))))) |
105 | 104 | orbi2d 914 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β ((π₯ = π β¨ (πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©)) β (π₯ = π β¨ ((π₯ β π β§ (π Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, πβ©)) β¨ (π₯ β π β§ (π
Btwn β¨π, π₯β© β¨ π₯ Btwn β¨π, π
β©)))))) |
106 | 80, 105 | bitr4d 281 |
. . . . . 6
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Colinear β¨π, πβ© β (π₯ = π β¨ (πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©)))) |
107 | | orcom 868 |
. . . . . . 7
β’ ((π₯ = π β¨ (πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©)) β ((πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©) β¨ π₯ = π)) |
108 | | or32 924 |
. . . . . . 7
β’ (((πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©) β¨ π₯ = π) β ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©)) |
109 | 107, 108 | bitri 274 |
. . . . . 6
β’ ((π₯ = π β¨ (πOutsideOfβ¨π, π₯β© β¨ πOutsideOfβ¨π
, π₯β©)) β ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©)) |
110 | 106, 109 | bitrdi 286 |
. . . . 5
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π₯ β (πΌβπ)) β§ π Btwn β¨π, π
β©) β (π₯ Colinear β¨π, πβ© β ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©))) |
111 | 110 | an32s 650 |
. . . 4
β’ ((((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π Btwn β¨π, π
β©) β§ π₯ β (πΌβπ)) β (π₯ Colinear β¨π, πβ© β ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©))) |
112 | 111 | rabbidva 3439 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π Btwn β¨π, π
β©) β {π₯ β (πΌβπ) β£ π₯ Colinear β¨π, πβ©} = {π₯ β (πΌβπ) β£ ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©)}) |
113 | | simp1 1136 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β π β β) |
114 | | simp21 1206 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β π β (πΌβπ)) |
115 | | simp22 1207 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β π β (πΌβπ)) |
116 | | simp3l 1201 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β π β π) |
117 | | fvline2 35106 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β (πLineπ) = {π₯ β (πΌβπ) β£ π₯ Colinear β¨π, πβ©}) |
118 | 113, 114,
115, 116, 117 | syl13anc 1372 |
. . . 4
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β (πLineπ) = {π₯ β (πΌβπ) β£ π₯ Colinear β¨π, πβ©}) |
119 | 118 | adantr 481 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π Btwn β¨π, π
β©) β (πLineπ) = {π₯ β (πΌβπ) β£ π₯ Colinear β¨π, πβ©}) |
120 | | fvray 35101 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π β π)) β (πRayπ) = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) |
121 | 113, 114,
115, 116, 120 | syl13anc 1372 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β (πRayπ) = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©}) |
122 | | rabsn 4724 |
. . . . . . . . 9
β’ (π β (πΌβπ) β {π₯ β (πΌβπ) β£ π₯ = π} = {π}) |
123 | 114, 122 | syl 17 |
. . . . . . . 8
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β {π₯ β (πΌβπ) β£ π₯ = π} = {π}) |
124 | 123 | eqcomd 2738 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β {π} = {π₯ β (πΌβπ) β£ π₯ = π}) |
125 | 121, 124 | uneq12d 4163 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β ((πRayπ) βͺ {π}) = ({π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} βͺ {π₯ β (πΌβπ) β£ π₯ = π})) |
126 | | simp23 1208 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β π
β (πΌβπ)) |
127 | | simp3r 1202 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β π β π
) |
128 | | fvray 35101 |
. . . . . . 7
β’ ((π β β β§ (π β (πΌβπ) β§ π
β (πΌβπ) β§ π β π
)) β (πRayπ
) = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©}) |
129 | 113, 114,
126, 127, 128 | syl13anc 1372 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β (πRayπ
) = {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©}) |
130 | 125, 129 | uneq12d 4163 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β (((πRayπ) βͺ {π}) βͺ (πRayπ
)) = (({π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} βͺ {π₯ β (πΌβπ) β£ π₯ = π}) βͺ {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©})) |
131 | 130 | adantr 481 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π Btwn β¨π, π
β©) β (((πRayπ) βͺ {π}) βͺ (πRayπ
)) = (({π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} βͺ {π₯ β (πΌβπ) β£ π₯ = π}) βͺ {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©})) |
132 | | unrab 4304 |
. . . . . 6
β’ ({π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} βͺ {π₯ β (πΌβπ) β£ π₯ = π}) = {π₯ β (πΌβπ) β£ (πOutsideOfβ¨π, π₯β© β¨ π₯ = π)} |
133 | 132 | uneq1i 4158 |
. . . . 5
β’ (({π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} βͺ {π₯ β (πΌβπ) β£ π₯ = π}) βͺ {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©}) = ({π₯ β (πΌβπ) β£ (πOutsideOfβ¨π, π₯β© β¨ π₯ = π)} βͺ {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©}) |
134 | | unrab 4304 |
. . . . 5
β’ ({π₯ β (πΌβπ) β£ (πOutsideOfβ¨π, π₯β© β¨ π₯ = π)} βͺ {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©}) = {π₯ β (πΌβπ) β£ ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©)} |
135 | 133, 134 | eqtri 2760 |
. . . 4
β’ (({π₯ β (πΌβπ) β£ πOutsideOfβ¨π, π₯β©} βͺ {π₯ β (πΌβπ) β£ π₯ = π}) βͺ {π₯ β (πΌβπ) β£ πOutsideOfβ¨π
, π₯β©}) = {π₯ β (πΌβπ) β£ ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©)} |
136 | 131, 135 | eqtrdi 2788 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π Btwn β¨π, π
β©) β (((πRayπ) βͺ {π}) βͺ (πRayπ
)) = {π₯ β (πΌβπ) β£ ((πOutsideOfβ¨π, π₯β© β¨ π₯ = π) β¨ πOutsideOfβ¨π
, π₯β©)}) |
137 | 112, 119,
136 | 3eqtr4d 2782 |
. 2
β’ (((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β§ π Btwn β¨π, π
β©) β (πLineπ) = (((πRayπ) βͺ {π}) βͺ (πRayπ
))) |
138 | 137 | ex 413 |
1
β’ ((π β β β§ (π β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β π β§ π β π
)) β (π Btwn β¨π, π
β© β (πLineπ) = (((πRayπ) βͺ {π}) βͺ (πRayπ
)))) |