Step | Hyp | Ref
| Expression |
1 | | mtest.n |
. . 3
β’ (π β π β β€) |
2 | | mtest.d |
. . 3
β’ (π β seqπ( + , π) β dom β ) |
3 | | mtest.z |
. . . . . 6
β’ π =
(β€β₯βπ) |
4 | | mtest.c |
. . . . . . 7
β’ ((π β§ π β π) β (πβπ) β β) |
5 | 4 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β π) β (πβπ) β β) |
6 | 3, 1, 5 | serf 13943 |
. . . . 5
β’ (π β seqπ( + , π):πβΆβ) |
7 | 6 | ffvelcdmda 7040 |
. . . 4
β’ ((π β§ π β π) β (seqπ( + , π)βπ) β β) |
8 | 7 | ralrimiva 3144 |
. . 3
β’ (π β βπ β π (seqπ( + , π)βπ) β β) |
9 | 3 | climbdd 15563 |
. . 3
β’ ((π β β€ β§ seqπ( + , π) β dom β β§ βπ β π (seqπ( + , π)βπ) β β) β βπ¦ β β βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦) |
10 | 1, 2, 8, 9 | syl3anc 1372 |
. 2
β’ (π β βπ¦ β β βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦) |
11 | 1 | adantr 482 |
. . 3
β’ ((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β π β β€) |
12 | | seqfn 13925 |
. . . . . . 7
β’ (π β β€ β seqπ( βf + , πΉ) Fn
(β€β₯βπ)) |
13 | 1, 12 | syl 17 |
. . . . . 6
β’ (π β seqπ( βf + , πΉ) Fn (β€β₯βπ)) |
14 | 3 | fneq2i 6605 |
. . . . . 6
β’ (seqπ( βf + , πΉ) Fn π β seqπ( βf + , πΉ) Fn (β€β₯βπ)) |
15 | 13, 14 | sylibr 233 |
. . . . 5
β’ (π β seqπ( βf + , πΉ) Fn π) |
16 | | mtest.t |
. . . . 5
β’ (π β seqπ( βf + , πΉ)(βπ’βπ)π) |
17 | | ulmf2 25759 |
. . . . 5
β’
((seqπ(
βf + , πΉ)
Fn π β§ seqπ( βf + , πΉ)(βπ’βπ)π) β seqπ( βf + , πΉ):πβΆ(β βm π)) |
18 | 15, 16, 17 | syl2anc 585 |
. . . 4
β’ (π β seqπ( βf + , πΉ):πβΆ(β βm π)) |
19 | 18 | adantr 482 |
. . 3
β’ ((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β seqπ( βf + , πΉ):πβΆ(β βm π)) |
20 | | simplrl 776 |
. . . 4
β’ (((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β π¦ β β) |
21 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π₯ = π§ β ((πΉβπ)βπ₯) = ((πΉβπ)βπ§)) |
22 | 21 | mpteq2dv 5212 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (π β π β¦ ((πΉβπ)βπ₯)) = (π β π β¦ ((πΉβπ)βπ§))) |
23 | 22 | seqeq3d 13921 |
. . . . . . . . . . 11
β’ (π₯ = π§ β seqπ( + , (π β π β¦ ((πΉβπ)βπ₯))) = seqπ( + , (π β π β¦ ((πΉβπ)βπ§)))) |
24 | 23 | fveq1d 6849 |
. . . . . . . . . 10
β’ (π₯ = π§ β (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ) = (seqπ( + , (π β π β¦ ((πΉβπ)βπ§)))βπ)) |
25 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β π β¦ (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ)) = (π₯ β π β¦ (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ)) |
26 | | fvex 6860 |
. . . . . . . . . 10
β’ (seqπ( + , (π β π β¦ ((πΉβπ)βπ§)))βπ) β V |
27 | 24, 25, 26 | fvmpt 6953 |
. . . . . . . . 9
β’ (π§ β π β ((π₯ β π β¦ (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ))βπ§) = (seqπ( + , (π β π β¦ ((πΉβπ)βπ§)))βπ)) |
28 | 27 | adantl 483 |
. . . . . . . 8
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β ((π₯ β π β¦ (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ))βπ§) = (seqπ( + , (π β π β¦ ((πΉβπ)βπ§)))βπ)) |
29 | | mtest.f |
. . . . . . . . . . . . . . 15
β’ (π β πΉ:πβΆ(β βm π)) |
30 | 29 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β πΉ:πβΆ(β βm π)) |
31 | 30 | feqmptd 6915 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β πΉ = (π β π β¦ (πΉβπ))) |
32 | 30 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β π) β (πΉβπ) β (β βm π)) |
33 | | elmapi 8794 |
. . . . . . . . . . . . . . . 16
β’ ((πΉβπ) β (β βm π) β (πΉβπ):πβΆβ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β π) β (πΉβπ):πβΆβ) |
35 | 34 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β π) β (πΉβπ) = (π₯ β π β¦ ((πΉβπ)βπ₯))) |
36 | 35 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (π β π β¦ (πΉβπ)) = (π β π β¦ (π₯ β π β¦ ((πΉβπ)βπ₯)))) |
37 | 31, 36 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β πΉ = (π β π β¦ (π₯ β π β¦ ((πΉβπ)βπ₯)))) |
38 | 37 | seqeq3d 13921 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β seqπ( βf + , πΉ) = seqπ( βf + , (π β π β¦ (π₯ β π β¦ ((πΉβπ)βπ₯))))) |
39 | 38 | fveq1d 6849 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (seqπ( βf + , πΉ)βπ) = (seqπ( βf + , (π β π β¦ (π₯ β π β¦ ((πΉβπ)βπ₯))))βπ)) |
40 | | mtest.s |
. . . . . . . . . . . 12
β’ (π β π β π) |
41 | 40 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β π β π) |
42 | | simplr 768 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β π β π) |
43 | 42, 3 | eleqtrdi 2848 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β π β (β€β₯βπ)) |
44 | | elfzuz 13444 |
. . . . . . . . . . . . . 14
β’ (π β (π...π) β π β (β€β₯βπ)) |
45 | 44, 3 | eleqtrrdi 2849 |
. . . . . . . . . . . . 13
β’ (π β (π...π) β π β π) |
46 | 45 | ssriv 3953 |
. . . . . . . . . . . 12
β’ (π...π) β π |
47 | 46 | a1i 11 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (π...π) β π) |
48 | 34 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’
((((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β π) β§ π₯ β π) β ((πΉβπ)βπ₯) β β) |
49 | 48 | anasss 468 |
. . . . . . . . . . 11
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ (π β π β§ π₯ β π)) β ((πΉβπ)βπ₯) β β) |
50 | 41, 43, 47, 49 | seqof2 13973 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (seqπ( βf + , (π β π β¦ (π₯ β π β¦ ((πΉβπ)βπ₯))))βπ) = (π₯ β π β¦ (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ))) |
51 | 39, 50 | eqtrd 2777 |
. . . . . . . . 9
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (seqπ( βf + , πΉ)βπ) = (π₯ β π β¦ (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ))) |
52 | 51 | fveq1d 6849 |
. . . . . . . 8
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β ((seqπ( βf + , πΉ)βπ)βπ§) = ((π₯ β π β¦ (seqπ( + , (π β π β¦ ((πΉβπ)βπ₯)))βπ))βπ§)) |
53 | 45 | adantl 483 |
. . . . . . . . . 10
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β π β π) |
54 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβπ) = (πΉβπ)) |
55 | 54 | fveq1d 6849 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβπ)βπ§) = ((πΉβπ)βπ§)) |
56 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π β π β¦ ((πΉβπ)βπ§)) = (π β π β¦ ((πΉβπ)βπ§)) |
57 | | fvex 6860 |
. . . . . . . . . . 11
β’ ((πΉβπ)βπ§) β V |
58 | 55, 56, 57 | fvmpt 6953 |
. . . . . . . . . 10
β’ (π β π β ((π β π β¦ ((πΉβπ)βπ§))βπ) = ((πΉβπ)βπ§)) |
59 | 53, 58 | syl 17 |
. . . . . . . . 9
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β ((π β π β¦ ((πΉβπ)βπ§))βπ) = ((πΉβπ)βπ§)) |
60 | | simplr 768 |
. . . . . . . . . . . . . 14
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β π) β π§ β π) |
61 | 34, 60 | ffvelcdmd 7041 |
. . . . . . . . . . . . 13
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β π) β ((πΉβπ)βπ§) β β) |
62 | 61 | fmpttd 7068 |
. . . . . . . . . . . 12
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (π β π β¦ ((πΉβπ)βπ§)):πβΆβ) |
63 | 62 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β π) β ((π β π β¦ ((πΉβπ)βπ§))βπ) β β) |
64 | 45, 63 | sylan2 594 |
. . . . . . . . . 10
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β ((π β π β¦ ((πΉβπ)βπ§))βπ) β β) |
65 | 59, 64 | eqeltrrd 2839 |
. . . . . . . . 9
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β ((πΉβπ)βπ§) β β) |
66 | 59, 43, 65 | fsumser 15622 |
. . . . . . . 8
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)((πΉβπ)βπ§) = (seqπ( + , (π β π β¦ ((πΉβπ)βπ§)))βπ)) |
67 | 28, 52, 66 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β ((seqπ( βf + , πΉ)βπ)βπ§) = Ξ£π β (π...π)((πΉβπ)βπ§)) |
68 | 67 | fveq2d 6851 |
. . . . . 6
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβ((seqπ( βf + , πΉ)βπ)βπ§)) = (absβΞ£π β (π...π)((πΉβπ)βπ§))) |
69 | | fzfid 13885 |
. . . . . . . . 9
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (π...π) β Fin) |
70 | 69, 65 | fsumcl 15625 |
. . . . . . . 8
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)((πΉβπ)βπ§) β β) |
71 | 70 | abscld 15328 |
. . . . . . 7
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβΞ£π β (π...π)((πΉβπ)βπ§)) β β) |
72 | 65 | abscld 15328 |
. . . . . . . 8
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β (absβ((πΉβπ)βπ§)) β β) |
73 | 69, 72 | fsumrecl 15626 |
. . . . . . 7
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(absβ((πΉβπ)βπ§)) β β) |
74 | 20 | adantr 482 |
. . . . . . 7
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β π¦ β β) |
75 | 69, 65 | fsumabs 15693 |
. . . . . . 7
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβΞ£π β (π...π)((πΉβπ)βπ§)) β€ Ξ£π β (π...π)(absβ((πΉβπ)βπ§))) |
76 | | simp-4l 782 |
. . . . . . . . . 10
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β π) |
77 | 76, 53, 4 | syl2anc 585 |
. . . . . . . . 9
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β (πβπ) β β) |
78 | 69, 77 | fsumrecl 15626 |
. . . . . . . 8
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(πβπ) β β) |
79 | | simplr 768 |
. . . . . . . . . 10
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β π§ β π) |
80 | | mtest.l |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ π§ β π)) β (absβ((πΉβπ)βπ§)) β€ (πβπ)) |
81 | 76, 53, 79, 80 | syl12anc 836 |
. . . . . . . . 9
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β (absβ((πΉβπ)βπ§)) β€ (πβπ)) |
82 | 69, 72, 77, 81 | fsumle 15691 |
. . . . . . . 8
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(absβ((πΉβπ)βπ§)) β€ Ξ£π β (π...π)(πβπ)) |
83 | 78 | recnd 11190 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(πβπ) β β) |
84 | 83 | abscld 15328 |
. . . . . . . . 9
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβΞ£π β (π...π)(πβπ)) β β) |
85 | 78 | leabsd 15306 |
. . . . . . . . 9
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(πβπ) β€ (absβΞ£π β (π...π)(πβπ))) |
86 | | eqidd 2738 |
. . . . . . . . . . . 12
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β (πβπ) = (πβπ)) |
87 | 76, 53, 5 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π β§ (π¦ β β β§
βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β§ π β (π...π)) β (πβπ) β β) |
88 | 86, 43, 87 | fsumser 15622 |
. . . . . . . . . . 11
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(πβπ) = (seqπ( + , π)βπ)) |
89 | 88 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβΞ£π β (π...π)(πβπ)) = (absβ(seqπ( + , π)βπ))) |
90 | | simprr 772 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦) |
91 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (seqπ( + , π)βπ) = (seqπ( + , π)βπ)) |
92 | 91 | fveq2d 6851 |
. . . . . . . . . . . . . 14
β’ (π = π β (absβ(seqπ( + , π)βπ)) = (absβ(seqπ( + , π)βπ))) |
93 | 92 | breq1d 5120 |
. . . . . . . . . . . . 13
β’ (π = π β ((absβ(seqπ( + , π)βπ)) β€ π¦ β (absβ(seqπ( + , π)βπ)) β€ π¦)) |
94 | 93 | rspccva 3583 |
. . . . . . . . . . . 12
β’
((βπ β
π (absβ(seqπ( + , π)βπ)) β€ π¦ β§ π β π) β (absβ(seqπ( + , π)βπ)) β€ π¦) |
95 | 90, 94 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β (absβ(seqπ( + , π)βπ)) β€ π¦) |
96 | 95 | adantr 482 |
. . . . . . . . . 10
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβ(seqπ( + , π)βπ)) β€ π¦) |
97 | 89, 96 | eqbrtrd 5132 |
. . . . . . . . 9
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβΞ£π β (π...π)(πβπ)) β€ π¦) |
98 | 78, 84, 74, 85, 97 | letrd 11319 |
. . . . . . . 8
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(πβπ) β€ π¦) |
99 | 73, 78, 74, 82, 98 | letrd 11319 |
. . . . . . 7
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β Ξ£π β (π...π)(absβ((πΉβπ)βπ§)) β€ π¦) |
100 | 71, 73, 74, 75, 99 | letrd 11319 |
. . . . . 6
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβΞ£π β (π...π)((πΉβπ)βπ§)) β€ π¦) |
101 | 68, 100 | eqbrtrd 5132 |
. . . . 5
β’ ((((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β§ π§ β π) β (absβ((seqπ( βf + , πΉ)βπ)βπ§)) β€ π¦) |
102 | 101 | ralrimiva 3144 |
. . . 4
β’ (((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β βπ§ β π (absβ((seqπ( βf + , πΉ)βπ)βπ§)) β€ π¦) |
103 | | brralrspcev 5170 |
. . . 4
β’ ((π¦ β β β§
βπ§ β π (absβ((seqπ( βf + , πΉ)βπ)βπ§)) β€ π¦) β βπ₯ β β βπ§ β π (absβ((seqπ( βf + , πΉ)βπ)βπ§)) β€ π₯) |
104 | 20, 102, 103 | syl2anc 585 |
. . 3
β’ (((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β§ π β π) β βπ₯ β β βπ§ β π (absβ((seqπ( βf + , πΉ)βπ)βπ§)) β€ π₯) |
105 | 16 | adantr 482 |
. . 3
β’ ((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β seqπ( βf + , πΉ)(βπ’βπ)π) |
106 | 3, 11, 19, 104, 105 | ulmbdd 25773 |
. 2
β’ ((π β§ (π¦ β β β§ βπ β π (absβ(seqπ( + , π)βπ)) β€ π¦)) β βπ₯ β β βπ§ β π (absβ(πβπ§)) β€ π₯) |
107 | 10, 106 | rexlimddv 3159 |
1
β’ (π β βπ₯ β β βπ§ β π (absβ(πβπ§)) β€ π₯) |