Step | Hyp | Ref
| Expression |
1 | | arch 12417 |
. . . . 5
β’ (π₯ β β β
βπ§ β β
π₯ < π§) |
2 | 1 | ad2antlr 726 |
. . . 4
β’ (((π β§ π₯ β β) β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯) β βπ§ β β π₯ < π§) |
3 | | df-ima 5651 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β πΎ) β (1...π)) = ran ((πΊ β πΎ) βΎ (1...π)) |
4 | | ovolicc2.8 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΊ:πβΆβ) |
5 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β =
(β€β₯β1) |
6 | | ovolicc2.15 |
. . . . . . . . . . . . . . . . . . . . 21
β’ πΎ = seq1((π» β 1st ), (β Γ
{πΆ})) |
7 | | 1zzd 12541 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β 1 β
β€) |
8 | | ovolicc2.14 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β πΆ β π) |
9 | | ovolicc2.11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π»:πβΆπ) |
10 | 5, 6, 7, 8, 9 | algrf 16456 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β πΎ:ββΆπ) |
11 | | ovolicc2.10 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = {π’ β π β£ (π’ β© (π΄[,]π΅)) β β
} |
12 | 11 | ssrab3 4045 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β π |
13 | | fss 6690 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΎ:ββΆπ β§ π β π) β πΎ:ββΆπ) |
14 | 10, 12, 13 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΎ:ββΆπ) |
15 | | fco 6697 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊ:πβΆβ β§ πΎ:ββΆπ) β (πΊ β πΎ):ββΆβ) |
16 | 4, 14, 15 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΊ β πΎ):ββΆβ) |
17 | | fz1ssnn 13479 |
. . . . . . . . . . . . . . . . . 18
β’
(1...π) β
β |
18 | | fssres 6713 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΊ β πΎ):ββΆβ β§ (1...π) β β) β
((πΊ β πΎ) βΎ (1...π)):(1...π)βΆβ) |
19 | 16, 17, 18 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((πΊ β πΎ) βΎ (1...π)):(1...π)βΆβ) |
20 | 19 | frnd 6681 |
. . . . . . . . . . . . . . . 16
β’ (π β ran ((πΊ β πΎ) βΎ (1...π)) β β) |
21 | 3, 20 | eqsstrid 3997 |
. . . . . . . . . . . . . . 15
β’ (π β ((πΊ β πΎ) β (1...π)) β β) |
22 | | nnssre 12164 |
. . . . . . . . . . . . . . 15
β’ β
β β |
23 | 21, 22 | sstrdi 3961 |
. . . . . . . . . . . . . 14
β’ (π β ((πΊ β πΎ) β (1...π)) β β) |
24 | 23 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β ((πΊ β πΎ) β (1...π)) β β) |
25 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π¦ β ((πΊ β πΎ) β (1...π))) |
26 | 24, 25 | sseldd 3950 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π¦ β β) |
27 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π₯ β β) |
28 | | nnre 12167 |
. . . . . . . . . . . . 13
β’ (π§ β β β π§ β
β) |
29 | 28 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π§ β β) |
30 | | lelttr 11252 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π₯ β β β§ π§ β β) β ((π¦ β€ π₯ β§ π₯ < π§) β π¦ < π§)) |
31 | 26, 27, 29, 30 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β ((π¦ β€ π₯ β§ π₯ < π§) β π¦ < π§)) |
32 | 31 | ancomsd 467 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β ((π₯ < π§ β§ π¦ β€ π₯) β π¦ < π§)) |
33 | 32 | expdimp 454 |
. . . . . . . . 9
β’
(((((π β§ π₯ β β) β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β§ π₯ < π§) β (π¦ β€ π₯ β π¦ < π§)) |
34 | 33 | an32s 651 |
. . . . . . . 8
β’
(((((π β§ π₯ β β) β§ π§ β β) β§ π₯ < π§) β§ π¦ β ((πΊ β πΎ) β (1...π))) β (π¦ β€ π₯ β π¦ < π§)) |
35 | 34 | ralimdva 3165 |
. . . . . . 7
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ π₯ < π§) β (βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯ β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) |
36 | 35 | impancom 453 |
. . . . . 6
β’ ((((π β§ π₯ β β) β§ π§ β β) β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯) β (π₯ < π§ β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) |
37 | 36 | an32s 651 |
. . . . 5
β’ ((((π β§ π₯ β β) β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯) β§ π§ β β) β (π₯ < π§ β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) |
38 | 37 | reximdva 3166 |
. . . 4
β’ (((π β§ π₯ β β) β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯) β (βπ§ β β π₯ < π§ β βπ§ β β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) |
39 | 2, 38 | mpd 15 |
. . 3
β’ (((π β§ π₯ β β) β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯) β βπ§ β β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§) |
40 | | fzfid 13885 |
. . . . 5
β’ (π β (1...π) β Fin) |
41 | | fvres 6866 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β (((πΊ β πΎ) βΎ (1...π))βπ) = ((πΊ β πΎ)βπ)) |
42 | 41 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (((πΊ β πΎ) βΎ (1...π))βπ) = ((πΊ β πΎ)βπ)) |
43 | | elfznn 13477 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β π β β) |
44 | | fvco3 6945 |
. . . . . . . . . . . . . . 15
β’ ((πΎ:ββΆπ β§ π β β) β ((πΊ β πΎ)βπ) = (πΊβ(πΎβπ))) |
45 | 10, 43, 44 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β ((πΊ β πΎ)βπ) = (πΊβ(πΎβπ))) |
46 | 42, 45 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (((πΊ β πΎ) βΎ (1...π))βπ) = (πΊβ(πΎβπ))) |
47 | 46 | adantrr 716 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β (((πΊ β πΎ) βΎ (1...π))βπ) = (πΊβ(πΎβπ))) |
48 | | fvres 6866 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (((πΊ β πΎ) βΎ (1...π))βπ) = ((πΊ β πΎ)βπ)) |
49 | 48 | ad2antll 728 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β (((πΊ β πΎ) βΎ (1...π))βπ) = ((πΊ β πΎ)βπ)) |
50 | | elfznn 13477 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β π β β) |
51 | 50 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β (1...π) β§ π β (1...π)) β π β β) |
52 | | fvco3 6945 |
. . . . . . . . . . . . . 14
β’ ((πΎ:ββΆπ β§ π β β) β ((πΊ β πΎ)βπ) = (πΊβ(πΎβπ))) |
53 | 10, 51, 52 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β ((πΊ β πΎ)βπ) = (πΊβ(πΎβπ))) |
54 | 49, 53 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β (((πΊ β πΎ) βΎ (1...π))βπ) = (πΊβ(πΎβπ))) |
55 | 47, 54 | eqeq12d 2753 |
. . . . . . . . . . 11
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β ((((πΊ β πΎ) βΎ (1...π))βπ) = (((πΊ β πΎ) βΎ (1...π))βπ) β (πΊβ(πΎβπ)) = (πΊβ(πΎβπ)))) |
56 | | 2fveq3 6852 |
. . . . . . . . . . . 12
β’ ((πΊβ(πΎβπ)) = (πΊβ(πΎβπ)) β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ))))) |
57 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...π) β β) |
58 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (1...π) β π β β) |
59 | 58 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (1...π)) β§ π β π) β π β β) |
60 | 59 | nnred 12175 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ π β π) β π β β) |
61 | | ovolicc2.16 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π = {π β β β£ π΅ β (πΎβπ)} |
62 | 61 | ssrab3 4045 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π β
β |
63 | 62, 22 | sstri 3958 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π β
β |
64 | | ovolicc2.17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ π = inf(π, β, < ) |
65 | 62, 5 | sseqtri 3985 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ π β
(β€β₯β1) |
66 | | nnnfi 13878 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ Β¬
β β Fin |
67 | | ovolicc2.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β π β (π« ran ((,) β πΉ) β© Fin)) |
68 | 67 | elin2d 4164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β π β Fin) |
69 | | ssfi 9124 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β Fin β§ π β π) β π β Fin) |
70 | 68, 12, 69 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β Fin) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π = β
) β π β Fin) |
72 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π = β
) β πΎ:ββΆπ) |
73 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((πΎβπ) = (πΎβπ) β (πΉβ(πΊβ(πΎβπ))) = (πΉβ(πΊβ(πΎβπ)))) |
74 | 73 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΎβπ) = (πΎβπ) β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ))))) |
75 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β π) |
76 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β π β β) |
77 | | ral0 4475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
βπ β
β
π β€ π |
78 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β π = β
) |
79 | 78 | raleqdv 3316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β (βπ β π π β€ π β βπ β β
π β€ π)) |
80 | 77, 79 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β βπ β π π β€ π) |
81 | 80 | ralrimivw 3148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β βπ β β βπ β π π β€ π) |
82 | | rabid2 3439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (β
= {π β β β£
βπ β π π β€ π} β βπ β β βπ β π π β€ π) |
83 | 81, 82 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β β = {π β β β£
βπ β π π β€ π}) |
84 | 76, 83 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β π β {π β β β£ βπ β π π β€ π}) |
85 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β π β β) |
86 | 85, 83 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β π β {π β β β£ βπ β π π β€ π}) |
87 | | ovolicc.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β π΄ β β) |
88 | | ovolicc.2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β π΅ β β) |
89 | | ovolicc.3 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β π΄ β€ π΅) |
90 | | ovolicc2.4 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
91 | | ovolicc2.5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
92 | | ovolicc2.7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β (π΄[,]π΅) β βͺ π) |
93 | | ovolicc2.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π‘ β π) β (((,) β πΉ)β(πΊβπ‘)) = π‘) |
94 | | ovolicc2.12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β§ π‘ β π) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) |
95 | | ovolicc2.13 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β π΄ β πΆ) |
96 | 87, 88, 89, 90, 91, 67, 92, 4, 93, 11, 9, 94, 95, 8, 6, 61 | ovolicc2lem3 24899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β§ (π β {π β β β£ βπ β π π β€ π} β§ π β {π β β β£ βπ β π π β€ π})) β (π = π β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ)))))) |
97 | 75, 84, 86, 96 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β (π = π β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ)))))) |
98 | 74, 97 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π = β
) β§ (π β β β§ π β β)) β ((πΎβπ) = (πΎβπ) β π = π)) |
99 | 98 | ralrimivva 3198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ π = β
) β βπ β β βπ β β ((πΎβπ) = (πΎβπ) β π = π)) |
100 | | dff13 7207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (πΎ:ββ1-1βπ β (πΎ:ββΆπ β§ βπ β β βπ β β ((πΎβπ) = (πΎβπ) β π = π))) |
101 | 72, 99, 100 | sylanbrc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ π = β
) β πΎ:ββ1-1βπ) |
102 | | f1domg 8919 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β Fin β (πΎ:ββ1-1βπ β β βΌ π)) |
103 | 71, 101, 102 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β§ π = β
) β β βΌ π) |
104 | | domfi 9143 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β Fin β§ β
βΌ π) β β
β Fin) |
105 | 70, 103, 104 | syl2an2r 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π = β
) β β β
Fin) |
106 | 105 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (π = β
β β β
Fin)) |
107 | 106 | necon3bd 2958 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (Β¬ β β Fin
β π β
β
)) |
108 | 66, 107 | mpi 20 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β π β β
) |
109 | | infssuzcl 12864 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β
(β€β₯β1) β§ π β β
) β inf(π, β, < ) β π) |
110 | 65, 108, 109 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β inf(π, β, < ) β π) |
111 | 64, 110 | eqeltrid 2842 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β π) |
112 | 63, 111 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β) |
113 | 112 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ π β π) β π β β) |
114 | 63 | sseli 3945 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β π β β) |
115 | 114 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ π β π) β π β β) |
116 | | elfzle2 13452 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β π β€ π) |
117 | 116 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ π β π) β π β€ π) |
118 | | infssuzle 12863 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β
(β€β₯β1) β§ π β π) β inf(π, β, < ) β€ π) |
119 | 65, 118 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β inf(π, β, < ) β€ π) |
120 | 64, 119 | eqbrtrid 5145 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β π β€ π) |
121 | 120 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β (1...π)) β§ π β π) β π β€ π) |
122 | 60, 113, 115, 117, 121 | letrd 11319 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β (1...π)) β§ π β π) β π β€ π) |
123 | 122 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β βπ β π π β€ π) |
124 | 57, 123 | ssrabdv 4036 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...π) β {π β β β£ βπ β π π β€ π}) |
125 | 124 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β (1...π) β {π β β β£ βπ β π π β€ π}) |
126 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β π β (1...π)) |
127 | 125, 126 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β π β {π β β β£ βπ β π π β€ π}) |
128 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β π β (1...π)) |
129 | 125, 128 | sseldd 3950 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β π β {π β β β£ βπ β π π β€ π}) |
130 | 127, 129 | jca 513 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β (π β {π β β β£ βπ β π π β€ π} β§ π β {π β β β£ βπ β π π β€ π})) |
131 | 130, 96 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β (π = π β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ)))))) |
132 | 56, 131 | syl5ibr 246 |
. . . . . . . . . . 11
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β ((πΊβ(πΎβπ)) = (πΊβ(πΎβπ)) β π = π)) |
133 | 55, 132 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β§ (π β (1...π) β§ π β (1...π))) β ((((πΊ β πΎ) βΎ (1...π))βπ) = (((πΊ β πΎ) βΎ (1...π))βπ) β π = π)) |
134 | 133 | ralrimivva 3198 |
. . . . . . . . 9
β’ (π β βπ β (1...π)βπ β (1...π)((((πΊ β πΎ) βΎ (1...π))βπ) = (((πΊ β πΎ) βΎ (1...π))βπ) β π = π)) |
135 | | dff13 7207 |
. . . . . . . . 9
β’ (((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1ββ β (((πΊ β πΎ) βΎ (1...π)):(1...π)βΆβ β§ βπ β (1...π)βπ β (1...π)((((πΊ β πΎ) βΎ (1...π))βπ) = (((πΊ β πΎ) βΎ (1...π))βπ) β π = π))) |
136 | 19, 134, 135 | sylanbrc 584 |
. . . . . . . 8
β’ (π β ((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1ββ) |
137 | | f1f1orn 6800 |
. . . . . . . 8
β’ (((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1ββ β ((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβran
((πΊ β πΎ) βΎ (1...π))) |
138 | 136, 137 | syl 17 |
. . . . . . 7
β’ (π β ((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβran
((πΊ β πΎ) βΎ (1...π))) |
139 | | f1oeq3 6779 |
. . . . . . . 8
β’ (((πΊ β πΎ) β (1...π)) = ran ((πΊ β πΎ) βΎ (1...π)) β (((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβ((πΊ β πΎ) β (1...π)) β ((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβran
((πΊ β πΎ) βΎ (1...π)))) |
140 | 3, 139 | ax-mp 5 |
. . . . . . 7
β’ (((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβ((πΊ β πΎ) β (1...π)) β ((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβran
((πΊ β πΎ) βΎ (1...π))) |
141 | 138, 140 | sylibr 233 |
. . . . . 6
β’ (π β ((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβ((πΊ β πΎ) β (1...π))) |
142 | | f1ofo 6796 |
. . . . . 6
β’ (((πΊ β πΎ) βΎ (1...π)):(1...π)β1-1-ontoβ((πΊ β πΎ) β (1...π)) β ((πΊ β πΎ) βΎ (1...π)):(1...π)βontoβ((πΊ β πΎ) β (1...π))) |
143 | 141, 142 | syl 17 |
. . . . 5
β’ (π β ((πΊ β πΎ) βΎ (1...π)):(1...π)βontoβ((πΊ β πΎ) β (1...π))) |
144 | | fofi 9289 |
. . . . 5
β’
(((1...π) β Fin
β§ ((πΊ β πΎ) βΎ (1...π)):(1...π)βontoβ((πΊ β πΎ) β (1...π))) β ((πΊ β πΎ) β (1...π)) β Fin) |
145 | 40, 143, 144 | syl2anc 585 |
. . . 4
β’ (π β ((πΊ β πΎ) β (1...π)) β Fin) |
146 | | fimaxre2 12107 |
. . . 4
β’ ((((πΊ β πΎ) β (1...π)) β β β§ ((πΊ β πΎ) β (1...π)) β Fin) β βπ₯ β β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯) |
147 | 23, 145, 146 | syl2anc 585 |
. . 3
β’ (π β βπ₯ β β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β€ π₯) |
148 | 39, 147 | r19.29a 3160 |
. 2
β’ (π β βπ§ β β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§) |
149 | 88, 87 | resubcld 11590 |
. . . . 5
β’ (π β (π΅ β π΄) β β) |
150 | 149 | rexrd 11212 |
. . . 4
β’ (π β (π΅ β π΄) β
β*) |
151 | 150 | adantr 482 |
. . 3
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (π΅ β π΄) β
β*) |
152 | | fzfid 13885 |
. . . . . 6
β’ (π β (1...π§) β Fin) |
153 | | elfznn 13477 |
. . . . . . . . 9
β’ (π β (1...π§) β π β β) |
154 | | eqid 2737 |
. . . . . . . . . . . 12
β’ ((abs
β β ) β πΉ) = ((abs β β ) β πΉ) |
155 | 154 | ovolfsf 24851 |
. . . . . . . . . . 11
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β ((abs β β ) β πΉ):ββΆ(0[,)+β)) |
156 | 91, 155 | syl 17 |
. . . . . . . . . 10
β’ (π β ((abs β β )
β πΉ):ββΆ(0[,)+β)) |
157 | 156 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)βπ) β (0[,)+β)) |
158 | 153, 157 | sylan2 594 |
. . . . . . . 8
β’ ((π β§ π β (1...π§)) β (((abs β β ) β
πΉ)βπ) β (0[,)+β)) |
159 | | elrege0 13378 |
. . . . . . . 8
β’ ((((abs
β β ) β πΉ)βπ) β (0[,)+β) β ((((abs
β β ) β πΉ)βπ) β β β§ 0 β€ (((abs β
β ) β πΉ)βπ))) |
160 | 158, 159 | sylib 217 |
. . . . . . 7
β’ ((π β§ π β (1...π§)) β ((((abs β β ) β
πΉ)βπ) β β β§ 0 β€ (((abs β
β ) β πΉ)βπ))) |
161 | 160 | simpld 496 |
. . . . . 6
β’ ((π β§ π β (1...π§)) β (((abs β β ) β
πΉ)βπ) β β) |
162 | 152, 161 | fsumrecl 15626 |
. . . . 5
β’ (π β Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ) β β) |
163 | 162 | adantr 482 |
. . . 4
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ) β β) |
164 | 163 | rexrd 11212 |
. . 3
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ) β
β*) |
165 | 154, 90 | ovolsf 24852 |
. . . . . . . . 9
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
166 | 91, 165 | syl 17 |
. . . . . . . 8
β’ (π β π:ββΆ(0[,)+β)) |
167 | 166 | frnd 6681 |
. . . . . . 7
β’ (π β ran π β (0[,)+β)) |
168 | | rge0ssre 13380 |
. . . . . . 7
β’
(0[,)+β) β β |
169 | 167, 168 | sstrdi 3961 |
. . . . . 6
β’ (π β ran π β β) |
170 | | ressxr 11206 |
. . . . . 6
β’ β
β β* |
171 | 169, 170 | sstrdi 3961 |
. . . . 5
β’ (π β ran π β
β*) |
172 | | supxrcl 13241 |
. . . . 5
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
173 | 171, 172 | syl 17 |
. . . 4
β’ (π β sup(ran π, β*, < ) β
β*) |
174 | 173 | adantr 482 |
. . 3
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β sup(ran π, β*, < ) β
β*) |
175 | 149 | adantr 482 |
. . . 4
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (π΅ β π΄) β β) |
176 | 21 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π β ((πΊ β πΎ) β (1...π))) β π β β) |
177 | 168, 157 | sselid 3947 |
. . . . . . 7
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)βπ) β β) |
178 | 176, 177 | syldan 592 |
. . . . . 6
β’ ((π β§ π β ((πΊ β πΎ) β (1...π))) β (((abs β β ) β
πΉ)βπ) β β) |
179 | 145, 178 | fsumrecl 15626 |
. . . . 5
β’ (π β Ξ£π β ((πΊ β πΎ) β (1...π))(((abs β β ) β πΉ)βπ) β β) |
180 | 179 | adantr 482 |
. . . 4
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β Ξ£π β ((πΊ β πΎ) β (1...π))(((abs β β ) β πΉ)βπ) β β) |
181 | | inss2 4194 |
. . . . . . . . . . 11
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
182 | | fss 6690 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β Γ β)) β πΉ:ββΆ(β Γ
β)) |
183 | 91, 181, 182 | sylancl 587 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆ(β Γ
β)) |
184 | 62, 111 | sselid 3947 |
. . . . . . . . . . . 12
β’ (π β π β β) |
185 | 14, 184 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ (π β (πΎβπ) β π) |
186 | 4, 185 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ (π β (πΊβ(πΎβπ)) β β) |
187 | 183, 186 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ (π β (πΉβ(πΊβ(πΎβπ))) β (β Γ
β)) |
188 | | xp2nd 7959 |
. . . . . . . . 9
β’ ((πΉβ(πΊβ(πΎβπ))) β (β Γ β) β
(2nd β(πΉβ(πΊβ(πΎβπ)))) β β) |
189 | 187, 188 | syl 17 |
. . . . . . . 8
β’ (π β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β β) |
190 | 12, 8 | sselid 3947 |
. . . . . . . . . . 11
β’ (π β πΆ β π) |
191 | 4, 190 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ (π β (πΊβπΆ) β β) |
192 | 183, 191 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ (π β (πΉβ(πΊβπΆ)) β (β Γ
β)) |
193 | | xp1st 7958 |
. . . . . . . . 9
β’ ((πΉβ(πΊβπΆ)) β (β Γ β) β
(1st β(πΉβ(πΊβπΆ))) β β) |
194 | 192, 193 | syl 17 |
. . . . . . . 8
β’ (π β (1st
β(πΉβ(πΊβπΆ))) β β) |
195 | 189, 194 | resubcld 11590 |
. . . . . . 7
β’ (π β ((2nd
β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) β β) |
196 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π = (πΊβ(πΎβπ)) β (((abs β β ) β
πΉ)βπ) = (((abs β β ) β πΉ)β(πΊβ(πΎβπ)))) |
197 | 177 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((abs β
β ) β πΉ)βπ) β β) |
198 | 176, 197 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β ((πΊ β πΎ) β (1...π))) β (((abs β β ) β
πΉ)βπ) β β) |
199 | 196, 40, 141, 46, 198 | fsumf1o 15615 |
. . . . . . . . 9
β’ (π β Ξ£π β ((πΊ β πΎ) β (1...π))(((abs β β ) β πΉ)βπ) = Ξ£π β (1...π)(((abs β β ) β πΉ)β(πΊβ(πΎβπ)))) |
200 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β πΊ:πβΆβ) |
201 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((πΎ:ββΆπ β§ π β β) β (πΎβπ) β π) |
202 | 14, 43, 201 | syl2an 597 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (πΎβπ) β π) |
203 | 200, 202 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πΊβ(πΎβπ)) β β) |
204 | 154 | ovolfsval 24850 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ (πΊβ(πΎβπ)) β β) β (((abs β
β ) β πΉ)β(πΊβ(πΎβπ))) = ((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβ(πΎβπ)))))) |
205 | 91, 203, 204 | syl2an2r 684 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (((abs β β ) β
πΉ)β(πΊβ(πΎβπ))) = ((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβ(πΎβπ)))))) |
206 | 205 | sumeq2dv 15595 |
. . . . . . . . 9
β’ (π β Ξ£π β (1...π)(((abs β β ) β πΉ)β(πΊβ(πΎβπ))) = Ξ£π β (1...π)((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβ(πΎβπ)))))) |
207 | 183 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β πΉ:ββΆ(β Γ
β)) |
208 | 4 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β πΊ:πβΆβ) |
209 | 14 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΎβπ) β π) |
210 | 208, 209 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΊβ(πΎβπ)) β β) |
211 | 207, 210 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πΉβ(πΊβ(πΎβπ))) β (β Γ
β)) |
212 | | xp2nd 7959 |
. . . . . . . . . . . . . 14
β’ ((πΉβ(πΊβ(πΎβπ))) β (β Γ β) β
(2nd β(πΉβ(πΊβ(πΎβπ)))) β β) |
213 | 211, 212 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β β) |
214 | 43, 213 | sylan2 594 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (2nd β(πΉβ(πΊβ(πΎβπ)))) β β) |
215 | 214 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (2nd β(πΉβ(πΊβ(πΎβπ)))) β β) |
216 | 183 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β πΉ:ββΆ(β Γ
β)) |
217 | 216, 203 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πΉβ(πΊβ(πΎβπ))) β (β Γ
β)) |
218 | | xp1st 7958 |
. . . . . . . . . . . . 13
β’ ((πΉβ(πΊβ(πΎβπ))) β (β Γ β) β
(1st β(πΉβ(πΊβ(πΎβπ)))) β β) |
219 | 217, 218 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (1st β(πΉβ(πΊβ(πΎβπ)))) β β) |
220 | 219 | recnd 11190 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (1st β(πΉβ(πΊβ(πΎβπ)))) β β) |
221 | 40, 215, 220 | fsumsub 15680 |
. . . . . . . . . 10
β’ (π β Ξ£π β (1...π)((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβ(πΎβπ))))) = (Ξ£π β (1...π)(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...π)(1st β(πΉβ(πΊβ(πΎβπ)))))) |
222 | | fzfid 13885 |
. . . . . . . . . . . . . 14
β’ (π β (1...(π β 1)) β Fin) |
223 | | elfznn 13477 |
. . . . . . . . . . . . . . 15
β’ (π β (1...(π β 1)) β π β β) |
224 | 223, 213 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(π β 1))) β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β β) |
225 | 222, 224 | fsumrecl 15626 |
. . . . . . . . . . . . 13
β’ (π β Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β β) |
226 | 225 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π β Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β β) |
227 | 189 | recnd 11190 |
. . . . . . . . . . . 12
β’ (π β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β β) |
228 | 65, 111 | sselid 3947 |
. . . . . . . . . . . . 13
β’ (π β π β
(β€β₯β1)) |
229 | | 2fveq3 6852 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΊβ(πΎβπ)) = (πΊβ(πΎβπ))) |
230 | 229 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = π β (πΉβ(πΊβ(πΎβπ))) = (πΉβ(πΊβ(πΎβπ)))) |
231 | 230 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π = π β (2nd β(πΉβ(πΊβ(πΎβπ)))) = (2nd β(πΉβ(πΊβ(πΎβπ))))) |
232 | 228, 215,
231 | fsumm1 15643 |
. . . . . . . . . . . 12
β’ (π β Ξ£π β (1...π)(2nd β(πΉβ(πΊβ(πΎβπ)))) = (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) + (2nd β(πΉβ(πΊβ(πΎβπ)))))) |
233 | 226, 227,
232 | comraddd 11376 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...π)(2nd β(πΉβ(πΊβ(πΎβπ)))) = ((2nd β(πΉβ(πΊβ(πΎβπ)))) + Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))))) |
234 | | 2fveq3 6852 |
. . . . . . . . . . . . . . 15
β’ (π = 1 β (πΊβ(πΎβπ)) = (πΊβ(πΎβ1))) |
235 | 234 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = 1 β (πΉβ(πΊβ(πΎβπ))) = (πΉβ(πΊβ(πΎβ1)))) |
236 | 235 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π = 1 β (1st
β(πΉβ(πΊβ(πΎβπ)))) = (1st β(πΉβ(πΊβ(πΎβ1))))) |
237 | 228, 220,
236 | fsum1p 15645 |
. . . . . . . . . . . 12
β’ (π β Ξ£π β (1...π)(1st β(πΉβ(πΊβ(πΎβπ)))) = ((1st β(πΉβ(πΊβ(πΎβ1)))) + Ξ£π β ((1 + 1)...π)(1st β(πΉβ(πΊβ(πΎβπ)))))) |
238 | 5, 6, 7, 8 | algr0 16455 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΎβ1) = πΆ) |
239 | 238 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π β (πΊβ(πΎβ1)) = (πΊβπΆ)) |
240 | 239 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π β (πΉβ(πΊβ(πΎβ1))) = (πΉβ(πΊβπΆ))) |
241 | 240 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π β (1st
β(πΉβ(πΊβ(πΎβ1)))) = (1st β(πΉβ(πΊβπΆ)))) |
242 | 7 | peano2zd 12617 |
. . . . . . . . . . . . . . 15
β’ (π β (1 + 1) β
β€) |
243 | 184 | nnzd 12533 |
. . . . . . . . . . . . . . 15
β’ (π β π β β€) |
244 | | 1z 12540 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β€ |
245 | | fzp1ss 13499 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
β€ β ((1 + 1)...π) β (1...π)) |
246 | 244, 245 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((1 + 1)...π) β (1...π)) |
247 | 246 | sselda 3949 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β ((1 + 1)...π)) β π β (1...π)) |
248 | 247, 220 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β ((1 + 1)...π)) β (1st β(πΉβ(πΊβ(πΎβπ)))) β β) |
249 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . 17
β’ (π = (π + 1) β (πΊβ(πΎβπ)) = (πΊβ(πΎβ(π + 1)))) |
250 | 249 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = (π + 1) β (πΉβ(πΊβ(πΎβπ))) = (πΉβ(πΊβ(πΎβ(π + 1))))) |
251 | 250 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (1st β(πΉβ(πΊβ(πΎβπ)))) = (1st β(πΉβ(πΊβ(πΎβ(π + 1)))))) |
252 | 7, 242, 243, 248, 251 | fsumshftm 15673 |
. . . . . . . . . . . . . 14
β’ (π β Ξ£π β ((1 + 1)...π)(1st β(πΉβ(πΊβ(πΎβπ)))) = Ξ£π β (((1 + 1) β 1)...(π β 1))(1st
β(πΉβ(πΊβ(πΎβ(π + 1)))))) |
253 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β |
254 | 253, 253 | pncan3oi 11424 |
. . . . . . . . . . . . . . . . 17
β’ ((1 + 1)
β 1) = 1 |
255 | 254 | oveq1i 7372 |
. . . . . . . . . . . . . . . 16
β’ (((1 + 1)
β 1)...(π β 1))
= (1...(π β
1)) |
256 | 255 | sumeq1i 15590 |
. . . . . . . . . . . . . . 15
β’
Ξ£π β (((1
+ 1) β 1)...(π
β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) = Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) |
257 | | fvoveq1 7385 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΎβ(π + 1)) = (πΎβ(π + 1))) |
258 | 257 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (πΊβ(πΎβ(π + 1))) = (πΊβ(πΎβ(π + 1)))) |
259 | 258 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πΉβ(πΊβ(πΎβ(π + 1)))) = (πΉβ(πΊβ(πΎβ(π + 1))))) |
260 | 259 | fveq2d 6851 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (1st β(πΉβ(πΊβ(πΎβ(π + 1))))) = (1st β(πΉβ(πΊβ(πΎβ(π + 1)))))) |
261 | 260 | cbvsumv 15588 |
. . . . . . . . . . . . . . 15
β’
Ξ£π β
(1...(π β
1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) = Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) |
262 | 256, 261 | eqtri 2765 |
. . . . . . . . . . . . . 14
β’
Ξ£π β (((1
+ 1) β 1)...(π
β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) = Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) |
263 | 252, 262 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π β Ξ£π β ((1 + 1)...π)(1st β(πΉβ(πΊβ(πΎβπ)))) = Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))) |
264 | 241, 263 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ (π β ((1st
β(πΉβ(πΊβ(πΎβ1)))) + Ξ£π β ((1 + 1)...π)(1st β(πΉβ(πΊβ(πΎβπ))))) = ((1st β(πΉβ(πΊβπΆ))) + Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))))) |
265 | 237, 264 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...π)(1st β(πΉβ(πΊβ(πΎβπ)))) = ((1st β(πΉβ(πΊβπΆ))) + Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))))) |
266 | 233, 265 | oveq12d 7380 |
. . . . . . . . . 10
β’ (π β (Ξ£π β (1...π)(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...π)(1st β(πΉβ(πΊβ(πΎβπ))))) = (((2nd β(πΉβ(πΊβ(πΎβπ)))) + Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ))))) β ((1st β(πΉβ(πΊβπΆ))) + Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
267 | 194 | recnd 11190 |
. . . . . . . . . . 11
β’ (π β (1st
β(πΉβ(πΊβπΆ))) β β) |
268 | | peano2nn 12172 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β (π + 1) β
β) |
269 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ:ββΆπ β§ (π + 1) β β) β (πΎβ(π + 1)) β π) |
270 | 14, 268, 269 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (πΎβ(π + 1)) β π) |
271 | 208, 270 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΊβ(πΎβ(π + 1))) β β) |
272 | 207, 271 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΉβ(πΊβ(πΎβ(π + 1)))) β (β Γ
β)) |
273 | | xp1st 7958 |
. . . . . . . . . . . . . . 15
β’ ((πΉβ(πΊβ(πΎβ(π + 1)))) β (β Γ β)
β (1st β(πΉβ(πΊβ(πΎβ(π + 1))))) β β) |
274 | 272, 273 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (1st
β(πΉβ(πΊβ(πΎβ(π + 1))))) β β) |
275 | 223, 274 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...(π β 1))) β (1st
β(πΉβ(πΊβ(πΎβ(π + 1))))) β β) |
276 | 222, 275 | fsumrecl 15626 |
. . . . . . . . . . . 12
β’ (π β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) β β) |
277 | 276 | recnd 11190 |
. . . . . . . . . . 11
β’ (π β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) β β) |
278 | 227, 226,
267, 277 | addsub4d 11566 |
. . . . . . . . . 10
β’ (π β (((2nd
β(πΉβ(πΊβ(πΎβπ)))) + Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ))))) β ((1st β(πΉβ(πΊβπΆ))) + Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))))) = (((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) + (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
279 | 221, 266,
278 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (π β Ξ£π β (1...π)((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβ(πΎβπ))))) = (((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) + (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
280 | 199, 206,
279 | 3eqtrd 2781 |
. . . . . . . 8
β’ (π β Ξ£π β ((πΊ β πΎ) β (1...π))(((abs β β ) β πΉ)βπ) = (((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) + (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
281 | 280, 179 | eqeltrrd 2839 |
. . . . . . 7
β’ (π β (((2nd
β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) + (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))))) β β) |
282 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΎβπ) = (πΎβπ)) |
283 | 282 | eleq2d 2824 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΅ β (πΎβπ) β π΅ β (πΎβπ))) |
284 | 283, 61 | elrab2 3653 |
. . . . . . . . . . . . 13
β’ (π β π β (π β β β§ π΅ β (πΎβπ))) |
285 | 111, 284 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β (π β β β§ π΅ β (πΎβπ))) |
286 | 285 | simprd 497 |
. . . . . . . . . . 11
β’ (π β π΅ β (πΎβπ)) |
287 | 87, 88, 89, 90, 91, 67, 92, 4, 93 | ovolicc2lem1 24897 |
. . . . . . . . . . . 12
β’ ((π β§ (πΎβπ) β π) β (π΅ β (πΎβπ) β (π΅ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π΅ β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ))))))) |
288 | 185, 287 | mpdan 686 |
. . . . . . . . . . 11
β’ (π β (π΅ β (πΎβπ) β (π΅ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π΅ β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ))))))) |
289 | 286, 288 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π΅ β β β§ (1st
β(πΉβ(πΊβ(πΎβπ)))) < π΅ β§ π΅ < (2nd β(πΉβ(πΊβ(πΎβπ)))))) |
290 | 289 | simp3d 1145 |
. . . . . . . . 9
β’ (π β π΅ < (2nd β(πΉβ(πΊβ(πΎβπ))))) |
291 | 87, 88, 89, 90, 91, 67, 92, 4, 93 | ovolicc2lem1 24897 |
. . . . . . . . . . . 12
β’ ((π β§ πΆ β π) β (π΄ β πΆ β (π΄ β β β§ (1st
β(πΉβ(πΊβπΆ))) < π΄ β§ π΄ < (2nd β(πΉβ(πΊβπΆ)))))) |
292 | 190, 291 | mpdan 686 |
. . . . . . . . . . 11
β’ (π β (π΄ β πΆ β (π΄ β β β§ (1st
β(πΉβ(πΊβπΆ))) < π΄ β§ π΄ < (2nd β(πΉβ(πΊβπΆ)))))) |
293 | 95, 292 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π΄ β β β§ (1st
β(πΉβ(πΊβπΆ))) < π΄ β§ π΄ < (2nd β(πΉβ(πΊβπΆ))))) |
294 | 293 | simp2d 1144 |
. . . . . . . . 9
β’ (π β (1st
β(πΉβ(πΊβπΆ))) < π΄) |
295 | 88, 194, 189, 87, 290, 294 | lt2subd 11786 |
. . . . . . . 8
β’ (π β (π΅ β π΄) < ((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ))))) |
296 | 149, 195,
295 | ltled 11310 |
. . . . . . 7
β’ (π β (π΅ β π΄) β€ ((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ))))) |
297 | 223 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...(π β 1))) β π β β) |
298 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (1...(π β 1))) β π β (1...(π β 1))) |
299 | 243 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (1...(π β 1))) β π β β€) |
300 | | elfzm11 13519 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((1
β β€ β§ π
β β€) β (π
β (1...(π β 1))
β (π β β€
β§ 1 β€ π β§ π < π))) |
301 | 244, 299,
300 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (1...(π β 1))) β (π β (1...(π β 1)) β (π β β€ β§ 1 β€ π β§ π < π))) |
302 | 298, 301 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (1...(π β 1))) β (π β β€ β§ 1 β€ π β§ π < π)) |
303 | 302 | simp3d 1145 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...(π β 1))) β π < π) |
304 | 297 | nnred 12175 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (1...(π β 1))) β π β β) |
305 | 112 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (1...(π β 1))) β π β β) |
306 | 304, 305 | ltnled 11309 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...(π β 1))) β (π < π β Β¬ π β€ π)) |
307 | 303, 306 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...(π β 1))) β Β¬ π β€ π) |
308 | | infssuzle 12863 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β
(β€β₯β1) β§ π β π) β inf(π, β, < ) β€ π) |
309 | 65, 308 | mpan 689 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β inf(π, β, < ) β€ π) |
310 | 64, 309 | eqbrtrid 5145 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π β€ π) |
311 | 307, 310 | nsyl 140 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...(π β 1))) β Β¬ π β π) |
312 | 297, 311 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...(π β 1))) β (π β β β§ Β¬ π β π)) |
313 | 87, 88, 89, 90, 91, 67, 92, 4, 93, 11, 9, 94, 95, 8, 6, 61 | ovolicc2lem2 24898 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π β β β§ Β¬ π β π)) β (2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅) |
314 | 312, 313 | syldan 592 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(π β 1))) β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β€ π΅) |
315 | 314 | iftrued 4499 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(π β 1))) β if((2nd
β(πΉβ(πΊβ(πΎβπ)))) β€ π΅, (2nd β(πΉβ(πΊβ(πΎβπ)))), π΅) = (2nd β(πΉβ(πΊβ(πΎβπ))))) |
316 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π‘ = (πΎβπ) β (πΉβ(πΊβπ‘)) = (πΉβ(πΊβ(πΎβπ)))) |
317 | 316 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π‘ = (πΎβπ) β (2nd β(πΉβ(πΊβπ‘))) = (2nd β(πΉβ(πΊβ(πΎβπ))))) |
318 | 317 | breq1d 5120 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ = (πΎβπ) β ((2nd β(πΉβ(πΊβπ‘))) β€ π΅ β (2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅)) |
319 | 318, 317 | ifbieq1d 4515 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = (πΎβπ) β if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) = if((2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅, (2nd β(πΉβ(πΊβ(πΎβπ)))), π΅)) |
320 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π‘ = (πΎβπ) β (π»βπ‘) = (π»β(πΎβπ))) |
321 | 319, 320 | eleq12d 2832 |
. . . . . . . . . . . . . . . 16
β’ (π‘ = (πΎβπ) β (if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘) β if((2nd β(πΉβ(πΊβ(πΎβπ)))) β€ π΅, (2nd β(πΉβ(πΊβ(πΎβπ)))), π΅) β (π»β(πΎβπ)))) |
322 | 94 | ralrimiva 3144 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) |
323 | 322 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(π β 1))) β βπ‘ β π if((2nd β(πΉβ(πΊβπ‘))) β€ π΅, (2nd β(πΉβ(πΊβπ‘))), π΅) β (π»βπ‘)) |
324 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ:ββΆπ β§ π β β) β (πΎβπ) β π) |
325 | 10, 223, 324 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(π β 1))) β (πΎβπ) β π) |
326 | 321, 323,
325 | rspcdva 3585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(π β 1))) β if((2nd
β(πΉβ(πΊβ(πΎβπ)))) β€ π΅, (2nd β(πΉβ(πΊβ(πΎβπ)))), π΅) β (π»β(πΎβπ))) |
327 | 315, 326 | eqeltrrd 2839 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(π β 1))) β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β (π»β(πΎβπ))) |
328 | 5, 6, 7, 8, 9 | algrp1 16457 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΎβ(π + 1)) = (π»β(πΎβπ))) |
329 | 223, 328 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(π β 1))) β (πΎβ(π + 1)) = (π»β(πΎβπ))) |
330 | 327, 329 | eleqtrrd 2841 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...(π β 1))) β (2nd
β(πΉβ(πΊβ(πΎβπ)))) β (πΎβ(π + 1))) |
331 | 223, 270 | sylan2 594 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(π β 1))) β (πΎβ(π + 1)) β π) |
332 | 87, 88, 89, 90, 91, 67, 92, 4, 93 | ovolicc2lem1 24897 |
. . . . . . . . . . . . . 14
β’ ((π β§ (πΎβ(π + 1)) β π) β ((2nd β(πΉβ(πΊβ(πΎβπ)))) β (πΎβ(π + 1)) β ((2nd β(πΉβ(πΊβ(πΎβπ)))) β β β§ (1st
β(πΉβ(πΊβ(πΎβ(π + 1))))) < (2nd β(πΉβ(πΊβ(πΎβπ)))) β§ (2nd β(πΉβ(πΊβ(πΎβπ)))) < (2nd β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
333 | 331, 332 | syldan 592 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...(π β 1))) β ((2nd
β(πΉβ(πΊβ(πΎβπ)))) β (πΎβ(π + 1)) β ((2nd β(πΉβ(πΊβ(πΎβπ)))) β β β§ (1st
β(πΉβ(πΊβ(πΎβ(π + 1))))) < (2nd β(πΉβ(πΊβ(πΎβπ)))) β§ (2nd β(πΉβ(πΊβ(πΎβπ)))) < (2nd β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
334 | 330, 333 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(π β 1))) β ((2nd
β(πΉβ(πΊβ(πΎβπ)))) β β β§ (1st
β(πΉβ(πΊβ(πΎβ(π + 1))))) < (2nd β(πΉβ(πΊβ(πΎβπ)))) β§ (2nd β(πΉβ(πΊβ(πΎβπ)))) < (2nd β(πΉβ(πΊβ(πΎβ(π + 1))))))) |
335 | 334 | simp2d 1144 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(π β 1))) β (1st
β(πΉβ(πΊβ(πΎβ(π + 1))))) < (2nd β(πΉβ(πΊβ(πΎβπ))))) |
336 | 275, 224,
335 | ltled 11310 |
. . . . . . . . . 10
β’ ((π β§ π β (1...(π β 1))) β (1st
β(πΉβ(πΊβ(πΎβ(π + 1))))) β€ (2nd β(πΉβ(πΊβ(πΎβπ))))) |
337 | 222, 275,
224, 336 | fsumle 15691 |
. . . . . . . . 9
β’ (π β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) β€ Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ))))) |
338 | 225, 276 | subge0d 11752 |
. . . . . . . . 9
β’ (π β (0 β€ (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))) β€ Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))))) |
339 | 337, 338 | mpbird 257 |
. . . . . . . 8
β’ (π β 0 β€ (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))))) |
340 | 225, 276 | resubcld 11590 |
. . . . . . . . 9
β’ (π β (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))) β β) |
341 | 195, 340 | addge01d 11750 |
. . . . . . . 8
β’ (π β (0 β€ (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))) β ((2nd
β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) β€ (((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) + (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1))))))))) |
342 | 339, 341 | mpbid 231 |
. . . . . . 7
β’ (π β ((2nd
β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) β€ (((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) + (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
343 | 149, 195,
281, 296, 342 | letrd 11319 |
. . . . . 6
β’ (π β (π΅ β π΄) β€ (((2nd β(πΉβ(πΊβ(πΎβπ)))) β (1st β(πΉβ(πΊβπΆ)))) + (Ξ£π β (1...(π β 1))(2nd β(πΉβ(πΊβ(πΎβπ)))) β Ξ£π β (1...(π β 1))(1st β(πΉβ(πΊβ(πΎβ(π + 1)))))))) |
344 | 343, 280 | breqtrrd 5138 |
. . . . 5
β’ (π β (π΅ β π΄) β€ Ξ£π β ((πΊ β πΎ) β (1...π))(((abs β β ) β πΉ)βπ)) |
345 | 344 | adantr 482 |
. . . 4
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (π΅ β π΄) β€ Ξ£π β ((πΊ β πΎ) β (1...π))(((abs β β ) β πΉ)βπ)) |
346 | | fzfid 13885 |
. . . . 5
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (1...π§) β Fin) |
347 | 161 | adantlr 714 |
. . . . 5
β’ (((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β§ π β (1...π§)) β (((abs β β ) β
πΉ)βπ) β β) |
348 | 160 | simprd 497 |
. . . . . 6
β’ ((π β§ π β (1...π§)) β 0 β€ (((abs β β )
β πΉ)βπ)) |
349 | 348 | adantlr 714 |
. . . . 5
β’ (((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β§ π β (1...π§)) β 0 β€ (((abs β β )
β πΉ)βπ)) |
350 | 21 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β ((πΊ β πΎ) β (1...π)) β β) |
351 | 350 | sselda 3949 |
. . . . . . . . . . 11
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π¦ β β) |
352 | 351 | nnred 12175 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π¦ β β) |
353 | 28 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π§ β β) |
354 | | ltle 11250 |
. . . . . . . . . 10
β’ ((π¦ β β β§ π§ β β) β (π¦ < π§ β π¦ β€ π§)) |
355 | 352, 353,
354 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β (π¦ < π§ β π¦ β€ π§)) |
356 | 351, 5 | eleqtrdi 2848 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π¦ β
(β€β₯β1)) |
357 | | nnz 12527 |
. . . . . . . . . . 11
β’ (π§ β β β π§ β
β€) |
358 | 357 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β π§ β β€) |
359 | | elfz5 13440 |
. . . . . . . . . 10
β’ ((π¦ β
(β€β₯β1) β§ π§ β β€) β (π¦ β (1...π§) β π¦ β€ π§)) |
360 | 356, 358,
359 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β (π¦ β (1...π§) β π¦ β€ π§)) |
361 | 355, 360 | sylibrd 259 |
. . . . . . . 8
β’ (((π β§ π§ β β) β§ π¦ β ((πΊ β πΎ) β (1...π))) β (π¦ < π§ β π¦ β (1...π§))) |
362 | 361 | ralimdva 3165 |
. . . . . . 7
β’ ((π β§ π§ β β) β (βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§ β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β (1...π§))) |
363 | 362 | impr 456 |
. . . . . 6
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β (1...π§)) |
364 | | dfss3 3937 |
. . . . . 6
β’ (((πΊ β πΎ) β (1...π)) β (1...π§) β βπ¦ β ((πΊ β πΎ) β (1...π))π¦ β (1...π§)) |
365 | 363, 364 | sylibr 233 |
. . . . 5
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β ((πΊ β πΎ) β (1...π)) β (1...π§)) |
366 | 346, 347,
349, 365 | fsumless 15688 |
. . . 4
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β Ξ£π β ((πΊ β πΎ) β (1...π))(((abs β β ) β πΉ)βπ) β€ Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ)) |
367 | 175, 180,
163, 345, 366 | letrd 11319 |
. . 3
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (π΅ β π΄) β€ Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ)) |
368 | | eqidd 2738 |
. . . . . 6
β’ (((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β§ π β (1...π§)) β (((abs β β ) β
πΉ)βπ) = (((abs β β ) β πΉ)βπ)) |
369 | | simprl 770 |
. . . . . . 7
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β π§ β β) |
370 | 369, 5 | eleqtrdi 2848 |
. . . . . 6
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β π§ β
(β€β₯β1)) |
371 | 347 | recnd 11190 |
. . . . . 6
β’ (((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β§ π β (1...π§)) β (((abs β β ) β
πΉ)βπ) β β) |
372 | 368, 370,
371 | fsumser 15622 |
. . . . 5
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ) = (seq1( + , ((abs β β )
β πΉ))βπ§)) |
373 | 90 | fveq1i 6848 |
. . . . 5
β’ (πβπ§) = (seq1( + , ((abs β β )
β πΉ))βπ§) |
374 | 372, 373 | eqtr4di 2795 |
. . . 4
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ) = (πβπ§)) |
375 | 166 | ffnd 6674 |
. . . . . 6
β’ (π β π Fn β) |
376 | | fnfvelrn 7036 |
. . . . . 6
β’ ((π Fn β β§ π§ β β) β (πβπ§) β ran π) |
377 | 375, 369,
376 | syl2an2r 684 |
. . . . 5
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (πβπ§) β ran π) |
378 | | supxrub 13250 |
. . . . 5
β’ ((ran
π β
β* β§ (πβπ§) β ran π) β (πβπ§) β€ sup(ran π, β*, <
)) |
379 | 171, 377,
378 | syl2an2r 684 |
. . . 4
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (πβπ§) β€ sup(ran π, β*, <
)) |
380 | 374, 379 | eqbrtrd 5132 |
. . 3
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β Ξ£π β (1...π§)(((abs β β ) β πΉ)βπ) β€ sup(ran π, β*, <
)) |
381 | 151, 164,
174, 367, 380 | xrletrd 13088 |
. 2
β’ ((π β§ (π§ β β β§ βπ¦ β ((πΊ β πΎ) β (1...π))π¦ < π§)) β (π΅ β π΄) β€ sup(ran π, β*, <
)) |
382 | 148, 381 | rexlimddv 3159 |
1
β’ (π β (π΅ β π΄) β€ sup(ran π, β*, <
)) |