Step | Hyp | Ref
| Expression |
1 | | monoord2.1 |
. . . 4
β’ (π β π β (β€β₯βπ)) |
2 | | monoord2.2 |
. . . . . . 7
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
3 | 2 | renegcld 11590 |
. . . . . 6
β’ ((π β§ π β (π...π)) β -(πΉβπ) β β) |
4 | 3 | fmpttd 7067 |
. . . . 5
β’ (π β (π β (π...π) β¦ -(πΉβπ)):(π...π)βΆβ) |
5 | 4 | ffvelcdmda 7039 |
. . . 4
β’ ((π β§ π β (π...π)) β ((π β (π...π) β¦ -(πΉβπ))βπ) β β) |
6 | | monoord2.3 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
7 | 6 | ralrimiva 3140 |
. . . . . . . 8
β’ (π β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
8 | | fvoveq1 7384 |
. . . . . . . . . 10
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
9 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
10 | 8, 9 | breq12d 5122 |
. . . . . . . . 9
β’ (π = π β ((πΉβ(π + 1)) β€ (πΉβπ) β (πΉβ(π + 1)) β€ (πΉβπ))) |
11 | 10 | cbvralvw 3224 |
. . . . . . . 8
β’
(βπ β
(π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ) β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
12 | 7, 11 | sylib 217 |
. . . . . . 7
β’ (π β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
13 | 12 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
14 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
15 | 14 | eleq1d 2819 |
. . . . . . . 8
β’ (π = (π + 1) β ((πΉβπ) β β β (πΉβ(π + 1)) β β)) |
16 | 2 | ralrimiva 3140 |
. . . . . . . . 9
β’ (π β βπ β (π...π)(πΉβπ) β β) |
17 | 16 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β βπ β (π...π)(πΉβπ) β β) |
18 | | fzp1elp1 13503 |
. . . . . . . . . 10
β’ (π β (π...(π β 1)) β (π + 1) β (π...((π β 1) + 1))) |
19 | 18 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β (π...((π β 1) + 1))) |
20 | | eluzelz 12781 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β π β β€) |
21 | 1, 20 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
22 | 21 | zcnd 12616 |
. . . . . . . . . . . 12
β’ (π β π β β) |
23 | | ax-1cn 11117 |
. . . . . . . . . . . 12
β’ 1 β
β |
24 | | npcan 11418 |
. . . . . . . . . . . 12
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
25 | 22, 23, 24 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β ((π β 1) + 1) = π) |
26 | 25 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π β (π...((π β 1) + 1)) = (π...π)) |
27 | 26 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (π...((π β 1) + 1)) = (π...π)) |
28 | 19, 27 | eleqtrd 2836 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β (π...π)) |
29 | 15, 17, 28 | rspcdva 3584 |
. . . . . . 7
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β β) |
30 | 9 | eleq1d 2819 |
. . . . . . . 8
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
31 | | fzssp1 13493 |
. . . . . . . . . 10
β’ (π...(π β 1)) β (π...((π β 1) + 1)) |
32 | 31, 26 | sseqtrid 4000 |
. . . . . . . . 9
β’ (π β (π...(π β 1)) β (π...π)) |
33 | 32 | sselda 3948 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β π β (π...π)) |
34 | 30, 17, 33 | rspcdva 3584 |
. . . . . . 7
β’ ((π β§ π β (π...(π β 1))) β (πΉβπ) β β) |
35 | 29, 34 | lenegd 11742 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β ((πΉβ(π + 1)) β€ (πΉβπ) β -(πΉβπ) β€ -(πΉβ(π + 1)))) |
36 | 13, 35 | mpbid 231 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β -(πΉβπ) β€ -(πΉβ(π + 1))) |
37 | 9 | negeqd 11403 |
. . . . . . 7
β’ (π = π β -(πΉβπ) = -(πΉβπ)) |
38 | | eqid 2733 |
. . . . . . 7
β’ (π β (π...π) β¦ -(πΉβπ)) = (π β (π...π) β¦ -(πΉβπ)) |
39 | | negex 11407 |
. . . . . . 7
β’ -(πΉβπ) β V |
40 | 37, 38, 39 | fvmpt 6952 |
. . . . . 6
β’ (π β (π...π) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
41 | 33, 40 | syl 17 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
42 | 14 | negeqd 11403 |
. . . . . . 7
β’ (π = (π + 1) β -(πΉβπ) = -(πΉβ(π + 1))) |
43 | | negex 11407 |
. . . . . . 7
β’ -(πΉβ(π + 1)) β V |
44 | 42, 38, 43 | fvmpt 6952 |
. . . . . 6
β’ ((π + 1) β (π...π) β ((π β (π...π) β¦ -(πΉβπ))β(π + 1)) = -(πΉβ(π + 1))) |
45 | 28, 44 | syl 17 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -(πΉβπ))β(π + 1)) = -(πΉβ(π + 1))) |
46 | 36, 41, 45 | 3brtr4d 5141 |
. . . 4
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -(πΉβπ))βπ) β€ ((π β (π...π) β¦ -(πΉβπ))β(π + 1))) |
47 | 1, 5, 46 | monoord 13947 |
. . 3
β’ (π β ((π β (π...π) β¦ -(πΉβπ))βπ) β€ ((π β (π...π) β¦ -(πΉβπ))βπ)) |
48 | | eluzfz1 13457 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β (π...π)) |
49 | 1, 48 | syl 17 |
. . . 4
β’ (π β π β (π...π)) |
50 | | fveq2 6846 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
51 | 50 | negeqd 11403 |
. . . . 5
β’ (π = π β -(πΉβπ) = -(πΉβπ)) |
52 | | negex 11407 |
. . . . 5
β’ -(πΉβπ) β V |
53 | 51, 38, 52 | fvmpt 6952 |
. . . 4
β’ (π β (π...π) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
54 | 49, 53 | syl 17 |
. . 3
β’ (π β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
55 | | eluzfz2 13458 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β (π...π)) |
56 | 1, 55 | syl 17 |
. . . 4
β’ (π β π β (π...π)) |
57 | | fveq2 6846 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
58 | 57 | negeqd 11403 |
. . . . 5
β’ (π = π β -(πΉβπ) = -(πΉβπ)) |
59 | | negex 11407 |
. . . . 5
β’ -(πΉβπ) β V |
60 | 58, 38, 59 | fvmpt 6952 |
. . . 4
β’ (π β (π...π) β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
61 | 56, 60 | syl 17 |
. . 3
β’ (π β ((π β (π...π) β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
62 | 47, 54, 61 | 3brtr3d 5140 |
. 2
β’ (π β -(πΉβπ) β€ -(πΉβπ)) |
63 | 57 | eleq1d 2819 |
. . . 4
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
64 | 63, 16, 56 | rspcdva 3584 |
. . 3
β’ (π β (πΉβπ) β β) |
65 | 50 | eleq1d 2819 |
. . . 4
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
66 | 65, 16, 49 | rspcdva 3584 |
. . 3
β’ (π β (πΉβπ) β β) |
67 | 64, 66 | lenegd 11742 |
. 2
β’ (π β ((πΉβπ) β€ (πΉβπ) β -(πΉβπ) β€ -(πΉβπ))) |
68 | 62, 67 | mpbird 257 |
1
β’ (π β (πΉβπ) β€ (πΉβπ)) |