Step | Hyp | Ref
| Expression |
1 | | monoord2xrv.n |
. . . 4
β’ (π β π β (β€β₯βπ)) |
2 | | monoord2xrv.x |
. . . . . . 7
β’ ((π β§ π β (π...π)) β (πΉβπ) β
β*) |
3 | 2 | xnegcld 13220 |
. . . . . 6
β’ ((π β§ π β (π...π)) β -π(πΉβπ) β
β*) |
4 | 3 | fmpttd 7064 |
. . . . 5
β’ (π β (π β (π...π) β¦ -π(πΉβπ)):(π...π)βΆβ*) |
5 | 4 | ffvelcdmda 7036 |
. . . 4
β’ ((π β§ π β (π...π)) β ((π β (π...π) β¦ -π(πΉβπ))βπ) β
β*) |
6 | | monoord2xrv.l |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
7 | 6 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
8 | | fvoveq1 7381 |
. . . . . . . . . 10
β’ (π = π β (πΉβ(π + 1)) = (πΉβ(π + 1))) |
9 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πΉβπ) = (πΉβπ)) |
10 | 8, 9 | breq12d 5119 |
. . . . . . . . 9
β’ (π = π β ((πΉβ(π + 1)) β€ (πΉβπ) β (πΉβ(π + 1)) β€ (πΉβπ))) |
11 | 10 | cbvralvw 3226 |
. . . . . . . 8
β’
(βπ β
(π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ) β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
12 | 7, 11 | sylib 217 |
. . . . . . 7
β’ (π β βπ β (π...(π β 1))(πΉβ(π + 1)) β€ (πΉβπ)) |
13 | 12 | r19.21bi 3235 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β€ (πΉβπ)) |
14 | | fzp1elp1 13495 |
. . . . . . . . . 10
β’ (π β (π...(π β 1)) β (π + 1) β (π...((π β 1) + 1))) |
15 | 14 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β (π...((π β 1) + 1))) |
16 | | eluzelz 12774 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯βπ) β π β β€) |
17 | 1, 16 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π β β€) |
18 | 17 | zcnd 12609 |
. . . . . . . . . . . 12
β’ (π β π β β) |
19 | | ax-1cn 11110 |
. . . . . . . . . . . 12
β’ 1 β
β |
20 | | npcan 11411 |
. . . . . . . . . . . 12
β’ ((π β β β§ 1 β
β) β ((π β
1) + 1) = π) |
21 | 18, 19, 20 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β ((π β 1) + 1) = π) |
22 | 21 | oveq2d 7374 |
. . . . . . . . . 10
β’ (π β (π...((π β 1) + 1)) = (π...π)) |
23 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π...(π β 1))) β (π...((π β 1) + 1)) = (π...π)) |
24 | 15, 23 | eleqtrd 2840 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β (π + 1) β (π...π)) |
25 | 2 | ralrimiva 3144 |
. . . . . . . . 9
β’ (π β βπ β (π...π)(πΉβπ) β
β*) |
26 | 25 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β βπ β (π...π)(πΉβπ) β
β*) |
27 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = (π + 1) β (πΉβπ) = (πΉβ(π + 1))) |
28 | 27 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = (π + 1) β ((πΉβπ) β β* β (πΉβ(π + 1)) β
β*)) |
29 | 28 | rspcv 3578 |
. . . . . . . 8
β’ ((π + 1) β (π...π) β (βπ β (π...π)(πΉβπ) β β* β (πΉβ(π + 1)) β
β*)) |
30 | 24, 26, 29 | sylc 65 |
. . . . . . 7
β’ ((π β§ π β (π...(π β 1))) β (πΉβ(π + 1)) β
β*) |
31 | | fzssp1 13485 |
. . . . . . . . . 10
β’ (π...(π β 1)) β (π...((π β 1) + 1)) |
32 | 31, 22 | sseqtrid 3997 |
. . . . . . . . 9
β’ (π β (π...(π β 1)) β (π...π)) |
33 | 32 | sselda 3945 |
. . . . . . . 8
β’ ((π β§ π β (π...(π β 1))) β π β (π...π)) |
34 | 9 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = π β ((πΉβπ) β β* β (πΉβπ) β
β*)) |
35 | 34 | rspcv 3578 |
. . . . . . . 8
β’ (π β (π...π) β (βπ β (π...π)(πΉβπ) β β* β (πΉβπ) β
β*)) |
36 | 33, 26, 35 | sylc 65 |
. . . . . . 7
β’ ((π β§ π β (π...(π β 1))) β (πΉβπ) β
β*) |
37 | | xleneg 13138 |
. . . . . . 7
β’ (((πΉβ(π + 1)) β β* β§
(πΉβπ) β β*) β ((πΉβ(π + 1)) β€ (πΉβπ) β -π(πΉβπ) β€ -π(πΉβ(π + 1)))) |
38 | 30, 36, 37 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (π...(π β 1))) β ((πΉβ(π + 1)) β€ (πΉβπ) β -π(πΉβπ) β€ -π(πΉβ(π + 1)))) |
39 | 13, 38 | mpbid 231 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β
-π(πΉβπ) β€ -π(πΉβ(π + 1))) |
40 | 9 | xnegeqd 43679 |
. . . . . . 7
β’ (π = π β -π(πΉβπ) = -π(πΉβπ)) |
41 | | eqid 2737 |
. . . . . . 7
β’ (π β (π...π) β¦ -π(πΉβπ)) = (π β (π...π) β¦ -π(πΉβπ)) |
42 | | xnegex 13128 |
. . . . . . 7
β’
-π(πΉβπ) β V |
43 | 40, 41, 42 | fvmpt 6949 |
. . . . . 6
β’ (π β (π...π) β ((π β (π...π) β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
44 | 33, 43 | syl 17 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
45 | 27 | xnegeqd 43679 |
. . . . . . 7
β’ (π = (π + 1) β -π(πΉβπ) = -π(πΉβ(π + 1))) |
46 | | xnegex 13128 |
. . . . . . 7
β’
-π(πΉβ(π + 1)) β V |
47 | 45, 41, 46 | fvmpt 6949 |
. . . . . 6
β’ ((π + 1) β (π...π) β ((π β (π...π) β¦ -π(πΉβπ))β(π + 1)) = -π(πΉβ(π + 1))) |
48 | 24, 47 | syl 17 |
. . . . 5
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -π(πΉβπ))β(π + 1)) = -π(πΉβ(π + 1))) |
49 | 39, 44, 48 | 3brtr4d 5138 |
. . . 4
β’ ((π β§ π β (π...(π β 1))) β ((π β (π...π) β¦ -π(πΉβπ))βπ) β€ ((π β (π...π) β¦ -π(πΉβπ))β(π + 1))) |
50 | 1, 5, 49 | monoordxrv 43724 |
. . 3
β’ (π β ((π β (π...π) β¦ -π(πΉβπ))βπ) β€ ((π β (π...π) β¦ -π(πΉβπ))βπ)) |
51 | | eluzfz1 13449 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β (π...π)) |
52 | 1, 51 | syl 17 |
. . . 4
β’ (π β π β (π...π)) |
53 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
54 | 53 | xnegeqd 43679 |
. . . . 5
β’ (π = π β -π(πΉβπ) = -π(πΉβπ)) |
55 | | xnegex 13128 |
. . . . 5
β’
-π(πΉβπ) β V |
56 | 54, 41, 55 | fvmpt 6949 |
. . . 4
β’ (π β (π...π) β ((π β (π...π) β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
57 | 52, 56 | syl 17 |
. . 3
β’ (π β ((π β (π...π) β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
58 | | eluzfz2 13450 |
. . . . 5
β’ (π β
(β€β₯βπ) β π β (π...π)) |
59 | 1, 58 | syl 17 |
. . . 4
β’ (π β π β (π...π)) |
60 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
61 | 60 | xnegeqd 43679 |
. . . . 5
β’ (π = π β -π(πΉβπ) = -π(πΉβπ)) |
62 | | xnegex 13128 |
. . . . 5
β’
-π(πΉβπ) β V |
63 | 61, 41, 62 | fvmpt 6949 |
. . . 4
β’ (π β (π...π) β ((π β (π...π) β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
64 | 59, 63 | syl 17 |
. . 3
β’ (π β ((π β (π...π) β¦ -π(πΉβπ))βπ) = -π(πΉβπ)) |
65 | 50, 57, 64 | 3brtr3d 5137 |
. 2
β’ (π β
-π(πΉβπ) β€ -π(πΉβπ)) |
66 | 60 | eleq1d 2823 |
. . . . 5
β’ (π = π β ((πΉβπ) β β* β (πΉβπ) β
β*)) |
67 | 66 | rspcv 3578 |
. . . 4
β’ (π β (π...π) β (βπ β (π...π)(πΉβπ) β β* β (πΉβπ) β
β*)) |
68 | 59, 25, 67 | sylc 65 |
. . 3
β’ (π β (πΉβπ) β
β*) |
69 | 53 | eleq1d 2823 |
. . . . 5
β’ (π = π β ((πΉβπ) β β* β (πΉβπ) β
β*)) |
70 | 69 | rspcv 3578 |
. . . 4
β’ (π β (π...π) β (βπ β (π...π)(πΉβπ) β β* β (πΉβπ) β
β*)) |
71 | 52, 25, 70 | sylc 65 |
. . 3
β’ (π β (πΉβπ) β
β*) |
72 | | xleneg 13138 |
. . 3
β’ (((πΉβπ) β β* β§ (πΉβπ) β β*) β ((πΉβπ) β€ (πΉβπ) β -π(πΉβπ) β€ -π(πΉβπ))) |
73 | 68, 71, 72 | syl2anc 585 |
. 2
β’ (π β ((πΉβπ) β€ (πΉβπ) β -π(πΉβπ) β€ -π(πΉβπ))) |
74 | 65, 73 | mpbird 257 |
1
β’ (π β (πΉβπ) β€ (πΉβπ)) |