Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π΄ β
(β€β₯β2)) |
2 | | elfzelz 13448 |
. . . . . . . . . . . 12
β’ (πΎ β (0...π) β πΎ β β€) |
3 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((πΎ β (0...π) β§ π β (0...π)) β πΎ β β€) |
4 | 3 | ad2antlr 726 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β πΎ β β€) |
5 | | rmyabs 41311 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€) β (absβ(π΄ Yrm πΎ)) = (π΄ Yrm (absβπΎ))) |
6 | 1, 4, 5 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (absβ(π΄ Yrm πΎ)) = (π΄ Yrm (absβπΎ))) |
7 | 3 | zred 12614 |
. . . . . . . . . . . 12
β’ ((πΎ β (0...π) β§ π β (0...π)) β πΎ β β) |
8 | 7 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β πΎ β β) |
9 | | elfzle1 13451 |
. . . . . . . . . . . . 13
β’ (πΎ β (0...π) β 0 β€ πΎ) |
10 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ ((πΎ β (0...π) β§ π β (0...π)) β 0 β€ πΎ) |
11 | 10 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β 0 β€ πΎ) |
12 | 8, 11 | absidd 15314 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (absβπΎ) = πΎ) |
13 | 12 | oveq2d 7378 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm (absβπΎ)) = (π΄ Yrm πΎ)) |
14 | 6, 13 | eqtrd 2777 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (absβ(π΄ Yrm πΎ)) = (π΄ Yrm πΎ)) |
15 | | elfzelz 13448 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β β€) |
16 | 15 | adantl 483 |
. . . . . . . . . . 11
β’ ((πΎ β (0...π) β§ π β (0...π)) β π β β€) |
17 | 16 | ad2antlr 726 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β β€) |
18 | | rmyabs 41311 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (absβ(π΄ Yrm π)) = (π΄ Yrm (absβπ))) |
19 | 1, 17, 18 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (absβ(π΄ Yrm π)) = (π΄ Yrm (absβπ))) |
20 | 16 | zred 12614 |
. . . . . . . . . . . 12
β’ ((πΎ β (0...π) β§ π β (0...π)) β π β β) |
21 | 20 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β β) |
22 | | elfzle1 13451 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β 0 β€ π) |
23 | 22 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΎ β (0...π) β§ π β (0...π)) β 0 β€ π) |
24 | 23 | ad2antlr 726 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β 0 β€ π) |
25 | 21, 24 | absidd 15314 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (absβπ) = π) |
26 | 25 | oveq2d 7378 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm (absβπ)) = (π΄ Yrm π)) |
27 | 19, 26 | eqtrd 2777 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (absβ(π΄ Yrm π)) = (π΄ Yrm π)) |
28 | 14, 27 | oveq12d 7380 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) = ((π΄ Yrm πΎ) + (π΄ Yrm π))) |
29 | | frmy 41267 |
. . . . . . . . . . . 12
β’
Yrm :((β€β₯β2) Γ
β€)βΆβ€ |
30 | 29 | fovcl 7489 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€) β (π΄ Yrm πΎ) β β€) |
31 | 1, 4, 30 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm πΎ) β β€) |
32 | 31 | zred 12614 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm πΎ) β β) |
33 | 29 | fovcl 7489 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
34 | 1, 17, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm π) β β€) |
35 | 34 | zred 12614 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm π) β β) |
36 | 32, 35 | readdcld 11191 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β β) |
37 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β β) |
38 | 37 | nnzd 12533 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β β€) |
39 | | peano2zm 12553 |
. . . . . . . . . . . 12
β’ (π β β€ β (π β 1) β
β€) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π β 1) β β€) |
41 | 29 | fovcl 7489 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ (π β 1) β β€) β (π΄ Yrm (π β 1)) β
β€) |
42 | 1, 40, 41 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm (π β 1)) β
β€) |
43 | 42 | zred 12614 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm (π β 1)) β
β) |
44 | 29 | fovcl 7489 |
. . . . . . . . . . 11
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm π) β β€) |
45 | 1, 38, 44 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm π) β β€) |
46 | 45 | zred 12614 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm π) β β) |
47 | 43, 46 | readdcld 11191 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) β β) |
48 | | frmx 41266 |
. . . . . . . . . . 11
β’
Xrm :((β€β₯β2) Γ
β€)βΆβ0 |
49 | 48 | fovcl 7489 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β
β0) |
50 | 1, 38, 49 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Xrm π) β
β0) |
51 | 50 | nn0red 12481 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Xrm π) β β) |
52 | | elfzle2 13452 |
. . . . . . . . . . . 12
β’ (πΎ β (0...(π β 1)) β πΎ β€ (π β 1)) |
53 | 52 | adantl 483 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ β (0...(π β 1))) β πΎ β€ (π β 1)) |
54 | | lermy 41308 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€ β§ (π β 1) β β€) β (πΎ β€ (π β 1) β (π΄ Yrm πΎ) β€ (π΄ Yrm (π β 1)))) |
55 | 1, 4, 40, 54 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (πΎ β€ (π β 1) β (π΄ Yrm πΎ) β€ (π΄ Yrm (π β 1)))) |
56 | 55 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ β (0...(π β 1))) β (πΎ β€ (π β 1) β (π΄ Yrm πΎ) β€ (π΄ Yrm (π β 1)))) |
57 | 53, 56 | mpbid 231 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ β (0...(π β 1))) β (π΄ Yrm πΎ) β€ (π΄ Yrm (π β 1))) |
58 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β (0...π)) |
59 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β€ π) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β€ π) |
61 | | lermy 41308 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ π β β€) β (π β€ π β (π΄ Yrm π) β€ (π΄ Yrm π))) |
62 | 1, 17, 38, 61 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π β€ π β (π΄ Yrm π) β€ (π΄ Yrm π))) |
63 | 60, 62 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm π) β€ (π΄ Yrm π)) |
64 | 63 | adantr 482 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ β (0...(π β 1))) β (π΄ Yrm π) β€ (π΄ Yrm π)) |
65 | | le2add 11644 |
. . . . . . . . . . . 12
β’ ((((π΄ Yrm πΎ) β β β§ (π΄ Yrm π) β β) β§ ((π΄ Yrm (π β 1)) β β
β§ (π΄ Yrm
π) β β)) β
(((π΄ Yrm πΎ) β€ (π΄ Yrm (π β 1)) β§ (π΄ Yrm π) β€ (π΄ Yrm π)) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π)))) |
66 | 32, 35, 43, 46, 65 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (((π΄ Yrm πΎ) β€ (π΄ Yrm (π β 1)) β§ (π΄ Yrm π) β€ (π΄ Yrm π)) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π)))) |
67 | 66 | adantr 482 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ β (0...(π β 1))) β (((π΄ Yrm πΎ) β€ (π΄ Yrm (π β 1)) β§ (π΄ Yrm π) β€ (π΄ Yrm π)) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π)))) |
68 | 57, 64, 67 | mp2and 698 |
. . . . . . . . 9
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ β (0...(π β 1))) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π))) |
69 | 31 | zcnd 12615 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm πΎ) β β) |
70 | 34 | zcnd 12615 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm π) β β) |
71 | 69, 70 | addcomd 11364 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) = ((π΄ Yrm π) + (π΄ Yrm πΎ))) |
72 | 71 | adantr 482 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) = ((π΄ Yrm π) + (π΄ Yrm πΎ))) |
73 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΎ β π β πΎ β π) |
74 | 73 | necomd 3000 |
. . . . . . . . . . . . . . . . . 18
β’ (πΎ β π β π β πΎ) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β π β§ πΎ = π) β π β πΎ) |
76 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β π β§ πΎ = π) β πΎ = π) |
77 | 75, 76 | neeqtrd 3014 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β π β§ πΎ = π) β π β π) |
78 | 77 | neneqd 2949 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β π β§ πΎ = π) β Β¬ π = π) |
79 | 78 | adantll 713 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β Β¬ π = π) |
80 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β0) |
81 | | nn0uz 12812 |
. . . . . . . . . . . . . . . . 17
β’
β0 = (β€β₯β0) |
82 | 80, 81 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
(β€β₯β0)) |
83 | 82 | ad4antlr 732 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β π β
(β€β₯β0)) |
84 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β π β (0...π)) |
85 | 84 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β π β (0...π)) |
86 | | fzm1 13528 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β0) β (π β (0...π) β (π β (0...(π β 1)) β¨ π = π))) |
87 | 86 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β0) β§ π β (0...π)) β (π β (0...(π β 1)) β¨ π = π)) |
88 | 83, 85, 87 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β (π β (0...(π β 1)) β¨ π = π)) |
89 | | orel2 890 |
. . . . . . . . . . . . . 14
β’ (Β¬
π = π β ((π β (0...(π β 1)) β¨ π = π) β π β (0...(π β 1)))) |
90 | 79, 88, 89 | sylc 65 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β π β (0...(π β 1))) |
91 | | elfzle2 13452 |
. . . . . . . . . . . . 13
β’ (π β (0...(π β 1)) β π β€ (π β 1)) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . 12
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β π β€ (π β 1)) |
93 | | lermy 41308 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β€ β§ (π β 1) β β€) β (π β€ (π β 1) β (π΄ Yrm π) β€ (π΄ Yrm (π β 1)))) |
94 | 1, 17, 40, 93 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π β€ (π β 1) β (π΄ Yrm π) β€ (π΄ Yrm (π β 1)))) |
95 | 94 | adantr 482 |
. . . . . . . . . . . 12
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β (π β€ (π β 1) β (π΄ Yrm π) β€ (π΄ Yrm (π β 1)))) |
96 | 92, 95 | mpbid 231 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β (π΄ Yrm π) β€ (π΄ Yrm (π β 1))) |
97 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β πΎ β (0...π)) |
98 | | elfzle2 13452 |
. . . . . . . . . . . . . 14
β’ (πΎ β (0...π) β πΎ β€ π) |
99 | 97, 98 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β πΎ β€ π) |
100 | | lermy 41308 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€ β§ π β β€) β (πΎ β€ π β (π΄ Yrm πΎ) β€ (π΄ Yrm π))) |
101 | 1, 4, 38, 100 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (πΎ β€ π β (π΄ Yrm πΎ) β€ (π΄ Yrm π))) |
102 | 99, 101 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm πΎ) β€ (π΄ Yrm π)) |
103 | 102 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β (π΄ Yrm πΎ) β€ (π΄ Yrm π)) |
104 | | le2add 11644 |
. . . . . . . . . . . . 13
β’ ((((π΄ Yrm π) β β β§ (π΄ Yrm πΎ) β β) β§ ((π΄ Yrm (π β 1)) β β
β§ (π΄ Yrm
π) β β)) β
(((π΄ Yrm π) β€ (π΄ Yrm (π β 1)) β§ (π΄ Yrm πΎ) β€ (π΄ Yrm π)) β ((π΄ Yrm π) + (π΄ Yrm πΎ)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π)))) |
105 | 35, 32, 43, 46, 104 | syl22anc 838 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (((π΄ Yrm π) β€ (π΄ Yrm (π β 1)) β§ (π΄ Yrm πΎ) β€ (π΄ Yrm π)) β ((π΄ Yrm π) + (π΄ Yrm πΎ)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π)))) |
106 | 105 | adantr 482 |
. . . . . . . . . . 11
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β (((π΄ Yrm π) β€ (π΄ Yrm (π β 1)) β§ (π΄ Yrm πΎ) β€ (π΄ Yrm π)) β ((π΄ Yrm π) + (π΄ Yrm πΎ)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π)))) |
107 | 96, 103, 106 | mp2and 698 |
. . . . . . . . . 10
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β ((π΄ Yrm π) + (π΄ Yrm πΎ)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π))) |
108 | 72, 107 | eqbrtrd 5132 |
. . . . . . . . 9
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β§ πΎ = π) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π))) |
109 | 37 | nnnn0d 12480 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β
β0) |
110 | 109, 81 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β
(β€β₯β0)) |
111 | | fzm1 13528 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β0) β (πΎ β (0...π) β (πΎ β (0...(π β 1)) β¨ πΎ = π))) |
112 | 111 | biimpa 478 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β0) β§ πΎ β (0...π)) β (πΎ β (0...(π β 1)) β¨ πΎ = π)) |
113 | 110, 97, 112 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (πΎ β (0...(π β 1)) β¨ πΎ = π)) |
114 | 68, 108, 113 | mpjaodan 958 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β€ ((π΄ Yrm (π β 1)) + (π΄ Yrm π))) |
115 | | jm2.24 41316 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) < (π΄ Xrm π)) |
116 | 1, 38, 115 | syl2anc 585 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) < (π΄ Xrm π)) |
117 | 36, 47, 51, 114, 116 | lelttrd 11320 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) < (π΄ Xrm π)) |
118 | 28, 117 | eqbrtrd 5132 |
. . . . . 6
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β ((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π)) |
119 | | simpr 486 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β πΎ β π) |
120 | | rmyeq 41307 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€ β§ π β β€) β (πΎ = π β (π΄ Yrm πΎ) = (π΄ Yrm π))) |
121 | 120 | necon3bid 2989 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€ β§ π β β€) β (πΎ β π β (π΄ Yrm πΎ) β (π΄ Yrm π))) |
122 | 1, 4, 17, 121 | syl3anc 1372 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (πΎ β π β (π΄ Yrm πΎ) β (π΄ Yrm π))) |
123 | 119, 122 | mpbid 231 |
. . . . . 6
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm πΎ) β (π΄ Yrm π)) |
124 | 7 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β πΎ β β) |
125 | | 0red 11165 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β 0 β β) |
126 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β πΎ = -π) |
127 | 22 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β 0 β€ π) |
128 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β π β β) |
129 | 128 | le0neg2d 11734 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β (0 β€ π β -π β€ 0)) |
130 | 127, 129 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β -π β€ 0) |
131 | 130 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β -π β€ 0) |
132 | 126, 131 | eqbrtrd 5132 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β πΎ β€ 0) |
133 | 10 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β 0 β€ πΎ) |
134 | | letri3 11247 |
. . . . . . . . . . . . . 14
β’ ((πΎ β β β§ 0 β
β) β (πΎ = 0
β (πΎ β€ 0 β§ 0
β€ πΎ))) |
135 | 134 | biimpar 479 |
. . . . . . . . . . . . 13
β’ (((πΎ β β β§ 0 β
β) β§ (πΎ β€ 0
β§ 0 β€ πΎ)) β
πΎ = 0) |
136 | 124, 125,
132, 133, 135 | syl22anc 838 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β πΎ = 0) |
137 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β§ πΎ = 0) β πΎ = 0) |
138 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β§ πΎ = 0) β πΎ = -π) |
139 | 138, 137 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β§ πΎ = 0) β -π = 0) |
140 | 128 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β π β β) |
141 | 140 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β§ πΎ = 0) β π β β) |
142 | 141 | negeq0d 11511 |
. . . . . . . . . . . . . 14
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β§ πΎ = 0) β (π = 0 β -π = 0)) |
143 | 139, 142 | mpbird 257 |
. . . . . . . . . . . . 13
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β§ πΎ = 0) β π = 0) |
144 | 137, 143 | eqtr4d 2780 |
. . . . . . . . . . . 12
β’
(((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β§ πΎ = 0) β πΎ = π) |
145 | 136, 144 | mpdan 686 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ = -π) β πΎ = π) |
146 | 145 | ex 414 |
. . . . . . . . . 10
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β (πΎ = -π β πΎ = π)) |
147 | 146 | necon3d 2965 |
. . . . . . . . 9
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β (πΎ β π β πΎ β -π)) |
148 | 147 | imp 408 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β πΎ β -π) |
149 | 58, 15 | syl 17 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β π β β€) |
150 | 149 | znegcld 12616 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β -π β β€) |
151 | | rmyeq 41307 |
. . . . . . . . . 10
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€ β§ -π β β€) β (πΎ = -π β (π΄ Yrm πΎ) = (π΄ Yrm -π))) |
152 | 151 | necon3bid 2989 |
. . . . . . . . 9
β’ ((π΄ β
(β€β₯β2) β§ πΎ β β€ β§ -π β β€) β (πΎ β -π β (π΄ Yrm πΎ) β (π΄ Yrm -π))) |
153 | 1, 4, 150, 152 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (πΎ β -π β (π΄ Yrm πΎ) β (π΄ Yrm -π))) |
154 | 148, 153 | mpbid 231 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm πΎ) β (π΄ Yrm -π)) |
155 | | rmyneg 41281 |
. . . . . . . 8
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Yrm -π) = -(π΄ Yrm π)) |
156 | 1, 17, 155 | syl2anc 585 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm -π) = -(π΄ Yrm π)) |
157 | 154, 156 | neeqtrd 3014 |
. . . . . 6
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (π΄ Yrm πΎ) β -(π΄ Yrm π)) |
158 | 118, 123,
157 | 3jca 1129 |
. . . . 5
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ πΎ β π) β (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) |
159 | 158 | ex 414 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β (πΎ β π β (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
160 | | simplll 774 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β π΄ β
(β€β₯β2)) |
161 | 3 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β πΎ β β€) |
162 | 160, 161,
30 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Yrm πΎ) β β€) |
163 | 162 | zcnd 12615 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Yrm πΎ) β β) |
164 | 16 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β π β β€) |
165 | 160, 164,
33 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Yrm π) β β€) |
166 | 165 | zcnd 12615 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Yrm π) β β) |
167 | 163, 166 | negsubd 11525 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) + -(π΄ Yrm π)) = ((π΄ Yrm πΎ) β (π΄ Yrm π))) |
168 | 167 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + -(π΄ Yrm π))) = (absβ((π΄ Yrm πΎ) β (π΄ Yrm π)))) |
169 | 166 | negcld 11506 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β -(π΄ Yrm π) β β) |
170 | 163, 169 | addcld 11181 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) + -(π΄ Yrm π)) β β) |
171 | 170 | abscld 15328 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + -(π΄ Yrm π))) β β) |
172 | 163 | abscld 15328 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ(π΄ Yrm πΎ)) β β) |
173 | 166 | abscld 15328 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ(π΄ Yrm π)) β β) |
174 | 172, 173 | readdcld 11191 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) β β) |
175 | | nnz 12527 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β€) |
176 | 175 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π΄ β
(β€β₯β2) β§ π β β) β π β β€) |
177 | 176 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β π β β€) |
178 | 49 | nn0zd 12532 |
. . . . . . . . . . . . 13
β’ ((π΄ β
(β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β€) |
179 | 160, 177,
178 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Xrm π) β β€) |
180 | 179 | zred 12614 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Xrm π) β β) |
181 | 163, 169 | abstrid 15348 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + -(π΄ Yrm π))) β€ ((absβ(π΄ Yrm πΎ)) + (absβ-(π΄ Yrm π)))) |
182 | | absneg 15169 |
. . . . . . . . . . . . . . 15
β’ ((π΄ Yrm π) β β β
(absβ-(π΄
Yrm π)) =
(absβ(π΄
Yrm π))) |
183 | 182 | eqcomd 2743 |
. . . . . . . . . . . . . 14
β’ ((π΄ Yrm π) β β β
(absβ(π΄
Yrm π)) =
(absβ-(π΄
Yrm π))) |
184 | 166, 183 | syl 17 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ(π΄ Yrm π)) = (absβ-(π΄ Yrm π))) |
185 | 184 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) = ((absβ(π΄ Yrm πΎ)) + (absβ-(π΄ Yrm π)))) |
186 | 181, 185 | breqtrrd 5138 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + -(π΄ Yrm π))) β€ ((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π)))) |
187 | | simpr1 1195 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π)) |
188 | 171, 174,
180, 186, 187 | lelttrd 11320 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + -(π΄ Yrm π))) < (π΄ Xrm π)) |
189 | 168, 188 | eqbrtrrd 5134 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) β (π΄ Yrm π))) < (π΄ Xrm π)) |
190 | 162, 165 | zsubcld 12619 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) β (π΄ Yrm π)) β β€) |
191 | 190 | zcnd 12615 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) β (π΄ Yrm π)) β β) |
192 | 191 | abscld 15328 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) β (π΄ Yrm π))) β β) |
193 | 192, 180 | ltnled 11309 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((absβ((π΄ Yrm πΎ) β (π΄ Yrm π))) < (π΄ Xrm π) β Β¬ (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β (π΄ Yrm π))))) |
194 | 189, 193 | mpbid 231 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β Β¬ (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β (π΄ Yrm π)))) |
195 | | simpr2 1196 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Yrm πΎ) β (π΄ Yrm π)) |
196 | 163, 166,
195 | subne0d 11528 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) β (π΄ Yrm π)) β 0) |
197 | | dvdsleabs 16200 |
. . . . . . . . 9
β’ (((π΄ Xrm π) β β€ β§ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β β€ β§ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β 0) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β (π΄ Yrm π))))) |
198 | 179, 190,
196, 197 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β (π΄ Yrm π))))) |
199 | 194, 198 | mtod 197 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β Β¬ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π))) |
200 | 163, 166 | subnegd 11526 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) β -(π΄ Yrm π)) = ((π΄ Yrm πΎ) + (π΄ Yrm π))) |
201 | 200 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) β -(π΄ Yrm π))) = (absβ((π΄ Yrm πΎ) + (π΄ Yrm π)))) |
202 | 163, 166 | addcld 11181 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) + (π΄ Yrm π)) β β) |
203 | 202 | abscld 15328 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + (π΄ Yrm π))) β β) |
204 | 163, 166 | abstrid 15348 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + (π΄ Yrm π))) β€ ((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π)))) |
205 | 203, 174,
180, 204, 187 | lelttrd 11320 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) + (π΄ Yrm π))) < (π΄ Xrm π)) |
206 | 201, 205 | eqbrtrd 5132 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) β -(π΄ Yrm π))) < (π΄ Xrm π)) |
207 | 165 | znegcld 12616 |
. . . . . . . . . . . . 13
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β -(π΄ Yrm π) β β€) |
208 | 162, 207 | zsubcld 12619 |
. . . . . . . . . . . 12
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β β€) |
209 | 208 | zcnd 12615 |
. . . . . . . . . . 11
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β β) |
210 | 209 | abscld 15328 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (absβ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β β) |
211 | 210, 180 | ltnled 11309 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((absβ((π΄ Yrm πΎ) β -(π΄ Yrm π))) < (π΄ Xrm π) β Β¬ (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
212 | 206, 211 | mpbid 231 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β Β¬ (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
213 | | simpr3 1197 |
. . . . . . . . . 10
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (π΄ Yrm πΎ) β -(π΄ Yrm π)) |
214 | 163, 169,
213 | subne0d 11528 |
. . . . . . . . 9
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β 0) |
215 | | dvdsleabs 16200 |
. . . . . . . . 9
β’ (((π΄ Xrm π) β β€ β§ ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β β€ β§ ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β 0) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
216 | 179, 208,
214, 215 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)) β (π΄ Xrm π) β€ (absβ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
217 | 212, 216 | mtod 197 |
. . . . . . 7
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β Β¬ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) |
218 | 199, 217 | jca 513 |
. . . . . 6
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β (Β¬ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β§ Β¬ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
219 | | pm4.56 988 |
. . . . . 6
β’ ((Β¬
(π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β§ Β¬ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β Β¬ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
220 | 218, 219 | sylib 217 |
. . . . 5
β’ ((((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β§ (((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π))) β Β¬ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) |
221 | 220 | ex 414 |
. . . 4
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β ((((absβ(π΄ Yrm πΎ)) + (absβ(π΄ Yrm π))) < (π΄ Xrm π) β§ (π΄ Yrm πΎ) β (π΄ Yrm π) β§ (π΄ Yrm πΎ) β -(π΄ Yrm π)) β Β¬ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
222 | 159, 221 | syld 47 |
. . 3
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β (πΎ β π β Β¬ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))))) |
223 | 222 | necon4ad 2963 |
. 2
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π))) β (((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π))) β πΎ = π)) |
224 | 223 | 3impia 1118 |
1
β’ (((π΄ β
(β€β₯β2) β§ π β β) β§ (πΎ β (0...π) β§ π β (0...π)) β§ ((π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β (π΄ Yrm π)) β¨ (π΄ Xrm π) β₯ ((π΄ Yrm πΎ) β -(π΄ Yrm π)))) β πΎ = π) |