Step | Hyp | Ref
| Expression |
1 | | 2z 12542 |
. . . . 5
β’ 2 β
β€ |
2 | | simplr 768 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β π β β€) |
3 | | zmulcl 12559 |
. . . . 5
β’ ((2
β β€ β§ π
β β€) β (2 Β· π) β β€) |
4 | 1, 2, 3 | sylancr 588 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β (2 Β· π) β
β€) |
5 | | zsubcl 12552 |
. . . . 5
β’ ((πΎ β β€ β§ π β β€) β (πΎ β π) β β€) |
6 | 5 | adantl 483 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β (πΎ β π) β β€) |
7 | | divides 16145 |
. . . 4
β’ (((2
Β· π) β β€
β§ (πΎ β π) β β€) β ((2
Β· π) β₯ (πΎ β π) β βπ β β€ (π Β· (2 Β· π)) = (πΎ β π))) |
8 | 4, 6, 7 | syl2anc 585 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β ((2 Β· π) β₯ (πΎ β π) β βπ β β€ (π Β· (2 Β· π)) = (πΎ β π))) |
9 | | simplll 774 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β π΄ β
(β€β₯β2)) |
10 | | simplrr 777 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β π β β€) |
11 | | simpllr 775 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β π β β€) |
12 | | simpr 486 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β π β β€) |
13 | | jm2.25 41352 |
. . . . . . 7
β’ ((π΄ β
(β€β₯β2) β§ (π β β€ β§ π β β€) β§ π β β€) β ((π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β -(π΄ Yrm π)))) |
14 | 9, 10, 11, 12, 13 | syl121anc 1376 |
. . . . . 6
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β ((π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β -(π΄ Yrm π)))) |
15 | 14 | adantr 482 |
. . . . 5
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β -(π΄ Yrm π)))) |
16 | | oveq2 7370 |
. . . . . . . 8
β’ ((π Β· (2 Β· π)) = (πΎ β π) β (π + (π Β· (2 Β· π))) = (π + (πΎ β π))) |
17 | 16 | oveq2d 7378 |
. . . . . . 7
β’ ((π Β· (2 Β· π)) = (πΎ β π) β (π΄ Yrm (π + (π Β· (2 Β· π)))) = (π΄ Yrm (π + (πΎ β π)))) |
18 | | zcn 12511 |
. . . . . . . . . 10
β’ (π β β€ β π β
β) |
19 | | zcn 12511 |
. . . . . . . . . 10
β’ (πΎ β β€ β πΎ β
β) |
20 | | pncan3 11416 |
. . . . . . . . . 10
β’ ((π β β β§ πΎ β β) β (π + (πΎ β π)) = πΎ) |
21 | 18, 19, 20 | syl2anr 598 |
. . . . . . . . 9
β’ ((πΎ β β€ β§ π β β€) β (π + (πΎ β π)) = πΎ) |
22 | 21 | ad2antlr 726 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (π + (πΎ β π)) = πΎ) |
23 | 22 | oveq2d 7378 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (π΄ Yrm (π + (πΎ β π))) = (π΄ Yrm πΎ)) |
24 | 17, 23 | sylan9eqr 2799 |
. . . . . 6
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β π)) β (π΄ Yrm (π + (π Β· (2 Β· π)))) = (π΄ Yrm πΎ)) |
25 | | eqidd 2738 |
. . . . . 6
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β π)) β (π΄ Yrm π) = (π΄ Yrm π)) |
26 | 24, 25 | acongeq12d 41332 |
. . . . 5
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β π)) β (((π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (π + (π Β· (2 Β· π)))) β -(π΄ Yrm π))) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
27 | 15, 26 | mpbid 231 |
. . . 4
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
28 | 27 | rexlimdva2 3155 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β (βπ β β€ (π Β· (2 Β· π)) = (πΎ β π) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
29 | 8, 28 | sylbid 239 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β ((2 Β· π) β₯ (πΎ β π) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
30 | | simprl 770 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β πΎ β β€) |
31 | | znegcl 12545 |
. . . . . 6
β’ (π β β€ β -π β
β€) |
32 | 31 | ad2antll 728 |
. . . . 5
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β -π β β€) |
33 | 30, 32 | zsubcld 12619 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β (πΎ β -π) β β€) |
34 | | divides 16145 |
. . . 4
β’ (((2
Β· π) β β€
β§ (πΎ β -π) β β€) β ((2
Β· π) β₯ (πΎ β -π) β βπ β β€ (π Β· (2 Β· π)) = (πΎ β -π))) |
35 | 4, 33, 34 | syl2anc 585 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β ((2 Β· π) β₯ (πΎ β -π) β βπ β β€ (π Β· (2 Β· π)) = (πΎ β -π))) |
36 | | frmx 41266 |
. . . . . . . . . 10
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
37 | 36 | fovcl 7489 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
38 | 37 | nn0zd 12532 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β€) |
39 | 9, 11, 38 | syl2anc 585 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (π΄ Xrm π) β β€) |
40 | | simplrl 776 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β πΎ β β€) |
41 | | frmy 41267 |
. . . . . . . . 9
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
42 | 41 | fovcl 7489 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€) β (π΄ Yrm πΎ) β β€) |
43 | 9, 40, 42 | syl2anc 585 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (π΄ Yrm πΎ) β β€) |
44 | 41 | fovcl 7489 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
45 | 9, 10, 44 | syl2anc 585 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (π΄ Yrm π) β β€) |
46 | 39, 43, 45 | 3jca 1129 |
. . . . . 6
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β ((π΄ Xrm π) β β€ β§ (π΄ Yrm πΎ) β β€ β§ (π΄ Yrm π) β β€)) |
47 | 46 | adantr 482 |
. . . . 5
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β -π)) β ((π΄ Xrm π) β β€ β§ (π΄ Yrm πΎ) β β€ β§ (π΄ Yrm π) β β€)) |
48 | 32 | adantr 482 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β -π β β€) |
49 | | jm2.25 41352 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ (-π β β€ β§ π β β€) β§ π β β€) β ((π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β (π΄ Yrm -π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β -(π΄ Yrm -π)))) |
50 | 9, 48, 11, 12, 49 | syl121anc 1376 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β ((π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β (π΄ Yrm -π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β -(π΄ Yrm -π)))) |
51 | 50 | adantr 482 |
. . . . . 6
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β (π΄ Yrm -π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β -(π΄ Yrm -π)))) |
52 | | oveq2 7370 |
. . . . . . . . 9
β’ ((π Β· (2 Β· π)) = (πΎ β -π) β (-π + (π Β· (2 Β· π))) = (-π + (πΎ β -π))) |
53 | 52 | oveq2d 7378 |
. . . . . . . 8
β’ ((π Β· (2 Β· π)) = (πΎ β -π) β (π΄ Yrm (-π + (π Β· (2 Β· π)))) = (π΄ Yrm (-π + (πΎ β -π)))) |
54 | 18 | negcld 11506 |
. . . . . . . . . . 11
β’ (π β β€ β -π β
β) |
55 | | pncan3 11416 |
. . . . . . . . . . 11
β’ ((-π β β β§ πΎ β β) β (-π + (πΎ β -π)) = πΎ) |
56 | 54, 19, 55 | syl2anr 598 |
. . . . . . . . . 10
β’ ((πΎ β β€ β§ π β β€) β (-π + (πΎ β -π)) = πΎ) |
57 | 56 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (-π + (πΎ β -π)) = πΎ) |
58 | 57 | oveq2d 7378 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (π΄ Yrm (-π + (πΎ β -π))) = (π΄ Yrm πΎ)) |
59 | 53, 58 | sylan9eqr 2799 |
. . . . . . 7
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β -π)) β (π΄ Yrm (-π + (π Β· (2 Β· π)))) = (π΄ Yrm πΎ)) |
60 | | rmyneg 41281 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm -π) = -(π΄ Yrm π)) |
61 | 9, 10, 60 | syl2anc 585 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β (π΄ Yrm -π) = -(π΄ Yrm π)) |
62 | 61 | adantr 482 |
. . . . . . 7
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β -π)) β (π΄ Yrm -π) = -(π΄ Yrm π)) |
63 | 59, 62 | acongeq12d 41332 |
. . . . . 6
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β -π)) β (((π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β (π΄ Yrm -π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm (-π + (π Β· (2 Β· π)))) β -(π΄ Yrm -π))) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β --(π΄ Yrm π))))) |
64 | 51, 63 | mpbid 231 |
. . . . 5
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β --(π΄ Yrm π)))) |
65 | | acongneg2 41330 |
. . . . 5
β’ ((((π΄ Xrm π) β β€ β§ (π΄ Yrm πΎ) β β€ β§ (π΄ Yrm π) β β€) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β --(π΄ Yrm π)))) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
66 | 47, 64, 65 | syl2anc 585 |
. . . 4
β’
(((((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β§ π β β€) β§ (π Β· (2 Β· π)) = (πΎ β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
67 | 66 | rexlimdva2 3155 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β (βπ β β€ (π Β· (2 Β· π)) = (πΎ β -π) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
68 | 35, 67 | sylbid 239 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β ((2 Β· π) β₯ (πΎ β -π) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
69 | 29, 68 | jaod 858 |
1
β’ (((π΄ β
(β€β₯β2) β§ π β β€) β§ (πΎ β β€ β§ π β β€)) β (((2 Β· π) β₯ (πΎ β π) β¨ (2 Β· π) β₯ (πΎ β -π)) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |