Step | Hyp | Ref
| Expression |
1 | | monoord2.1 |
. . . 4
β’ (π β π β (β€β₯βπ)) |
2 | | monoord2.2 |
. . . . . . 7
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
3 | 2 | renegcld 8337 |
. . . . . 6
β’ ((π β§ π β (π...π)) β -(πΉβπ) β β) |
4 | | eqid 2177 |
. . . . . 6
β’ (π β (π...π) β¦ -(πΉβπ)) = (π β (π...π) β¦ -(πΉβπ)) |
5 | 3, 4 | fmptd 5671 |
. . . . 5
β’ (π β (π β (π...π) β¦ -(πΉβπ)):(π...π)βΆβ) |
6 | 5 | ffvelcdmda 5652 |
. . . 4
β’ ((π β§ π β (π...π)) β ((π β (π...π) β¦ -(πΉβπ))βπ) β β) |
7 | | monoord2.3 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
8 | 7 | ralrimiva 2550 |
. . . . . . . 8
β’ (π β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
9 | | oveq1 5882 |
. . . . . . . . . . 11
β’ (π = π β (π + 1) = (π + 1)) |
10 | 9 | fveq2d 5520 |
. . . . . . . . . 10
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
11 | | fveq2 5516 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
12 | 10, 11 | breq12d 4017 |
. . . . . . . . 9
β’ (π = π β ((πΉβ(π + 1)) β€ (πΉβπ) β (πΉβ(π + 1)) β€ (πΉβπ))) |
13 | 12 | cbvralv 2704 |
. . . . . . . 8
β’
(βπ β
(π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ) β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
14 | 8, 13 | sylib 122 |
. . . . . . 7
β’ (π β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
15 | 14 | r19.21bi 2565 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
16 | | fveq2 5516 |
. . . . . . . . 9
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
17 | 16 | eleq1d 2246 |
. . . . . . . 8
β’ (π = (π + 1) β ((πΉβπ) β β β (πΉβ(π + 1)) β β)) |
18 | 2 | ralrimiva 2550 |
. . . . . . . . 9
β’ (π β βπ β (π...π)(πΉβπ) β β) |
19 | 18 | adantr 276 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β βπ β (π...π)(πΉβπ) β β) |
20 | | fzp1elp1 10075 |
. . . . . . . . . 10
β’ (π β (π...(π β 1)) β (π + 1) β (π...((π β 1) + 1))) |
21 | 20 | adantl 277 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β (π...((π β 1) + 1))) |
22 | | eluzelz 9537 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β π β β€) |
23 | 1, 22 | syl 14 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
24 | 23 | zcnd 9376 |
. . . . . . . . . . . 12
β’ (π β π β β) |
25 | | ax-1cn 7904 |
. . . . . . . . . . . 12
β’ 1 β
β |
26 | | npcan 8166 |
. . . . . . . . . . . 12
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
27 | 24, 25, 26 | sylancl 413 |
. . . . . . . . . . 11
β’ (π β ((π β 1) + 1) = π) |
28 | 27 | oveq2d 5891 |
. . . . . . . . . 10
β’ (π β (π...((π β 1) + 1)) = (π...π)) |
29 | 28 | adantr 276 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (π...((π β 1) + 1)) = (π...π)) |
30 | 21, 29 | eleqtrd 2256 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β (π...π)) |
31 | 17, 19, 30 | rspcdva 2847 |
. . . . . . 7
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β β) |
32 | 11 | eleq1d 2246 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
33 | | fzssp1 10067 |
. . . . . . . . . 10
β’ (π...(π β 1)) β (π...((π β 1) + 1)) |
34 | 33, 28 | sseqtrid 3206 |
. . . . . . . . 9
β’ (π β (π...(π β 1)) β (π...π)) |
35 | 34 | sselda 3156 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β π β (π...π)) |
36 | 32, 19, 35 | rspcdva 2847 |
. . . . . . 7
β’ ((π β§ π β (π...(π β 1))) β (πΉβπ) β β) |
37 | 31, 36 | lenegd 8481 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β ((πΉβ(π + 1)) β€ (πΉβπ) β -(πΉβπ) β€ -(πΉβ(π + 1)))) |
38 | 15, 37 | mpbid 147 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β -(πΉβπ) β€ -(πΉβ(π + 1))) |
39 | 36 | renegcld 8337 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β -(πΉβπ) β β) |
40 | 11 | negeqd 8152 |
. . . . . . 7
β’ (π = π β -(πΉβπ) = -(πΉβπ)) |
41 | 40, 4 | fvmptg 5593 |
. . . . . 6
β’ ((π β (π...π) β§ -(πΉβπ) β β) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
42 | 35, 39, 41 | syl2anc 411 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
43 | 31 | renegcld 8337 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β -(πΉβ(π + 1)) β β) |
44 | 16 | negeqd 8152 |
. . . . . . 7
β’ (π = (π + 1) β -(πΉβπ) = -(πΉβ(π + 1))) |
45 | 44, 4 | fvmptg 5593 |
. . . . . 6
β’ (((π + 1) β (π...π) β§ -(πΉβ(π + 1)) β β) β ((π β (π...π) β¦ -(πΉβπ))β(π + 1)) = -(πΉβ(π + 1))) |
46 | 30, 43, 45 | syl2anc 411 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -(πΉβπ))β(π + 1)) = -(πΉβ(π + 1))) |
47 | 38, 42, 46 | 3brtr4d 4036 |
. . . 4
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -(πΉβπ))βπ) β€ ((π β (π...π) β¦ -(πΉβπ))β(π + 1))) |
48 | 1, 6, 47 | monoord 10476 |
. . 3
β’ (π β ((π β (π...π) β¦ -(πΉβπ))βπ) β€ ((π β (π...π) β¦ -(πΉβπ))βπ)) |
49 | | eluzfz1 10031 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β (π...π)) |
50 | 1, 49 | syl 14 |
. . . 4
β’ (π β π β (π...π)) |
51 | | fveq2 5516 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
52 | 51 | eleq1d 2246 |
. . . . . 6
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
53 | 52, 18, 50 | rspcdva 2847 |
. . . . 5
β’ (π β (πΉβπ) β β) |
54 | 53 | renegcld 8337 |
. . . 4
β’ (π β -(πΉβπ) β β) |
55 | 51 | negeqd 8152 |
. . . . 5
β’ (π = π β -(πΉβπ) = -(πΉβπ)) |
56 | 55, 4 | fvmptg 5593 |
. . . 4
β’ ((π β (π...π) β§ -(πΉβπ) β β) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
57 | 50, 54, 56 | syl2anc 411 |
. . 3
β’ (π β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
58 | | eluzfz2 10032 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β (π...π)) |
59 | 1, 58 | syl 14 |
. . . 4
β’ (π β π β (π...π)) |
60 | | fveq2 5516 |
. . . . . . 7
β’ (π = π β (πΉβπ) = (πΉβπ)) |
61 | 60 | eleq1d 2246 |
. . . . . 6
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
62 | 61, 18, 59 | rspcdva 2847 |
. . . . 5
β’ (π β (πΉβπ) β β) |
63 | 62 | renegcld 8337 |
. . . 4
β’ (π β -(πΉβπ) β β) |
64 | 60 | negeqd 8152 |
. . . . 5
β’ (π = π β -(πΉβπ) = -(πΉβπ)) |
65 | 64, 4 | fvmptg 5593 |
. . . 4
β’ ((π β (π...π) β§ -(πΉβπ) β β) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
66 | 59, 63, 65 | syl2anc 411 |
. . 3
β’ (π β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
67 | 48, 57, 66 | 3brtr3d 4035 |
. 2
β’ (π β -(πΉβπ) β€ -(πΉβπ)) |
68 | 62, 53 | lenegd 8481 |
. 2
β’ (π β ((πΉβπ) β€ (πΉβπ) β -(πΉβπ) β€ -(πΉβπ))) |
69 | 67, 68 | mpbird 167 |
1
β’ (π β (πΉβπ) β€ (πΉβπ)) |