Step | Hyp | Ref
| Expression |
1 | | nonconne 2951 |
. 2
β’ Β¬
(π = π β§ π β π) |
2 | | simpl1 1190 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β πΎ β HL) |
3 | | simpl2 1191 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β π β πΆ) |
4 | | eqid 2731 |
. . . . . . . 8
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
5 | | osumcl.c |
. . . . . . . 8
β’ πΆ = (PSubClβπΎ) |
6 | 4, 5 | psubclssatN 39116 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ) β π β (AtomsβπΎ)) |
7 | 2, 3, 6 | syl2anc 583 |
. . . . . 6
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β π β (AtomsβπΎ)) |
8 | | simpl3 1192 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β π β πΆ) |
9 | 4, 5 | psubclssatN 39116 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ) β π β (AtomsβπΎ)) |
10 | 2, 8, 9 | syl2anc 583 |
. . . . . 6
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β π β (AtomsβπΎ)) |
11 | | osumcl.p |
. . . . . . 7
β’ + =
(+πβπΎ) |
12 | 4, 11 | paddssat 38989 |
. . . . . 6
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π + π) β (AtomsβπΎ)) |
13 | 2, 7, 10, 12 | syl3anc 1370 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (π + π) β (AtomsβπΎ)) |
14 | | osumcl.o |
. . . . . 6
β’ β₯ =
(β₯πβπΎ) |
15 | 4, 14 | 2polssN 39090 |
. . . . 5
β’ ((πΎ β HL β§ (π + π) β (AtomsβπΎ)) β (π + π) β ( β₯ β( β₯
β(π + π)))) |
16 | 2, 13, 15 | syl2anc 583 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (π + π) β ( β₯ β( β₯
β(π + π)))) |
17 | | df-pss 3968 |
. . . . . . 7
β’ ((π + π) β ( β₯ β( β₯
β(π + π))) β ((π + π) β ( β₯ β( β₯
β(π + π))) β§ (π + π) β ( β₯ β( β₯
β(π + π))))) |
18 | | pssnel 4471 |
. . . . . . 7
β’ ((π + π) β ( β₯ β( β₯
β(π + π))) β βπ(π β ( β₯ β( β₯
β(π + π))) β§ Β¬ π β (π + π))) |
19 | 17, 18 | sylbir 234 |
. . . . . 6
β’ (((π + π) β ( β₯ β( β₯
β(π + π))) β§ (π + π) β ( β₯ β( β₯
β(π + π)))) β βπ(π β ( β₯ β( β₯
β(π + π))) β§ Β¬ π β (π + π))) |
20 | | df-rex 3070 |
. . . . . 6
β’
(βπ β (
β₯
β( β₯ β(π + π))) Β¬ π β (π + π) β βπ(π β ( β₯ β( β₯
β(π + π))) β§ Β¬ π β (π + π))) |
21 | 19, 20 | sylibr 233 |
. . . . 5
β’ (((π + π) β ( β₯ β( β₯
β(π + π))) β§ (π + π) β ( β₯ β( β₯
β(π + π)))) β βπ β ( β₯ β( β₯
β(π + π))) Β¬ π β (π + π)) |
22 | | eqid 2731 |
. . . . . . . . . . 11
β’
(leβπΎ) =
(leβπΎ) |
23 | | eqid 2731 |
. . . . . . . . . . 11
β’
(joinβπΎ) =
(joinβπΎ) |
24 | | eqid 2731 |
. . . . . . . . . . 11
β’ (π + {π}) = (π + {π}) |
25 | | eqid 2731 |
. . . . . . . . . . 11
β’ ( β₯
β( β₯ β(π + π))) = ( β₯ β( β₯
β(π + π))) |
26 | 22, 23, 4, 11, 14, 5, 24, 25 | osumcllem9N 39139 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β (π + {π}) = π) |
27 | | simp11 1202 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β πΎ β HL) |
28 | | simp12 1203 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β π β πΆ) |
29 | 27, 28, 6 | syl2anc 583 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β π β (AtomsβπΎ)) |
30 | | simp13 1204 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β π β πΆ) |
31 | 27, 30, 9 | syl2anc 583 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β π β (AtomsβπΎ)) |
32 | 13 | 3adantr3 1170 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π))))) β (π + π) β (AtomsβπΎ)) |
33 | 32 | 3adant3 1131 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β (π + π) β (AtomsβπΎ)) |
34 | 4, 14 | polssatN 39083 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π + π) β (AtomsβπΎ)) β ( β₯ β(π + π)) β (AtomsβπΎ)) |
35 | 27, 33, 34 | syl2anc 583 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β ( β₯ β(π + π)) β (AtomsβπΎ)) |
36 | 4, 14 | polssatN 39083 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ ( β₯
β(π + π)) β (AtomsβπΎ)) β ( β₯ β( β₯
β(π + π))) β (AtomsβπΎ)) |
37 | 27, 35, 36 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β ( β₯ β( β₯
β(π + π))) β (AtomsβπΎ)) |
38 | | simp23 1207 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β π β ( β₯ β( β₯
β(π + π)))) |
39 | 37, 38 | sseldd 3984 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β π β (AtomsβπΎ)) |
40 | | simp3 1137 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β Β¬ π β (π + π)) |
41 | 22, 23, 4, 11, 14, 5, 24, 25 | osumcllem10N 39140 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ π β (AtomsβπΎ) β§ Β¬ π β (π + π)) β (π + {π}) β π) |
42 | 27, 29, 31, 39, 40, 41 | syl311anc 1383 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β (π + {π}) β π) |
43 | 26, 42 | pm2.21ddne 3025 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β§ Β¬ π β (π + π)) β (π = π β§ π β π)) |
44 | 43 | 3exp 1118 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((π β ( β₯ βπ) β§ π β β
β§ π β ( β₯ β( β₯
β(π + π)))) β (Β¬ π β (π + π) β (π = π β§ π β π)))) |
45 | 44 | 3expd 1352 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β (π β ( β₯ βπ) β (π β β
β (π β ( β₯ β( β₯
β(π + π))) β (Β¬ π β (π + π) β (π = π β§ π β π)))))) |
46 | 45 | imp32 418 |
. . . . . 6
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (π β ( β₯ β( β₯
β(π + π))) β (Β¬ π β (π + π) β (π = π β§ π β π)))) |
47 | 46 | rexlimdv 3152 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (βπ β ( β₯ β( β₯
β(π + π))) Β¬ π β (π + π) β (π = π β§ π β π))) |
48 | 21, 47 | syl5 34 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (((π + π) β ( β₯ β( β₯
β(π + π))) β§ (π + π) β ( β₯ β( β₯
β(π + π)))) β (π = π β§ π β π))) |
49 | 16, 48 | mpand 692 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β ((π + π) β ( β₯ β( β₯
β(π + π))) β (π = π β§ π β π))) |
50 | 49 | necon1bd 2957 |
. 2
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (Β¬ (π = π β§ π β π) β (π + π) = ( β₯ β( β₯
β(π + π))))) |
51 | 1, 50 | mpi 20 |
1
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (π + π) = ( β₯ β( β₯
β(π + π)))) |