Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) β πΎ β HL) |
2 | | simp1 1137 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β πΎ β HL) |
3 | | 2polss.a |
. . . . . . . . 9
β’ π΄ = (AtomsβπΎ) |
4 | | 2polss.p |
. . . . . . . . 9
β’ β₯ =
(β₯πβπΎ) |
5 | 3, 4 | polssatN 38779 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
6 | 5 | 3adant2 1132 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ βπ) β π΄) |
7 | 3, 4 | polssatN 38779 |
. . . . . . 7
β’ ((πΎ β HL β§ ( β₯
βπ) β π΄) β ( β₯ β( β₯
βπ)) β π΄) |
8 | 2, 6, 7 | syl2anc 585 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β( β₯
βπ)) β π΄) |
9 | 8 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) β ( β₯ β( β₯
βπ)) β π΄) |
10 | | simpr 486 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) β ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) |
11 | 3, 4 | polcon3N 38788 |
. . . . 5
β’ ((πΎ β HL β§ ( β₯
β( β₯ βπ)) β π΄ β§ ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) β ( β₯ β( β₯
β( β₯ βπ))) β ( β₯ β( β₯
β( β₯ βπ)))) |
12 | 1, 9, 10, 11 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) β ( β₯ β( β₯
β( β₯ βπ))) β ( β₯ β( β₯
β( β₯ βπ)))) |
13 | 12 | ex 414 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ)) β ( β₯ β( β₯
β( β₯ βπ))) β ( β₯ β( β₯
β( β₯ βπ))))) |
14 | 3, 4 | 3polN 38787 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯
β( β₯ βπ))) = ( β₯ βπ)) |
15 | 14 | 3adant2 1132 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β( β₯
β( β₯ βπ))) = ( β₯ βπ)) |
16 | 3, 4 | 3polN 38787 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯
β( β₯ βπ))) = ( β₯ βπ)) |
17 | 16 | 3adant3 1133 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β( β₯
β( β₯ βπ))) = ( β₯ βπ)) |
18 | 15, 17 | sseq12d 4016 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( β₯ β( β₯
β( β₯ βπ))) β ( β₯ β( β₯
β( β₯ βπ))) β ( β₯ βπ) β ( β₯ βπ))) |
19 | 13, 18 | sylibd 238 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ)) β ( β₯ βπ) β ( β₯ βπ))) |
20 | | simpl1 1192 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ βπ) β ( β₯ βπ)) β πΎ β HL) |
21 | 3, 4 | polssatN 38779 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
22 | 21 | 3adant3 1133 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ βπ) β π΄) |
23 | 22 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ βπ) β ( β₯ βπ)) β ( β₯ βπ) β π΄) |
24 | | simpr 486 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ βπ) β ( β₯ βπ)) β ( β₯ βπ) β ( β₯ βπ)) |
25 | 3, 4 | polcon3N 38788 |
. . . 4
β’ ((πΎ β HL β§ ( β₯
βπ) β π΄ β§ ( β₯ βπ) β ( β₯ βπ)) β ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) |
26 | 20, 23, 24, 25 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ( β₯ βπ) β ( β₯ βπ)) β ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ))) |
27 | 26 | ex 414 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( β₯ βπ) β ( β₯ βπ) β ( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ)))) |
28 | 19, 27 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( β₯ β( β₯
βπ)) β ( β₯
β( β₯ βπ)) β ( β₯ βπ) β ( β₯ βπ))) |