Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β β) |
2 | | simpr1 1195 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β (πΌβπ)) |
3 | | simpr2 1196 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΄ β (πΌβπ)) |
4 | | simpr3 1197 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΅ β (πΌβπ)) |
5 | | brsegle2 34740 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ)) β§ (π β (πΌβπ) β§ π΅ β (πΌβπ))) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β βπ¦ β (πΌβπ)(π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) |
6 | 1, 2, 3, 2, 4, 5 | syl122anc 1380 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β βπ¦ β (πΌβπ)(π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) |
7 | 6 | adantr 482 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β βπ¦ β (πΌβπ)(π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) |
8 | | simprl 770 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β πOutsideOfβ¨π΄, π΅β©) |
9 | | outsideofcom 34759 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β πOutsideOfβ¨π΅, π΄β©)) |
10 | 9 | ad2antrr 725 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π΄, π΅β© β πOutsideOfβ¨π΅, π΄β©)) |
11 | 8, 10 | mpbid 231 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β πOutsideOfβ¨π΅, π΄β©) |
12 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π β β) |
13 | | simplr1 1216 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π β (πΌβπ)) |
14 | | simplr3 1218 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π΅ β (πΌβπ)) |
15 | 12, 13, 14 | cgrrflxd 34619 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β β¨π, π΅β©Cgrβ¨π, π΅β©) |
16 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β β¨π, π΅β©Cgrβ¨π, π΅β©) |
17 | 11, 16 | jca 513 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©)) |
18 | | simprrl 780 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΄ Btwn β¨π, π¦β©) |
19 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π¦ β (πΌβπ)) |
20 | | simplr2 1217 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π΄ β (πΌβπ)) |
21 | | btwncolinear1 34700 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β (πΌβπ) β§ π¦ β (πΌβπ) β§ π΄ β (πΌβπ))) β (π΄ Btwn β¨π, π¦β© β π Colinear β¨π¦, π΄β©)) |
22 | 12, 13, 19, 20, 21 | syl13anc 1373 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β (π΄ Btwn β¨π, π¦β© β π Colinear β¨π¦, π΄β©)) |
23 | 22 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (π΄ Btwn β¨π, π¦β© β π Colinear β¨π¦, π΄β©)) |
24 | 18, 23 | mpd 15 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π Colinear β¨π¦, π΄β©) |
25 | | outsidene1 34754 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β π΄ β π)) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π΄, π΅β© β π΄ β π)) |
27 | 8, 26 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΄ β π) |
28 | 27 | neneqd 2945 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β Β¬ π΄ = π) |
29 | | df-3an 1090 |
. . . . . . . . . . . . 13
β’ ((πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©) β ((πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β§ π Btwn β¨π¦, π΄β©)) |
30 | | simpr2l 1233 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π΄ Btwn β¨π, π¦β©) |
31 | 12, 20, 13, 19, 30 | btwncomand 34646 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π΄ Btwn β¨π¦, πβ©) |
32 | | simpr3 1197 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π Btwn β¨π¦, π΄β©) |
33 | | btwnswapid2 34649 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π β (πΌβπ))) β ((π΄ Btwn β¨π¦, πβ© β§ π Btwn β¨π¦, π΄β©) β π΄ = π)) |
34 | 12, 20, 19, 13, 33 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β ((π΄ Btwn β¨π¦, πβ© β§ π Btwn β¨π¦, π΄β©) β π΄ = π)) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β ((π΄ Btwn β¨π¦, πβ© β§ π Btwn β¨π¦, π΄β©) β π΄ = π)) |
36 | 31, 32, 35 | mp2and 698 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π΄ = π) |
37 | 29, 36 | sylan2br 596 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ ((πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β§ π Btwn β¨π¦, π΄β©)) β π΄ = π) |
38 | 37 | expr 458 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (π Btwn β¨π¦, π΄β© β π΄ = π)) |
39 | 28, 38 | mtod 197 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β Β¬ π Btwn β¨π¦, π΄β©) |
40 | | broutsideof 34752 |
. . . . . . . . . 10
β’ (πOutsideOfβ¨π¦, π΄β© β (π Colinear β¨π¦, π΄β© β§ Β¬ π Btwn β¨π¦, π΄β©)) |
41 | 24, 39, 40 | sylanbrc 584 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β πOutsideOfβ¨π¦, π΄β©) |
42 | | simprrr 781 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β β¨π, π¦β©Cgrβ¨π, π΅β©) |
43 | 41, 42 | jca 513 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) |
44 | | outsideofeq 34761 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π¦ β (πΌβπ))) β (((πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©) β§ (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β π΅ = π¦)) |
45 | 12, 13, 20, 13, 14, 14, 19, 44 | syl133anc 1394 |
. . . . . . . . 9
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β (((πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©) β§ (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β π΅ = π¦)) |
46 | 45 | adantr 482 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (((πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©) β§ (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β π΅ = π¦)) |
47 | 17, 43, 46 | mp2and 698 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΅ = π¦) |
48 | | opeq2 4832 |
. . . . . . . . 9
β’ (π΅ = π¦ β β¨π, π΅β© = β¨π, π¦β©) |
49 | 48 | breq2d 5118 |
. . . . . . . 8
β’ (π΅ = π¦ β (π΄ Btwn β¨π, π΅β© β π΄ Btwn β¨π, π¦β©)) |
50 | 18, 49 | syl5ibrcom 247 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (π΅ = π¦ β π΄ Btwn β¨π, π΅β©)) |
51 | 47, 50 | mpd 15 |
. . . . . 6
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΄ Btwn β¨π, π΅β©) |
52 | 51 | an4s 659 |
. . . . 5
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β§ (π¦ β (πΌβπ) β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΄ Btwn β¨π, π΅β©) |
53 | 52 | rexlimdvaa 3150 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (βπ¦ β (πΌβπ)(π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β π΄ Btwn β¨π, π΅β©)) |
54 | 7, 53 | sylbid 239 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β π΄ Btwn β¨π, π΅β©)) |
55 | | btwnsegle 34748 |
. . . 4
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ Btwn β¨π, π΅β© β β¨π, π΄β© Segβ€ β¨π, π΅β©)) |
56 | 55 | adantr 482 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (π΄ Btwn β¨π, π΅β© β β¨π, π΄β© Segβ€ β¨π, π΅β©)) |
57 | 54, 56 | impbid 211 |
. 2
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β π΄ Btwn β¨π, π΅β©)) |
58 | 57 | ex 414 |
1
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (β¨π, π΄β© Segβ€ β¨π, π΅β© β π΄ Btwn β¨π, π΅β©))) |