Step | Hyp | Ref
| Expression |
1 | | radcnvlt.a |
. . . . 5
β’ (π β (absβπ) < π
) |
2 | | ressxr 11258 |
. . . . . . 7
β’ β
β β* |
3 | | radcnvlt.x |
. . . . . . . 8
β’ (π β π β β) |
4 | 3 | abscld 15383 |
. . . . . . 7
β’ (π β (absβπ) β
β) |
5 | 2, 4 | sselid 3981 |
. . . . . 6
β’ (π β (absβπ) β
β*) |
6 | | iccssxr 13407 |
. . . . . . 7
β’
(0[,]+β) β β* |
7 | | pser.g |
. . . . . . . 8
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
8 | | radcnv.a |
. . . . . . . 8
β’ (π β π΄:β0βΆβ) |
9 | | radcnv.r |
. . . . . . . 8
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
10 | 7, 8, 9 | radcnvcl 25929 |
. . . . . . 7
β’ (π β π
β (0[,]+β)) |
11 | 6, 10 | sselid 3981 |
. . . . . 6
β’ (π β π
β
β*) |
12 | | xrltnle 11281 |
. . . . . 6
β’
(((absβπ)
β β* β§ π
β β*) β
((absβπ) < π
β Β¬ π
β€ (absβπ))) |
13 | 5, 11, 12 | syl2anc 585 |
. . . . 5
β’ (π β ((absβπ) < π
β Β¬ π
β€ (absβπ))) |
14 | 1, 13 | mpbid 231 |
. . . 4
β’ (π β Β¬ π
β€ (absβπ)) |
15 | 9 | breq1i 5156 |
. . . . . 6
β’ (π
β€ (absβπ) β sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) β€ (absβπ)) |
16 | | ssrab2 4078 |
. . . . . . . 8
β’ {π β β β£ seq0( +
, (πΊβπ)) β dom β } β
β |
17 | 16, 2 | sstri 3992 |
. . . . . . 7
β’ {π β β β£ seq0( +
, (πΊβπ)) β dom β } β
β* |
18 | | supxrleub 13305 |
. . . . . . 7
β’ (({π β β β£ seq0( +
, (πΊβπ)) β dom β } β
β* β§ (absβπ) β β*) β
(sup({π β β
β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) β€ (absβπ)
β βπ β
{π β β β£
seq0( + , (πΊβπ)) β dom β }π β€ (absβπ))) |
19 | 17, 5, 18 | sylancr 588 |
. . . . . 6
β’ (π β (sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) β€ (absβπ)
β βπ β
{π β β β£
seq0( + , (πΊβπ)) β dom β }π β€ (absβπ))) |
20 | 15, 19 | bitrid 283 |
. . . . 5
β’ (π β (π
β€ (absβπ) β βπ β {π β β β£ seq0( + , (πΊβπ)) β dom β }π β€ (absβπ))) |
21 | | fveq2 6892 |
. . . . . . . 8
β’ (π = π β (πΊβπ) = (πΊβπ )) |
22 | 21 | seqeq3d 13974 |
. . . . . . 7
β’ (π = π β seq0( + , (πΊβπ)) = seq0( + , (πΊβπ ))) |
23 | 22 | eleq1d 2819 |
. . . . . 6
β’ (π = π β (seq0( + , (πΊβπ)) β dom β β seq0( + , (πΊβπ )) β dom β )) |
24 | 23 | ralrab 3690 |
. . . . 5
β’
(βπ β
{π β β β£
seq0( + , (πΊβπ)) β dom β }π β€ (absβπ) β βπ β β (seq0( + ,
(πΊβπ )) β dom β β π β€ (absβπ))) |
25 | 20, 24 | bitrdi 287 |
. . . 4
β’ (π β (π
β€ (absβπ) β βπ β β (seq0( + , (πΊβπ )) β dom β β π β€ (absβπ)))) |
26 | 14, 25 | mtbid 324 |
. . 3
β’ (π β Β¬ βπ β β (seq0( + ,
(πΊβπ )) β dom β β π β€ (absβπ))) |
27 | | rexanali 3103 |
. . 3
β’
(βπ β
β (seq0( + , (πΊβπ )) β dom β β§ Β¬ π β€ (absβπ)) β Β¬ βπ β β (seq0( + ,
(πΊβπ )) β dom β β π β€ (absβπ))) |
28 | 26, 27 | sylibr 233 |
. 2
β’ (π β βπ β β (seq0( + , (πΊβπ )) β dom β β§ Β¬ π β€ (absβπ))) |
29 | | ltnle 11293 |
. . . . . . 7
β’
(((absβπ)
β β β§ π
β β) β ((absβπ) < π β Β¬ π β€ (absβπ))) |
30 | 4, 29 | sylan 581 |
. . . . . 6
β’ ((π β§ π β β) β ((absβπ) < π β Β¬ π β€ (absβπ))) |
31 | 30 | adantr 482 |
. . . . 5
β’ (((π β§ π β β) β§ seq0( + , (πΊβπ )) β dom β ) β
((absβπ) < π β Β¬ π β€ (absβπ))) |
32 | 8 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β π΄:β0βΆβ) |
33 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β π β β) |
34 | | simplr 768 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β π β β) |
35 | 34 | recnd 11242 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β π β β) |
36 | | simprr 772 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β (absβπ) < π ) |
37 | | 0red 11217 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β 0 β β) |
38 | 33 | abscld 15383 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β (absβπ) β β) |
39 | 33 | absge0d 15391 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β 0 β€ (absβπ)) |
40 | 37, 38, 34, 39, 36 | lelttrd 11372 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β 0 < π ) |
41 | 37, 34, 40 | ltled 11362 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β 0 β€ π ) |
42 | 34, 41 | absidd 15369 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β (absβπ ) = π ) |
43 | 36, 42 | breqtrrd 5177 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β (absβπ) < (absβπ )) |
44 | | simprl 770 |
. . . . . . . 8
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β seq0( + , (πΊβπ )) β dom β ) |
45 | | radcnvlt1.h |
. . . . . . . 8
β’ π» = (π β β0 β¦ (π Β· (absβ((πΊβπ)βπ)))) |
46 | 7, 32, 33, 35, 43, 44, 45 | radcnvlem1 25925 |
. . . . . . 7
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β seq0( + , π») β dom β ) |
47 | 7, 32, 33, 35, 43, 44 | radcnvlem2 25926 |
. . . . . . 7
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β seq0( + , (abs β (πΊβπ))) β dom β ) |
48 | 46, 47 | jca 513 |
. . . . . 6
β’ (((π β§ π β β) β§ (seq0( + , (πΊβπ )) β dom β β§ (absβπ) < π )) β (seq0( + , π») β dom β β§ seq0( + , (abs
β (πΊβπ))) β dom β
)) |
49 | 48 | expr 458 |
. . . . 5
β’ (((π β§ π β β) β§ seq0( + , (πΊβπ )) β dom β ) β
((absβπ) < π β (seq0( + , π») β dom β β§ seq0(
+ , (abs β (πΊβπ))) β dom β ))) |
50 | 31, 49 | sylbird 260 |
. . . 4
β’ (((π β§ π β β) β§ seq0( + , (πΊβπ )) β dom β ) β (Β¬ π β€ (absβπ) β (seq0( + , π») β dom β β§ seq0(
+ , (abs β (πΊβπ))) β dom β ))) |
51 | 50 | expimpd 455 |
. . 3
β’ ((π β§ π β β) β ((seq0( + , (πΊβπ )) β dom β β§ Β¬ π β€ (absβπ)) β (seq0( + , π») β dom β β§ seq0(
+ , (abs β (πΊβπ))) β dom β ))) |
52 | 51 | rexlimdva 3156 |
. 2
β’ (π β (βπ β β (seq0( + , (πΊβπ )) β dom β β§ Β¬ π β€ (absβπ)) β (seq0( + , π») β dom β β§ seq0(
+ , (abs β (πΊβπ))) β dom β ))) |
53 | 28, 52 | mpd 15 |
1
β’ (π β (seq0( + , π») β dom β β§ seq0(
+ , (abs β (πΊβπ))) β dom β )) |