Step | Hyp | Ref
| Expression |
1 | | simp1 1134 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β β) |
2 | | simp21 1204 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π΄ β (πΌβπ)) |
3 | | simp32 1208 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β (πΌβπ)) |
4 | | simp22 1205 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π
β (πΌβπ)) |
5 | | broutsideof2 35641 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ))) β (π΄OutsideOfβ¨π, π
β© β (π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)))) |
6 | 1, 2, 3, 4, 5 | syl13anc 1370 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (π΄OutsideOfβ¨π, π
β© β (π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)))) |
7 | 6 | anbi1d 629 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π΄OutsideOfβ¨π, π
β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) |
8 | | simp33 1209 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π β (πΌβπ)) |
9 | | broutsideof2 35641 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π β (πΌβπ) β§ π
β (πΌβπ))) β (π΄OutsideOfβ¨π, π
β© β (π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)))) |
10 | 1, 2, 8, 4, 9 | syl13anc 1370 |
. . . 4
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (π΄OutsideOfβ¨π, π
β© β (π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)))) |
11 | 10 | anbi1d 629 |
. . 3
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π΄OutsideOfβ¨π, π
β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) |
12 | 7, 11 | anbi12d 630 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((π΄OutsideOfβ¨π, π
β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π, π
β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)))) |
13 | | simpll3 1212 |
. . . . . . 7
β’ ((((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) |
14 | | simprl3 1218 |
. . . . . . 7
β’ ((((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) |
15 | 13, 14 | jca 511 |
. . . . . 6
β’ ((((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β ((π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©) β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©))) |
16 | 15 | adantl 481 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) β ((π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©) β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©))) |
17 | | simpll2 1211 |
. . . . . 6
β’ ((((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β π
β π΄) |
18 | 17 | adantl 481 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) β π
β π΄) |
19 | | simp23 1206 |
. . . . . 6
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β π΅ β (πΌβπ)) |
20 | | simp31 1207 |
. . . . . 6
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β πΆ β (πΌβπ)) |
21 | | simprlr 779 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) β β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) |
22 | | simprrr 781 |
. . . . . 6
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) β β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) |
23 | 1, 2, 3, 2, 8, 19,
20, 21, 22 | cgrtr3and 35514 |
. . . . 5
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
24 | 16, 18, 23 | jca32 515 |
. . . 4
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) β (((π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©) β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) |
25 | | simprll 778 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π Btwn β¨π΄, π
β©) |
26 | | simprlr 779 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π Btwn β¨π΄, π
β©) |
27 | | simprrr 781 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
28 | | midofsegid 35623 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β© β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π)) |
29 | 1, 2, 4, 3, 8, 28 | syl122anc 1377 |
. . . . . . . . 9
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β© β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π)) |
30 | 29 | adantr 480 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β© β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π)) |
31 | 25, 26, 27, 30 | mp3and 1461 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π = π) |
32 | 31 | exp32 420 |
. . . . . 6
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π Btwn β¨π΄, π
β© β§ π Btwn β¨π΄, π
β©) β ((π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π))) |
33 | | simprlr 779 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π Btwn β¨π΄, π
β©) |
34 | | simprll 778 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π
Btwn β¨π΄, πβ©) |
35 | 1, 2, 8, 4, 3, 33,
34 | btwnexchand 35545 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π Btwn β¨π΄, πβ©) |
36 | | simprrr 781 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
37 | 1, 2, 3, 8, 35, 36 | endofsegidand 35605 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π Btwn β¨π΄, π
β©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π = π) |
38 | 37 | exp32 420 |
. . . . . 6
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π
Btwn β¨π΄, πβ© β§ π Btwn β¨π΄, π
β©) β ((π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π))) |
39 | | simprll 778 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π Btwn β¨π΄, π
β©) |
40 | | simprlr 779 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π
Btwn β¨π΄, πβ©) |
41 | 1, 2, 3, 4, 8, 39,
40 | btwnexchand 35545 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π Btwn β¨π΄, πβ©) |
42 | | simprrr 781 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
43 | 1, 2, 3, 2, 8, 42 | cgrcomand 35510 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
44 | 1, 2, 8, 3, 41, 43 | endofsegidand 35605 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π = π) |
45 | 44 | eqcomd 2733 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π = π) |
46 | 45 | exp32 420 |
. . . . . 6
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π Btwn β¨π΄, π
β© β§ π
Btwn β¨π΄, πβ©) β ((π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π))) |
47 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β π Btwn β¨π΄, πβ©) |
48 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
49 | 48 | adantl 481 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
50 | 1, 2, 3, 2, 8, 49 | cgrcomand 35510 |
. . . . . . . . . . 11
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
51 | 1, 2, 8, 3, 47, 50 | endofsegidand 35605 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β π = π) |
52 | 51 | eqcomd 2733 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β π = π) |
53 | 52 | expr 456 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β (π Btwn β¨π΄, πβ© β π = π)) |
54 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β π Btwn β¨π΄, πβ©) |
55 | | simplrr 777 |
. . . . . . . . . . 11
β’ ((((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
56 | 55 | adantl 481 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β β¨π΄, πβ©Cgrβ¨π΄, πβ©) |
57 | 1, 2, 3, 8, 54, 56 | endofsegidand 35605 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©)) β§ π Btwn β¨π΄, πβ©)) β π = π) |
58 | 57 | expr 456 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β (π Btwn β¨π΄, πβ© β π = π)) |
59 | | simprrl 780 |
. . . . . . . . . 10
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π
β π΄) |
60 | 59 | necomd 2991 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π΄ β π
) |
61 | | simprll 778 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π
Btwn β¨π΄, πβ©) |
62 | | simprlr 779 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π
Btwn β¨π΄, πβ©) |
63 | | btwnconn1 35620 |
. . . . . . . . . . 11
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ)) β§ (π β (πΌβπ) β§ π β (πΌβπ))) β ((π΄ β π
β§ π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β (π Btwn β¨π΄, πβ© β¨ π Btwn β¨π΄, πβ©))) |
64 | 1, 2, 4, 3, 8, 63 | syl122anc 1377 |
. . . . . . . . . 10
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π΄ β π
β§ π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β (π Btwn β¨π΄, πβ© β¨ π Btwn β¨π΄, πβ©))) |
65 | 64 | adantr 480 |
. . . . . . . . 9
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β ((π΄ β π
β§ π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β (π Btwn β¨π΄, πβ© β¨ π Btwn β¨π΄, πβ©))) |
66 | 60, 61, 62, 65 | mp3and 1461 |
. . . . . . . 8
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β (π Btwn β¨π΄, πβ© β¨ π Btwn β¨π΄, πβ©)) |
67 | 53, 58, 66 | mpjaod 859 |
. . . . . . 7
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π = π) |
68 | 67 | exp32 420 |
. . . . . 6
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((π
Btwn β¨π΄, πβ© β§ π
Btwn β¨π΄, πβ©) β ((π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π))) |
69 | 32, 38, 46, 68 | ccased 1037 |
. . . . 5
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©) β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β ((π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©) β π = π))) |
70 | 69 | imp32 418 |
. . . 4
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©) β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ (π
β π΄ β§ β¨π΄, πβ©Cgrβ¨π΄, πβ©))) β π = π) |
71 | 24, 70 | syldan 590 |
. . 3
β’ (((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β§ (((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©))) β π = π) |
72 | 71 | ex 412 |
. 2
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β ((((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ ((π β π΄ β§ π
β π΄ β§ (π Btwn β¨π΄, π
β© β¨ π
Btwn β¨π΄, πβ©)) β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β π = π)) |
73 | 12, 72 | sylbid 239 |
1
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π
β (πΌβπ) β§ π΅ β (πΌβπ)) β§ (πΆ β (πΌβπ) β§ π β (πΌβπ) β§ π β (πΌβπ))) β (((π΄OutsideOfβ¨π, π
β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©) β§ (π΄OutsideOfβ¨π, π
β© β§ β¨π΄, πβ©Cgrβ¨π΅, πΆβ©)) β π = π)) |