Step | Hyp | Ref
| Expression |
1 | | iserabs.1 |
. 2
β’ π =
(β€β₯βπ) |
2 | | iserabs.5 |
. 2
β’ (π β π β β€) |
3 | | iserabs.2 |
. . 3
β’ (π β seqπ( + , πΉ) β π΄) |
4 | | zex 9264 |
. . . . . . 7
β’ β€
β V |
5 | | uzssz 9549 |
. . . . . . 7
β’
(β€β₯βπ) β β€ |
6 | 4, 5 | ssexi 4143 |
. . . . . 6
β’
(β€β₯βπ) β V |
7 | 1, 6 | eqeltri 2250 |
. . . . 5
β’ π β V |
8 | 7 | mptex 5744 |
. . . 4
β’ (π β π β¦ (absβ(seqπ( + , πΉ)βπ))) β V |
9 | 8 | a1i 9 |
. . 3
β’ (π β (π β π β¦ (absβ(seqπ( + , πΉ)βπ))) β V) |
10 | | iserabs.6 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
11 | 1, 2, 10 | serf 10476 |
. . . 4
β’ (π β seqπ( + , πΉ):πβΆβ) |
12 | 11 | ffvelcdmda 5653 |
. . 3
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
13 | | simpr 110 |
. . . 4
β’ ((π β§ π β π) β π β π) |
14 | 12 | abscld 11192 |
. . . 4
β’ ((π β§ π β π) β (absβ(seqπ( + , πΉ)βπ)) β β) |
15 | | 2fveq3 5522 |
. . . . 5
β’ (π = π β (absβ(seqπ( + , πΉ)βπ)) = (absβ(seqπ( + , πΉ)βπ))) |
16 | | eqid 2177 |
. . . . 5
β’ (π β π β¦ (absβ(seqπ( + , πΉ)βπ))) = (π β π β¦ (absβ(seqπ( + , πΉ)βπ))) |
17 | 15, 16 | fvmptg 5594 |
. . . 4
β’ ((π β π β§ (absβ(seqπ( + , πΉ)βπ)) β β) β ((π β π β¦ (absβ(seqπ( + , πΉ)βπ)))βπ) = (absβ(seqπ( + , πΉ)βπ))) |
18 | 13, 14, 17 | syl2anc 411 |
. . 3
β’ ((π β§ π β π) β ((π β π β¦ (absβ(seqπ( + , πΉ)βπ)))βπ) = (absβ(seqπ( + , πΉ)βπ))) |
19 | 1, 3, 9, 2, 12, 18 | climabs 11330 |
. 2
β’ (π β (π β π β¦ (absβ(seqπ( + , πΉ)βπ))) β (absβπ΄)) |
20 | | iserabs.3 |
. 2
β’ (π β seqπ( + , πΊ) β π΅) |
21 | 18, 14 | eqeltrd 2254 |
. 2
β’ ((π β§ π β π) β ((π β π β¦ (absβ(seqπ( + , πΉ)βπ)))βπ) β β) |
22 | | iserabs.7 |
. . . . 5
β’ ((π β§ π β π) β (πΊβπ) = (absβ(πΉβπ))) |
23 | 10 | abscld 11192 |
. . . . 5
β’ ((π β§ π β π) β (absβ(πΉβπ)) β β) |
24 | 22, 23 | eqeltrd 2254 |
. . . 4
β’ ((π β§ π β π) β (πΊβπ) β β) |
25 | 1, 2, 24 | serfre 10477 |
. . 3
β’ (π β seqπ( + , πΊ):πβΆβ) |
26 | 25 | ffvelcdmda 5653 |
. 2
β’ ((π β§ π β π) β (seqπ( + , πΊ)βπ) β β) |
27 | 2 | adantr 276 |
. . . . . 6
β’ ((π β§ π β π) β π β β€) |
28 | | eluzelz 9539 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β π β β€) |
29 | 28, 1 | eleq2s 2272 |
. . . . . . 7
β’ (π β π β π β β€) |
30 | 29 | adantl 277 |
. . . . . 6
β’ ((π β§ π β π) β π β β€) |
31 | 27, 30 | fzfigd 10433 |
. . . . 5
β’ ((π β§ π β π) β (π...π) β Fin) |
32 | | elfzuz 10023 |
. . . . . . . 8
β’ (π β (π...π) β π β (β€β₯βπ)) |
33 | 32, 1 | eleqtrrdi 2271 |
. . . . . . 7
β’ (π β (π...π) β π β π) |
34 | 33, 10 | sylan2 286 |
. . . . . 6
β’ ((π β§ π β (π...π)) β (πΉβπ) β β) |
35 | 34 | adantlr 477 |
. . . . 5
β’ (((π β§ π β π) β§ π β (π...π)) β (πΉβπ) β β) |
36 | 31, 35 | fsumabs 11475 |
. . . 4
β’ ((π β§ π β π) β (absβΞ£π β (π...π)(πΉβπ)) β€ Ξ£π β (π...π)(absβ(πΉβπ))) |
37 | | eqidd 2178 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) = (πΉβπ)) |
38 | 1 | eleq2i 2244 |
. . . . . . . 8
β’ (π β π β π β (β€β₯βπ)) |
39 | 38 | biimpi 120 |
. . . . . . 7
β’ (π β π β π β (β€β₯βπ)) |
40 | 39 | adantl 277 |
. . . . . 6
β’ ((π β§ π β π) β π β (β€β₯βπ)) |
41 | 1 | eleq2i 2244 |
. . . . . . . 8
β’ (π β π β π β (β€β₯βπ)) |
42 | 41, 10 | sylan2br 288 |
. . . . . . 7
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
43 | 42 | adantlr 477 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
44 | 37, 40, 43 | fsum3ser 11407 |
. . . . 5
β’ ((π β§ π β π) β Ξ£π β (π...π)(πΉβπ) = (seqπ( + , πΉ)βπ)) |
45 | 44 | fveq2d 5521 |
. . . 4
β’ ((π β§ π β π) β (absβΞ£π β (π...π)(πΉβπ)) = (absβ(seqπ( + , πΉ)βπ))) |
46 | 22 | adantlr 477 |
. . . . . 6
β’ (((π β§ π β π) β§ π β π) β (πΊβπ) = (absβ(πΉβπ))) |
47 | 41, 46 | sylan2br 288 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (πΊβπ) = (absβ(πΉβπ))) |
48 | 23 | adantlr 477 |
. . . . . . 7
β’ (((π β§ π β π) β§ π β π) β (absβ(πΉβπ)) β β) |
49 | 41, 48 | sylan2br 288 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (absβ(πΉβπ)) β β) |
50 | 49 | recnd 7988 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (absβ(πΉβπ)) β β) |
51 | 47, 40, 50 | fsum3ser 11407 |
. . . 4
β’ ((π β§ π β π) β Ξ£π β (π...π)(absβ(πΉβπ)) = (seqπ( + , πΊ)βπ)) |
52 | 36, 45, 51 | 3brtr3d 4036 |
. . 3
β’ ((π β§ π β π) β (absβ(seqπ( + , πΉ)βπ)) β€ (seqπ( + , πΊ)βπ)) |
53 | 18, 52 | eqbrtrd 4027 |
. 2
β’ ((π β§ π β π) β ((π β π β¦ (absβ(seqπ( + , πΉ)βπ)))βπ) β€ (seqπ( + , πΊ)βπ)) |
54 | 1, 2, 19, 20, 21, 26, 53 | climle 11344 |
1
β’ (π β (absβπ΄) β€ π΅) |