Step | Hyp | Ref
| Expression |
1 | | simpl1l 1225 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β πΎ β HL) |
2 | | hlatl 37825 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
3 | 1, 2 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β πΎ β AtLat) |
4 | | simpl3l 1229 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β π β π΄) |
5 | | trlne.l |
. . . . 5
β’ β€ =
(leβπΎ) |
6 | | eqid 2737 |
. . . . 5
β’
(0.βπΎ) =
(0.βπΎ) |
7 | | trlne.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
8 | 5, 6, 7 | atnle0 37774 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄) β Β¬ π β€ (0.βπΎ)) |
9 | 3, 4, 8 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β Β¬ π β€ (0.βπΎ)) |
10 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΎ β HL β§ π β π»)) |
11 | | simpl3 1194 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (π β π΄ β§ Β¬ π β€ π)) |
12 | | simpl2 1193 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β πΉ β π) |
13 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = π) |
14 | | trlne.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
15 | | trlne.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
16 | | trlne.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
17 | 5, 6, 7, 14, 15, 16 | trl0 38636 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) = π)) β (π
βπΉ) = (0.βπΎ)) |
18 | 10, 11, 12, 13, 17 | syl112anc 1375 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (π
βπΉ) = (0.βπΎ)) |
19 | 18 | breq2d 5118 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (π β€ (π
βπΉ) β π β€ (0.βπΎ))) |
20 | 9, 19 | mtbird 325 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β Β¬ π β€ (π
βπΉ)) |
21 | 5, 7, 14, 15, 16 | trlne 38651 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β π β (π
βπΉ)) |
22 | 21 | adantr 482 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β π β (π
βπΉ)) |
23 | | simpl1l 1225 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β πΎ β HL) |
24 | 23, 2 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β πΎ β AtLat) |
25 | | simpl3l 1229 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β π β π΄) |
26 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β (πΎ β HL β§ π β π»)) |
27 | | simpl3 1194 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β (π β π΄ β§ Β¬ π β€ π)) |
28 | | simpl2 1193 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β πΉ β π) |
29 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β (πΉβπ) β π) |
30 | 5, 7, 14, 15, 16 | trlat 38635 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) β π)) β (π
βπΉ) β π΄) |
31 | 26, 27, 28, 29, 30 | syl112anc 1375 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β (π
βπΉ) β π΄) |
32 | 5, 7 | atncmp 37777 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄ β§ (π
βπΉ) β π΄) β (Β¬ π β€ (π
βπΉ) β π β (π
βπΉ))) |
33 | 24, 25, 31, 32 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β (Β¬ π β€ (π
βπΉ) β π β (π
βπΉ))) |
34 | 22, 33 | mpbird 257 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β Β¬ π β€ (π
βπΉ)) |
35 | 20, 34 | pm2.61dane 3033 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β Β¬ π β€ (π
βπΉ)) |