Step | Hyp | Ref
| Expression |
1 | | simp21l 1288 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π΄) |
2 | | simp21r 1289 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β Β¬ π β€ π) |
3 | | simp23 1206 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π = (0.βπΎ)) |
4 | 3 | oveq1d 7429 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β¨ π) = ((0.βπΎ) β¨ π)) |
5 | | simp32 1208 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π = (0.βπΎ)) |
6 | 5 | oveq1d 7429 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β¨ π) = ((0.βπΎ) β¨ π)) |
7 | 4, 6 | eqtr4d 2770 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β¨ π) = (π β¨ π)) |
8 | | breq1 5145 |
. . . . 5
β’ (π§ = π β (π§ β€ π β π β€ π)) |
9 | 8 | notbid 318 |
. . . 4
β’ (π§ = π β (Β¬ π§ β€ π β Β¬ π β€ π)) |
10 | | oveq2 7422 |
. . . . 5
β’ (π§ = π β (π β¨ π§) = (π β¨ π)) |
11 | | oveq2 7422 |
. . . . 5
β’ (π§ = π β (π β¨ π§) = (π β¨ π)) |
12 | 10, 11 | eqeq12d 2743 |
. . . 4
β’ (π§ = π β ((π β¨ π§) = (π β¨ π§) β (π β¨ π) = (π β¨ π))) |
13 | 9, 12 | anbi12d 630 |
. . 3
β’ (π§ = π β ((Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)) β (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) |
14 | 13 | rspcev 3607 |
. 2
β’ ((π β π΄ β§ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
15 | 1, 2, 7, 14 | syl12anc 836 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π = (0.βπΎ)) β§ (π β π β§ π = (0.βπΎ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |