Step | Hyp | Ref
| Expression |
1 | | ressxr 11206 |
. . 3
β’ β
β β* |
2 | | radcnvle.x |
. . . 4
β’ (π β π β β) |
3 | 2 | abscld 15328 |
. . 3
β’ (π β (absβπ) β
β) |
4 | 1, 3 | sselid 3947 |
. 2
β’ (π β (absβπ) β
β*) |
5 | | iccssxr 13354 |
. . 3
β’
(0[,]+β) β β* |
6 | | pser.g |
. . . 4
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
7 | | radcnv.a |
. . . 4
β’ (π β π΄:β0βΆβ) |
8 | | radcnv.r |
. . . 4
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
9 | 6, 7, 8 | radcnvcl 25792 |
. . 3
β’ (π β π
β (0[,]+β)) |
10 | 5, 9 | sselid 3947 |
. 2
β’ (π β π
β
β*) |
11 | | simpr 486 |
. . . 4
β’ ((π β§ π
< (absβπ)) β π
< (absβπ)) |
12 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ π
< (absβπ)) β π
β
β*) |
13 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π
< (absβπ)) β (absβπ) β β) |
14 | | 0xr 11209 |
. . . . . . . . . . 11
β’ 0 β
β* |
15 | | pnfxr 11216 |
. . . . . . . . . . 11
β’ +β
β β* |
16 | | elicc1 13315 |
. . . . . . . . . . 11
β’ ((0
β β* β§ +β β β*) β
(π
β (0[,]+β)
β (π
β
β* β§ 0 β€ π
β§ π
β€ +β))) |
17 | 14, 15, 16 | mp2an 691 |
. . . . . . . . . 10
β’ (π
β (0[,]+β) β
(π
β
β* β§ 0 β€ π
β§ π
β€ +β)) |
18 | 9, 17 | sylib 217 |
. . . . . . . . 9
β’ (π β (π
β β* β§ 0 β€
π
β§ π
β€ +β)) |
19 | 18 | simp2d 1144 |
. . . . . . . 8
β’ (π β 0 β€ π
) |
20 | | ge0gtmnf 13098 |
. . . . . . . 8
β’ ((π
β β*
β§ 0 β€ π
) β
-β < π
) |
21 | 10, 19, 20 | syl2anc 585 |
. . . . . . 7
β’ (π β -β < π
) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ π
< (absβπ)) β -β < π
) |
23 | 4 | adantr 482 |
. . . . . . 7
β’ ((π β§ π
< (absβπ)) β (absβπ) β
β*) |
24 | 12, 23, 11 | xrltled 13076 |
. . . . . 6
β’ ((π β§ π
< (absβπ)) β π
β€ (absβπ)) |
25 | | xrre 13095 |
. . . . . 6
β’ (((π
β β*
β§ (absβπ) β
β) β§ (-β < π
β§ π
β€ (absβπ))) β π
β β) |
26 | 12, 13, 22, 24, 25 | syl22anc 838 |
. . . . 5
β’ ((π β§ π
< (absβπ)) β π
β β) |
27 | | avglt1 12398 |
. . . . 5
β’ ((π
β β β§
(absβπ) β
β) β (π
<
(absβπ) β π
< ((π
+ (absβπ)) / 2))) |
28 | 26, 13, 27 | syl2anc 585 |
. . . 4
β’ ((π β§ π
< (absβπ)) β (π
< (absβπ) β π
< ((π
+ (absβπ)) / 2))) |
29 | 11, 28 | mpbid 231 |
. . 3
β’ ((π β§ π
< (absβπ)) β π
< ((π
+ (absβπ)) / 2)) |
30 | 26, 13 | readdcld 11191 |
. . . . 5
β’ ((π β§ π
< (absβπ)) β (π
+ (absβπ)) β β) |
31 | 30 | rehalfcld 12407 |
. . . 4
β’ ((π β§ π
< (absβπ)) β ((π
+ (absβπ)) / 2) β β) |
32 | | ssrab2 4042 |
. . . . . . 7
β’ {π β β β£ seq0( +
, (πΊβπ)) β dom β } β
β |
33 | 32, 1 | sstri 3958 |
. . . . . 6
β’ {π β β β£ seq0( +
, (πΊβπ)) β dom β } β
β* |
34 | 7 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π
< (absβπ)) β π΄:β0βΆβ) |
35 | 31 | recnd 11190 |
. . . . . . . 8
β’ ((π β§ π
< (absβπ)) β ((π
+ (absβπ)) / 2) β β) |
36 | 2 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π
< (absβπ)) β π β β) |
37 | | 0red 11165 |
. . . . . . . . . . 11
β’ ((π β§ π
< (absβπ)) β 0 β β) |
38 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π
< (absβπ)) β 0 β€ π
) |
39 | 37, 26, 31, 38, 29 | lelttrd 11320 |
. . . . . . . . . . 11
β’ ((π β§ π
< (absβπ)) β 0 < ((π
+ (absβπ)) / 2)) |
40 | 37, 31, 39 | ltled 11310 |
. . . . . . . . . 10
β’ ((π β§ π
< (absβπ)) β 0 β€ ((π
+ (absβπ)) / 2)) |
41 | 31, 40 | absidd 15314 |
. . . . . . . . 9
β’ ((π β§ π
< (absβπ)) β (absβ((π
+ (absβπ)) / 2)) = ((π
+ (absβπ)) / 2)) |
42 | | avglt2 12399 |
. . . . . . . . . . 11
β’ ((π
β β β§
(absβπ) β
β) β (π
<
(absβπ) β
((π
+ (absβπ)) / 2) < (absβπ))) |
43 | 26, 13, 42 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π
< (absβπ)) β (π
< (absβπ) β ((π
+ (absβπ)) / 2) < (absβπ))) |
44 | 11, 43 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π
< (absβπ)) β ((π
+ (absβπ)) / 2) < (absβπ)) |
45 | 41, 44 | eqbrtrd 5132 |
. . . . . . . 8
β’ ((π β§ π
< (absβπ)) β (absβ((π
+ (absβπ)) / 2)) < (absβπ)) |
46 | | radcnvle.a |
. . . . . . . . 9
β’ (π β seq0( + , (πΊβπ)) β dom β ) |
47 | 46 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π
< (absβπ)) β seq0( + , (πΊβπ)) β dom β ) |
48 | 6, 34, 35, 36, 45, 47 | radcnvlem3 25790 |
. . . . . . 7
β’ ((π β§ π
< (absβπ)) β seq0( + , (πΊβ((π
+ (absβπ)) / 2))) β dom β
) |
49 | | fveq2 6847 |
. . . . . . . . . 10
β’ (π¦ = ((π
+ (absβπ)) / 2) β (πΊβπ¦) = (πΊβ((π
+ (absβπ)) / 2))) |
50 | 49 | seqeq3d 13921 |
. . . . . . . . 9
β’ (π¦ = ((π
+ (absβπ)) / 2) β seq0( + , (πΊβπ¦)) = seq0( + , (πΊβ((π
+ (absβπ)) / 2)))) |
51 | 50 | eleq1d 2823 |
. . . . . . . 8
β’ (π¦ = ((π
+ (absβπ)) / 2) β (seq0( + , (πΊβπ¦)) β dom β β seq0( + , (πΊβ((π
+ (absβπ)) / 2))) β dom β
)) |
52 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π¦ β (πΊβπ) = (πΊβπ¦)) |
53 | 52 | seqeq3d 13921 |
. . . . . . . . . 10
β’ (π = π¦ β seq0( + , (πΊβπ)) = seq0( + , (πΊβπ¦))) |
54 | 53 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = π¦ β (seq0( + , (πΊβπ)) β dom β β seq0( + , (πΊβπ¦)) β dom β )) |
55 | 54 | cbvrabv 3420 |
. . . . . . . 8
β’ {π β β β£ seq0( +
, (πΊβπ)) β dom β } = {π¦ β β β£ seq0( +
, (πΊβπ¦)) β dom β
} |
56 | 51, 55 | elrab2 3653 |
. . . . . . 7
β’ (((π
+ (absβπ)) / 2) β {π β β β£ seq0( + , (πΊβπ)) β dom β } β (((π
+ (absβπ)) / 2) β β β§ seq0( + ,
(πΊβ((π
+ (absβπ)) / 2))) β dom β
)) |
57 | 31, 48, 56 | sylanbrc 584 |
. . . . . 6
β’ ((π β§ π
< (absβπ)) β ((π
+ (absβπ)) / 2) β {π β β β£ seq0( + , (πΊβπ)) β dom β }) |
58 | | supxrub 13250 |
. . . . . 6
β’ (({π β β β£ seq0( +
, (πΊβπ)) β dom β } β
β* β§ ((π
+ (absβπ)) / 2) β {π β β β£ seq0( + , (πΊβπ)) β dom β }) β ((π
+ (absβπ)) / 2) β€ sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< )) |
59 | 33, 57, 58 | sylancr 588 |
. . . . 5
β’ ((π β§ π
< (absβπ)) β ((π
+ (absβπ)) / 2) β€ sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< )) |
60 | 59, 8 | breqtrrdi 5152 |
. . . 4
β’ ((π β§ π
< (absβπ)) β ((π
+ (absβπ)) / 2) β€ π
) |
61 | 31, 26, 60 | lensymd 11313 |
. . 3
β’ ((π β§ π
< (absβπ)) β Β¬ π
< ((π
+ (absβπ)) / 2)) |
62 | 29, 61 | pm2.65da 816 |
. 2
β’ (π β Β¬ π
< (absβπ)) |
63 | 4, 10, 62 | xrnltled 11230 |
1
β’ (π β (absβπ) β€ π
) |