Step | Hyp | Ref
| Expression |
1 | | simpl 482 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β β) |
2 | | simpr1 1191 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π β (πΌβπ)) |
3 | | simpr2 1192 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΄ β (πΌβπ)) |
4 | | simpr3 1193 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β π΅ β (πΌβπ)) |
5 | | brsegle2 35614 |
. . . . . 6
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ)) β§ (π β (πΌβπ) β§ π΅ β (πΌβπ))) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β βπ¦ β (πΌβπ)(π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) |
6 | 1, 2, 3, 2, 4, 5 | syl122anc 1376 |
. . . . 5
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β βπ¦ β (πΌβπ)(π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) |
7 | 6 | adantr 480 |
. . . 4
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β βπ¦ β (πΌβπ)(π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) |
8 | | simprl 768 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β πOutsideOfβ¨π΄, π΅β©) |
9 | | outsideofcom 35633 |
. . . . . . . . . . 11
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β πOutsideOfβ¨π΅, π΄β©)) |
10 | 9 | ad2antrr 723 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π΄, π΅β© β πOutsideOfβ¨π΅, π΄β©)) |
11 | 8, 10 | mpbid 231 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β πOutsideOfβ¨π΅, π΄β©) |
12 | | simpll 764 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π β β) |
13 | | simplr1 1212 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π β (πΌβπ)) |
14 | | simplr3 1214 |
. . . . . . . . . . 11
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π΅ β (πΌβπ)) |
15 | 12, 13, 14 | cgrrflxd 35493 |
. . . . . . . . . 10
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β β¨π, π΅β©Cgrβ¨π, π΅β©) |
16 | 15 | adantr 480 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β β¨π, π΅β©Cgrβ¨π, π΅β©) |
17 | 11, 16 | jca 511 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©)) |
18 | | simprrl 778 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΄ Btwn β¨π, π¦β©) |
19 | | simpr 484 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π¦ β (πΌβπ)) |
20 | | simplr2 1213 |
. . . . . . . . . . . . 13
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β π΄ β (πΌβπ)) |
21 | | btwncolinear1 35574 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β (πΌβπ) β§ π¦ β (πΌβπ) β§ π΄ β (πΌβπ))) β (π΄ Btwn β¨π, π¦β© β π Colinear β¨π¦, π΄β©)) |
22 | 12, 13, 19, 20, 21 | syl13anc 1369 |
. . . . . . . . . . . 12
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β (π΄ Btwn β¨π, π¦β© β π Colinear β¨π¦, π΄β©)) |
23 | 22 | adantr 480 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (π΄ Btwn β¨π, π¦β© β π Colinear β¨π¦, π΄β©)) |
24 | 18, 23 | mpd 15 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π Colinear β¨π¦, π΄β©) |
25 | | outsidene1 35628 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β π΄ β π)) |
26 | 25 | ad2antrr 723 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π΄, π΅β© β π΄ β π)) |
27 | 8, 26 | mpd 15 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΄ β π) |
28 | 27 | neneqd 2939 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β Β¬ π΄ = π) |
29 | | df-3an 1086 |
. . . . . . . . . . . . 13
β’ ((πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©) β ((πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β§ π Btwn β¨π¦, π΄β©)) |
30 | | simpr2l 1229 |
. . . . . . . . . . . . . . 15
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π΄ Btwn β¨π, π¦β©) |
31 | 12, 20, 13, 19, 30 | btwncomand 35520 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π΄ Btwn β¨π¦, πβ©) |
32 | | simpr3 1193 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π Btwn β¨π¦, π΄β©) |
33 | | btwnswapid2 35523 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π΄ β (πΌβπ) β§ π¦ β (πΌβπ) β§ π β (πΌβπ))) β ((π΄ Btwn β¨π¦, πβ© β§ π Btwn β¨π¦, π΄β©) β π΄ = π)) |
34 | 12, 20, 19, 13, 33 | syl13anc 1369 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β ((π΄ Btwn β¨π¦, πβ© β§ π Btwn β¨π¦, π΄β©) β π΄ = π)) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β ((π΄ Btwn β¨π¦, πβ© β§ π Btwn β¨π¦, π΄β©) β π΄ = π)) |
36 | 31, 32, 35 | mp2and 696 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©) β§ π Btwn β¨π¦, π΄β©)) β π΄ = π) |
37 | 29, 36 | sylan2br 594 |
. . . . . . . . . . . 12
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ ((πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β§ π Btwn β¨π¦, π΄β©)) β π΄ = π) |
38 | 37 | expr 456 |
. . . . . . . . . . 11
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (π Btwn β¨π¦, π΄β© β π΄ = π)) |
39 | 28, 38 | mtod 197 |
. . . . . . . . . 10
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β Β¬ π Btwn β¨π¦, π΄β©) |
40 | | broutsideof 35626 |
. . . . . . . . . 10
β’ (πOutsideOfβ¨π¦, π΄β© β (π Colinear β¨π¦, π΄β© β§ Β¬ π Btwn β¨π¦, π΄β©)) |
41 | 24, 39, 40 | sylanbrc 582 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β πOutsideOfβ¨π¦, π΄β©) |
42 | | simprrr 779 |
. . . . . . . . 9
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β β¨π, π¦β©Cgrβ¨π, π΅β©) |
43 | 41, 42 | jca 511 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) |
44 | | outsideofeq 35635 |
. . . . . . . . . 10
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π β (πΌβπ)) β§ (π΅ β (πΌβπ) β§ π΅ β (πΌβπ) β§ π¦ β (πΌβπ))) β (((πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©) β§ (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β π΅ = π¦)) |
45 | 12, 13, 20, 13, 14, 14, 19, 44 | syl133anc 1390 |
. . . . . . . . 9
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β (((πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©) β§ (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β π΅ = π¦)) |
46 | 45 | adantr 480 |
. . . . . . . 8
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (((πOutsideOfβ¨π΅, π΄β© β§ β¨π, π΅β©Cgrβ¨π, π΅β©) β§ (πOutsideOfβ¨π¦, π΄β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©)) β π΅ = π¦)) |
47 | 17, 43, 46 | mp2and 696 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΅ = π¦) |
48 | | opeq2 4869 |
. . . . . . . . 9
β’ (π΅ = π¦ β β¨π, π΅β© = β¨π, π¦β©) |
49 | 48 | breq2d 5153 |
. . . . . . . 8
β’ (π΅ = π¦ β (π΄ Btwn β¨π, π΅β© β π΄ Btwn β¨π, π¦β©)) |
50 | 18, 49 | syl5ibrcom 246 |
. . . . . . 7
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β (π΅ = π¦ β π΄ Btwn β¨π, π΅β©)) |
51 | 47, 50 | mpd 15 |
. . . . . 6
β’ ((((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ π¦ β (πΌβπ)) β§ (πOutsideOfβ¨π΄, π΅β© β§ (π΄ Btwn β¨π, π¦β© β§ β¨π, π¦β©Cgrβ¨π, π΅β©))) β π΄ Btwn β¨π, π΅β©) |
52 | 51 | an4s 657 |
. . . . 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 35622 |
. . . 4
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (π΄ Btwn β¨π, π΅β© β β¨π, π΄β© Segβ€ β¨π, π΅β©)) |
56 | 55 | adantr 480 |
. . 3
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (π΄ Btwn β¨π, π΅β© β β¨π, π΄β© Segβ€ β¨π, π΅β©)) |
57 | 54, 56 | impbid 211 |
. 2
β’ (((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β§ πOutsideOfβ¨π΄, π΅β©) β (β¨π, π΄β© Segβ€ β¨π, π΅β© β π΄ Btwn β¨π, π΅β©)) |
58 | 57 | ex 412 |
1
β’ ((π β β β§ (π β (πΌβπ) β§ π΄ β (πΌβπ) β§ π΅ β (πΌβπ))) β (πOutsideOfβ¨π΄, π΅β© β (β¨π, π΄β© Segβ€ β¨π, π΅β© β π΄ Btwn β¨π, π΅β©))) |