Step | Hyp | Ref
| Expression |
1 | | sscon 4139 |
. . . . . . 7
β’ (π β π β (π β π) β (π β π)) |
2 | 1 | adantl 483 |
. . . . . 6
β’ ((π β π β§ π β π) β (π β π) β (π β π)) |
3 | | difss 4132 |
. . . . . 6
β’ (π β π) β π |
4 | 2, 3 | jctil 521 |
. . . . 5
β’ ((π β π β§ π β π) β ((π β π) β π β§ (π β π) β (π β π))) |
5 | | clscld.1 |
. . . . . . 7
β’ π = βͺ
π½ |
6 | 5 | clsss 22558 |
. . . . . 6
β’ ((π½ β Top β§ (π β π) β π β§ (π β π) β (π β π)) β ((clsβπ½)β(π β π)) β ((clsβπ½)β(π β π))) |
7 | 6 | 3expb 1121 |
. . . . 5
β’ ((π½ β Top β§ ((π β π) β π β§ (π β π) β (π β π))) β ((clsβπ½)β(π β π)) β ((clsβπ½)β(π β π))) |
8 | 4, 7 | sylan2 594 |
. . . 4
β’ ((π½ β Top β§ (π β π β§ π β π)) β ((clsβπ½)β(π β π)) β ((clsβπ½)β(π β π))) |
9 | 8 | sscond 4142 |
. . 3
β’ ((π½ β Top β§ (π β π β§ π β π)) β (π β ((clsβπ½)β(π β π))) β (π β ((clsβπ½)β(π β π)))) |
10 | | sstr2 3990 |
. . . . 5
β’ (π β π β (π β π β π β π)) |
11 | 10 | impcom 409 |
. . . 4
β’ ((π β π β§ π β π) β π β π) |
12 | 5 | ntrval2 22555 |
. . . 4
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) = (π β ((clsβπ½)β(π β π)))) |
13 | 11, 12 | sylan2 594 |
. . 3
β’ ((π½ β Top β§ (π β π β§ π β π)) β ((intβπ½)βπ) = (π β ((clsβπ½)β(π β π)))) |
14 | 5 | ntrval2 22555 |
. . . 4
β’ ((π½ β Top β§ π β π) β ((intβπ½)βπ) = (π β ((clsβπ½)β(π β π)))) |
15 | 14 | adantrr 716 |
. . 3
β’ ((π½ β Top β§ (π β π β§ π β π)) β ((intβπ½)βπ) = (π β ((clsβπ½)β(π β π)))) |
16 | 9, 13, 15 | 3sstr4d 4030 |
. 2
β’ ((π½ β Top β§ (π β π β§ π β π)) β ((intβπ½)βπ) β ((intβπ½)βπ)) |
17 | 16 | 3impb 1116 |
1
β’ ((π½ β Top β§ π β π β§ π β π) β ((intβπ½)βπ) β ((intβπ½)βπ)) |