Step | Hyp | Ref
| Expression |
1 | | cvgcmp.1 |
. 2
β’ π =
(β€β₯βπ) |
2 | | seqex 13915 |
. . 3
β’ seqπ( + , πΊ) β V |
3 | 2 | a1i 11 |
. 2
β’ (π β seqπ( + , πΊ) β V) |
4 | | cvgcmp.2 |
. . . . . . . 8
β’ (π β π β π) |
5 | 4, 1 | eleqtrdi 2848 |
. . . . . . 7
β’ (π β π β (β€β₯βπ)) |
6 | | eluzel2 12775 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β π β β€) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (π β π β β€) |
8 | | cvgcmp.5 |
. . . . . 6
β’ (π β seqπ( + , πΉ) β dom β ) |
9 | 1 | climcau 15562 |
. . . . . 6
β’ ((π β β€ β§ seqπ( + , πΉ) β dom β ) β βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) |
10 | 7, 8, 9 | syl2anc 585 |
. . . . 5
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) |
11 | | cvgcmp.3 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ) β β) |
12 | 1, 7, 11 | serfre 13944 |
. . . . . . . . . 10
β’ (π β seqπ( + , πΉ):πβΆβ) |
13 | 12 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
14 | 13 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π β π) β (seqπ( + , πΉ)βπ) β β) |
15 | 14 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ β π (seqπ( + , πΉ)βπ) β β) |
16 | 1 | r19.29uz 15242 |
. . . . . . . 8
β’
((βπ β
π (seqπ( + , πΉ)βπ) β β β§ βπ β π βπ β (β€β₯βπ)(absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯)) |
17 | 16 | ex 414 |
. . . . . . 7
β’
(βπ β
π (seqπ( + , πΉ)βπ) β β β (βπ β π βπ β (β€β₯βπ)(absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯ β βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯))) |
18 | 15, 17 | syl 17 |
. . . . . 6
β’ (π β (βπ β π βπ β (β€β₯βπ)(absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯ β βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯))) |
19 | 18 | ralimdv 3167 |
. . . . 5
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)(absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯ β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯))) |
20 | 10, 19 | mpd 15 |
. . . 4
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯)) |
21 | 1 | uztrn2 12789 |
. . . . . . . . . . 11
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
22 | 4, 21 | sylan 581 |
. . . . . . . . . 10
β’ ((π β§ π β (β€β₯βπ)) β π β π) |
23 | | cvgcmp.4 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β (πΊβπ) β β) |
24 | 1, 7, 23 | serfre 13944 |
. . . . . . . . . . . 12
β’ (π β seqπ( + , πΊ):πβΆβ) |
25 | 24 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (seqπ( + , πΊ)βπ) β β) |
26 | 25 | recnd 11190 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (seqπ( + , πΊ)βπ) β β) |
27 | 22, 26 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β (seqπ( + , πΊ)βπ) β β) |
28 | 27 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β (β€β₯βπ)(seqπ( + , πΊ)βπ) β β) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
βπ β
(β€β₯βπ)(seqπ( + , πΊ)βπ) β β) |
30 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π) |
31 | 30, 12 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β seqπ( + , πΉ):πβΆβ) |
32 | 30, 4 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β π) |
33 | | simprl 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β (β€β₯βπ)) |
34 | 1 | uztrn2 12789 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
35 | 32, 33, 34 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β π) |
36 | 31, 35 | ffvelcdmd 7041 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΉ)βπ) β β) |
37 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(β€β₯βπ) = (β€β₯βπ) |
38 | 37 | uztrn2 12789 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
39 | 38 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β (β€β₯βπ)) |
40 | 32, 39, 21 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β π) |
41 | 30, 40, 13 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΉ)βπ) β β) |
42 | 30, 40, 25 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΊ)βπ) β β) |
43 | 30, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β seqπ( + , πΊ):πβΆβ) |
44 | 43, 35 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΊ)βπ) β β) |
45 | 42, 44 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) β β) |
46 | 35, 1 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β (β€β₯βπ)) |
47 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β (β€β₯βπ)) |
48 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π...π) β π β (β€β₯βπ)) |
49 | 48, 1 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π...π) β π β π) |
50 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πΉβπ) = (πΉβπ)) |
51 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = π β (πΊβπ) = (πΊβπ)) |
52 | 50, 51 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β ((πΉβπ) β (πΊβπ)) = ((πΉβπ) β (πΊβπ))) |
53 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π β¦ ((πΉβπ) β (πΊβπ))) = (π β π β¦ ((πΉβπ) β (πΊβπ))) |
54 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΉβπ) β (πΊβπ)) β V |
55 | 52, 53, 54 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ) = ((πΉβπ) β (πΊβπ))) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ) = ((πΉβπ) β (πΊβπ))) |
57 | 11, 23 | resubcld 11590 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β ((πΉβπ) β (πΊβπ)) β β) |
58 | 56, 57 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ) β β) |
59 | 30, 49, 58 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ) β β) |
60 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((π + 1)...π) β π β (β€β₯β(π + 1))) |
61 | | peano2uz 12833 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β
(β€β₯βπ) β (π + 1) β
(β€β₯βπ)) |
62 | 33, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (π + 1) β
(β€β₯βπ)) |
63 | 37 | uztrn2 12789 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π + 1) β
(β€β₯βπ) β§ π β (β€β₯β(π + 1))) β π β
(β€β₯βπ)) |
64 | 62, 63 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (β€β₯β(π + 1))) β π β
(β€β₯βπ)) |
65 | | cvgcmp.7 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β€ (πΉβπ)) |
66 | 1 | uztrn2 12789 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
67 | 4, 66 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β (β€β₯βπ)) β π β π) |
68 | 11, 23 | subge0d 11752 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π) β (0 β€ ((πΉβπ) β (πΊβπ)) β (πΊβπ) β€ (πΉβπ))) |
69 | 67, 68 | syldan 592 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (β€β₯βπ)) β (0 β€ ((πΉβπ) β (πΊβπ)) β (πΊβπ) β€ (πΉβπ))) |
70 | 65, 69 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (β€β₯βπ)) β 0 β€ ((πΉβπ) β (πΊβπ))) |
71 | 67, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (β€β₯βπ)) β ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ) = ((πΉβπ) β (πΊβπ))) |
72 | 70, 71 | breqtrrd 5138 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (β€β₯βπ)) β 0 β€ ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ)) |
73 | 30, 64, 72 | syl2an2r 684 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (β€β₯β(π + 1))) β 0 β€ ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ)) |
74 | 60, 73 | sylan2 594 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β ((π + 1)...π)) β 0 β€ ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ)) |
75 | 46, 47, 59, 74 | sermono 13947 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , (π β π β¦ ((πΉβπ) β (πΊβπ))))βπ) β€ (seqπ( + , (π β π β¦ ((πΉβπ) β (πΊβπ))))βπ)) |
76 | | elfzuz 13444 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π...π) β π β (β€β₯βπ)) |
77 | 76, 1 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π...π) β π β π) |
78 | 11 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (πΉβπ) β β) |
79 | 30, 77, 78 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΉβπ) β β) |
80 | 23 | recnd 11190 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β π) β (πΊβπ) β β) |
81 | 30, 77, 80 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΊβπ) β β) |
82 | 30, 77, 56 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ) = ((πΉβπ) β (πΊβπ))) |
83 | 46, 79, 81, 82 | sersub 13958 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , (π β π β¦ ((πΉβπ) β (πΊβπ))))βπ) = ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ))) |
84 | 40, 1 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π β (β€β₯βπ)) |
85 | 30, 49, 78 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΉβπ) β β) |
86 | 30, 49, 80 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΊβπ) β β) |
87 | 30, 49, 56 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β ((π β π β¦ ((πΉβπ) β (πΊβπ)))βπ) = ((πΉβπ) β (πΊβπ))) |
88 | 84, 85, 86, 87 | sersub 13958 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , (π β π β¦ ((πΉβπ) β (πΊβπ))))βπ) = ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ))) |
89 | 75, 83, 88 | 3brtr3d 5141 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ)) β€ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ))) |
90 | 41, 42 | resubcld 11590 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ)) β β) |
91 | 36, 44, 90 | lesubaddd 11759 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ)) β€ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ)) β (seqπ( + , πΉ)βπ) β€ (((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ)) + (seqπ( + , πΊ)βπ)))) |
92 | 89, 91 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΉ)βπ) β€ (((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ)) + (seqπ( + , πΊ)βπ))) |
93 | 41 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΉ)βπ) β β) |
94 | 42 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΊ)βπ) β β) |
95 | 44 | recnd 11190 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΊ)βπ) β β) |
96 | 93, 94, 95 | subsubd 11547 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β ((seqπ( + , πΉ)βπ) β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) = (((seqπ( + , πΉ)βπ) β (seqπ( + , πΊ)βπ)) + (seqπ( + , πΊ)βπ))) |
97 | 92, 96 | breqtrrd 5138 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΉ)βπ) β€ ((seqπ( + , πΉ)βπ) β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)))) |
98 | 36, 41, 45, 97 | lesubd 11766 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) β€ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) |
99 | 41, 36 | resubcld 11590 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) β β) |
100 | | rpre 12930 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β+
β π₯ β
β) |
101 | 100 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β π₯ β β) |
102 | | lelttr 11252 |
. . . . . . . . . . . . . 14
β’
((((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) β β β§ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) β β β§ π₯ β β) β ((((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) β€ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) β§ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) < π₯) β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) < π₯)) |
103 | 45, 99, 101, 102 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β ((((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) β€ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) β§ ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) < π₯) β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) < π₯)) |
104 | 98, 103 | mpand 694 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) < π₯ β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) < π₯)) |
105 | 30, 49, 11 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΉβπ) β β) |
106 | 60, 64 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β ((π + 1)...π)) β π β (β€β₯βπ)) |
107 | | 0red 11165 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯βπ)) β 0 β
β) |
108 | 67, 23 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯βπ)) β (πΊβπ) β β) |
109 | 67, 11 | syldan 592 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
110 | | cvgcmp.6 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (β€β₯βπ)) β 0 β€ (πΊβπ)) |
111 | 107, 108,
109, 110, 65 | letrd 11319 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β€β₯βπ)) β 0 β€ (πΉβπ)) |
112 | 30, 106, 111 | syl2an2r 684 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β ((π + 1)...π)) β 0 β€ (πΉβπ)) |
113 | 46, 47, 105, 112 | sermono 13947 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΉ)βπ) β€ (seqπ( + , πΉ)βπ)) |
114 | 36, 41, 113 | abssubge0d 15323 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) = ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) |
115 | 114 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β
((absβ((seqπ( + ,
πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯ β ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ)) < π₯)) |
116 | 30, 49, 23 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (π...π)) β (πΊβπ) β β) |
117 | 30, 64, 110 | syl2an2r 684 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β (β€β₯β(π + 1))) β 0 β€ (πΊβπ)) |
118 | 60, 117 | sylan2 594 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β§ π β ((π + 1)...π)) β 0 β€ (πΊβπ)) |
119 | 46, 47, 116, 118 | sermono 13947 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (seqπ( + , πΊ)βπ) β€ (seqπ( + , πΊ)βπ)) |
120 | 44, 42, 119 | abssubge0d 15323 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) = ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) |
121 | 120 | breq1d 5120 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β
((absβ((seqπ( + ,
πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯ β ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ)) < π₯)) |
122 | 104, 115,
121 | 3imtr4d 294 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β+) β§ (π β
(β€β₯βπ) β§ π β (β€β₯βπ))) β
((absβ((seqπ( + ,
πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯ β (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
123 | 122 | anassrs 469 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β§ π β (β€β₯βπ)) β ((absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯ β (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
124 | 123 | adantld 492 |
. . . . . . . . 9
β’ ((((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β§ π β (β€β₯βπ)) β (((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
125 | 124 | ralimdva 3165 |
. . . . . . . 8
β’ (((π β§ π₯ β β+) β§ π β
(β€β₯βπ)) β (βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ β (β€β₯βπ)(absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
126 | 125 | reximdva 3166 |
. . . . . . 7
β’ ((π β§ π₯ β β+) β
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
127 | 37 | r19.29uz 15242 |
. . . . . . 7
β’
((βπ β
(β€β₯βπ)(seqπ( + , πΊ)βπ) β β β§ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
128 | 29, 126, 127 | syl6an 683 |
. . . . . 6
β’ ((π β§ π₯ β β+) β
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
129 | 128 | ralimdva 3165 |
. . . . 5
β’ (π β (βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
130 | 1, 37 | cau4 15248 |
. . . . . 6
β’ (π β π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯))) |
131 | 4, 130 | syl 17 |
. . . . 5
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯))) |
132 | 1, 37 | cau4 15248 |
. . . . . 6
β’ (π β π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
133 | 4, 132 | syl 17 |
. . . . 5
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
134 | 129, 131,
133 | 3imtr4d 294 |
. . . 4
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((seqπ( + , πΉ)βπ) β β β§ (absβ((seqπ( + , πΉ)βπ) β (seqπ( + , πΉ)βπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
135 | 20, 134 | mpd 15 |
. . 3
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
136 | 1 | uztrn2 12789 |
. . . . . . . 8
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
137 | | simpr 486 |
. . . . . . . . 9
β’
(((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) |
138 | 25 | biantrurd 534 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯ β ((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
139 | 137, 138 | imbitrid 243 |
. . . . . . . 8
β’ ((π β§ π β π) β (((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β ((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
140 | 136, 139 | sylan2 594 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β (β€β₯βπ))) β (((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β ((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
141 | 140 | anassrs 469 |
. . . . . 6
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β (((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β ((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
142 | 141 | ralimdva 3165 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
143 | 142 | reximdva 3166 |
. . . 4
β’ (π β (βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
144 | 143 | ralimdv 3167 |
. . 3
β’ (π β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯))) |
145 | 135, 144 | mpd 15 |
. 2
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((seqπ( + , πΊ)βπ) β β β§ (absβ((seqπ( + , πΊ)βπ) β (seqπ( + , πΊ)βπ))) < π₯)) |
146 | 1, 3, 145 | caurcvg2 15569 |
1
β’ (π β seqπ( + , πΊ) β dom β ) |