Step | Hyp | Ref
| Expression |
1 | | acongrep 41347 |
. . . 4
β’ ((π β β β§ π β β€) β
βπ β (0...π)((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) |
2 | 1 | ad2ant2l 745 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β βπ β (0...π)((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) |
3 | | acongrep 41347 |
. . . . . . 7
β’ ((π β β β§ πΎ β β€) β
βπ β (0...π)((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) |
4 | 3 | ad2ant2lr 747 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β βπ β (0...π)((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) |
5 | | 2z 12540 |
. . . . . . . . . . 11
β’ 2 β
β€ |
6 | | simpl1l 1225 |
. . . . . . . . . . . 12
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (π΄ β (β€β₯β2)
β§ π β
β)) |
7 | | nnz 12525 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β€) |
8 | 7 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β β€) |
9 | 6, 8 | syl 17 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π β β€) |
10 | | zmulcl 12557 |
. . . . . . . . . . 11
β’ ((2
β β€ β§ π
β β€) β (2 Β· π) β β€) |
11 | 5, 9, 10 | sylancr 588 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (2 Β· π) β β€) |
12 | | simplrl 776 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β πΎ β β€) |
13 | 12 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β πΎ β β€) |
14 | | simpl3l 1229 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π β (0...π)) |
15 | 14 | elfzelzd 13448 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π β β€) |
16 | | simplrr 777 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π β β€) |
17 | 16 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π β β€) |
18 | | simpl2r 1228 |
. . . . . . . . . . . 12
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) |
19 | | simpl2l 1227 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π β (0...π)) |
20 | | simplll 774 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π΄ β
(β€β₯β2)) |
21 | 20 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π΄ β
(β€β₯β2)) |
22 | | frmx 41280 |
. . . . . . . . . . . . . . . . . 18
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
23 | 22 | fovcl 7485 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
24 | 23 | nn0zd 12530 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β€) |
25 | 21, 9, 24 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (π΄ Xrm π) β β€) |
26 | 19 | elfzelzd 13448 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π β β€) |
27 | | frmy 41281 |
. . . . . . . . . . . . . . . . 17
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
28 | 27 | fovcl 7485 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
29 | 21, 26, 28 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (π΄ Yrm π) β β€) |
30 | 27 | fovcl 7485 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
31 | 21, 17, 30 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (π΄ Yrm π) β β€) |
32 | 27 | fovcl 7485 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
33 | 21, 15, 32 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (π΄ Yrm π) β β€) |
34 | 27 | fovcl 7485 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€) β (π΄ Yrm πΎ) β β€) |
35 | 21, 13, 34 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (π΄ Yrm πΎ) β β€) |
36 | | jm2.26a 41367 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (π β β€ β§ πΎ β β€)) β (((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm πΎ)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm πΎ))))) |
37 | 21, 9, 26, 13, 36 | syl22anc 838 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm πΎ)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm πΎ))))) |
38 | 18, 37 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm πΎ)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm πΎ)))) |
39 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
40 | | acongtr 41345 |
. . . . . . . . . . . . . . . 16
β’ ((((π΄ Xrm π) β β€ β§ (π΄ Yrm π) β β€) β§ ((π΄ Yrm πΎ) β β€ β§ (π΄ Yrm π) β β€) β§ (((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm πΎ)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm πΎ))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π)))) |
41 | 25, 29, 35, 31, 38, 39, 40 | syl222anc 1387 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π)))) |
42 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) |
43 | | acongsym 41343 |
. . . . . . . . . . . . . . . . 17
β’ ((((2
Β· π) β β€
β§ π β β€
β§ π β β€)
β§ ((2 Β· π)
β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) β ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) |
44 | 11, 15, 17, 42, 43 | syl31anc 1374 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) |
45 | | jm2.26a 41367 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (π β β€ β§ π β β€)) β (((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π))))) |
46 | 21, 9, 17, 15, 45 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π))))) |
47 | 44, 46 | mpd 15 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π)))) |
48 | | acongtr 41345 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ Xrm π) β β€ β§ (π΄ Yrm π) β β€) β§ ((π΄ Yrm π) β β€ β§ (π΄ Yrm π) β β€) β§ (((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π))))) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π)))) |
49 | 25, 29, 31, 33, 41, 47, 48 | syl222anc 1387 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π)))) |
50 | | jm2.26lem3 41368 |
. . . . . . . . . . . . . 14
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (π β (0...π) β§ π β (0...π)) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm π) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm π) β -(π΄ Yrm π)))) β π = π) |
51 | 6, 19, 14, 49, 50 | syl121anc 1376 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β π = π) |
52 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = π β π = π) |
53 | | eqidd 2734 |
. . . . . . . . . . . . . 14
β’ (π = π β πΎ = πΎ) |
54 | 52, 53 | acongeq12d 41346 |
. . . . . . . . . . . . 13
β’ (π = π β (((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)) β ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)))) |
55 | 51, 54 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β (((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)) β ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)))) |
56 | 18, 55 | mpbid 231 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) |
57 | | acongsym 41343 |
. . . . . . . . . . 11
β’ ((((2
Β· π) β β€
β§ π β β€
β§ πΎ β β€)
β§ ((2 Β· π)
β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π))) |
58 | 11, 15, 13, 56, 57 | syl31anc 1374 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π))) |
59 | | acongtr 41345 |
. . . . . . . . . 10
β’ ((((2
Β· π) β β€
β§ πΎ β β€)
β§ (π β β€
β§ π β β€)
β§ (((2 Β· π)
β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π))) |
60 | 11, 13, 15, 17, 58, 42, 59 | syl222anc 1387 |
. . . . . . . . 9
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β§ (π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)))) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π))) |
61 | 60 | 3exp1 1353 |
. . . . . . . 8
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β ((π β (0...π) β§ ((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ))) β ((π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)))))) |
62 | 61 | expd 417 |
. . . . . . 7
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β (π β (0...π) β (((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)) β ((π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π))))))) |
63 | 62 | rexlimdv 3147 |
. . . . . 6
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β (βπ β (0...π)((2 Β· π) β₯ (π β πΎ) β¨ (2 Β· π) β₯ (π β -πΎ)) β ((π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)))))) |
64 | 4, 63 | mpd 15 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β ((π β (0...π) β§ ((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π))) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π))))) |
65 | 64 | expd 417 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β (π β (0...π) β (((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)))))) |
66 | 65 | rexlimdv 3147 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β (βπ β (0...π)((2 Β· π) β₯ (π β π) β¨ (2 Β· π) β₯ (π β -π)) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π))))) |
67 | 2, 66 | mpd 15 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)))) |
68 | | jm2.26a 41367 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β (((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
69 | 7, 68 | sylanl2 680 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β (((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
70 | 67, 69 | impbid 211 |
1
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β β€ β§ π β β€)) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)))) |