Step | Hyp | Ref
| Expression |
1 | | psercn.s |
. . . . . . . . 9
β’ π = (β‘abs β (0[,)π
)) |
2 | | cnvimass 6074 |
. . . . . . . . . 10
β’ (β‘abs β (0[,)π
)) β dom abs |
3 | | absf 15290 |
. . . . . . . . . . 11
β’
abs:ββΆβ |
4 | 3 | fdmi 6723 |
. . . . . . . . . 10
β’ dom abs =
β |
5 | 2, 4 | sseqtri 4013 |
. . . . . . . . 9
β’ (β‘abs β (0[,)π
)) β β |
6 | 1, 5 | eqsstri 4011 |
. . . . . . . 8
β’ π β
β |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β π β β) |
8 | 7 | sselda 3977 |
. . . . . 6
β’ ((π β§ π β π) β π β β) |
9 | 8 | abscld 15389 |
. . . . 5
β’ ((π β§ π β π) β (absβπ) β β) |
10 | | pserf.g |
. . . . . . . 8
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
11 | | pserf.f |
. . . . . . . 8
β’ πΉ = (π¦ β π β¦ Ξ£π β β0 ((πΊβπ¦)βπ)) |
12 | | pserf.a |
. . . . . . . 8
β’ (π β π΄:β0βΆβ) |
13 | | pserf.r |
. . . . . . . 8
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
14 | | psercn.m |
. . . . . . . 8
β’ π = if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)) |
15 | 10, 11, 12, 13, 1, 14 | psercnlem1 26317 |
. . . . . . 7
β’ ((π β§ π β π) β (π β β+ β§
(absβπ) < π β§ π < π
)) |
16 | 15 | simp1d 1139 |
. . . . . 6
β’ ((π β§ π β π) β π β
β+) |
17 | 16 | rpred 13022 |
. . . . 5
β’ ((π β§ π β π) β π β β) |
18 | 9, 17 | readdcld 11247 |
. . . 4
β’ ((π β§ π β π) β ((absβπ) + π) β β) |
19 | | 0red 11221 |
. . . . 5
β’ ((π β§ π β π) β 0 β β) |
20 | 8 | absge0d 15397 |
. . . . 5
β’ ((π β§ π β π) β 0 β€ (absβπ)) |
21 | 9, 16 | ltaddrpd 13055 |
. . . . 5
β’ ((π β§ π β π) β (absβπ) < ((absβπ) + π)) |
22 | 19, 9, 18, 20, 21 | lelttrd 11376 |
. . . 4
β’ ((π β§ π β π) β 0 < ((absβπ) + π)) |
23 | 18, 22 | elrpd 13019 |
. . 3
β’ ((π β§ π β π) β ((absβπ) + π) β
β+) |
24 | 23 | rphalfcld 13034 |
. 2
β’ ((π β§ π β π) β (((absβπ) + π) / 2) β
β+) |
25 | 15 | simp2d 1140 |
. . 3
β’ ((π β§ π β π) β (absβπ) < π) |
26 | | avglt1 12454 |
. . . 4
β’
(((absβπ)
β β β§ π
β β) β ((absβπ) < π β (absβπ) < (((absβπ) + π) / 2))) |
27 | 9, 17, 26 | syl2anc 583 |
. . 3
β’ ((π β§ π β π) β ((absβπ) < π β (absβπ) < (((absβπ) + π) / 2))) |
28 | 25, 27 | mpbid 231 |
. 2
β’ ((π β§ π β π) β (absβπ) < (((absβπ) + π) / 2)) |
29 | 18 | rehalfcld 12463 |
. . . 4
β’ ((π β§ π β π) β (((absβπ) + π) / 2) β β) |
30 | 29 | rexrd 11268 |
. . 3
β’ ((π β§ π β π) β (((absβπ) + π) / 2) β
β*) |
31 | 17 | rexrd 11268 |
. . 3
β’ ((π β§ π β π) β π β
β*) |
32 | | iccssxr 13413 |
. . . . 5
β’
(0[,]+β) β β* |
33 | 10, 12, 13 | radcnvcl 26308 |
. . . . 5
β’ (π β π
β (0[,]+β)) |
34 | 32, 33 | sselid 3975 |
. . . 4
β’ (π β π
β
β*) |
35 | 34 | adantr 480 |
. . 3
β’ ((π β§ π β π) β π
β
β*) |
36 | | avglt2 12455 |
. . . . 5
β’
(((absβπ)
β β β§ π
β β) β ((absβπ) < π β (((absβπ) + π) / 2) < π)) |
37 | 9, 17, 36 | syl2anc 583 |
. . . 4
β’ ((π β§ π β π) β ((absβπ) < π β (((absβπ) + π) / 2) < π)) |
38 | 25, 37 | mpbid 231 |
. . 3
β’ ((π β§ π β π) β (((absβπ) + π) / 2) < π) |
39 | 15 | simp3d 1141 |
. . 3
β’ ((π β§ π β π) β π < π
) |
40 | 30, 31, 35, 38, 39 | xrlttrd 13144 |
. 2
β’ ((π β§ π β π) β (((absβπ) + π) / 2) < π
) |
41 | 24, 28, 40 | 3jca 1125 |
1
β’ ((π β§ π β π) β ((((absβπ) + π) / 2) β β+ β§
(absβπ) <
(((absβπ) + π) / 2) β§ (((absβπ) + π) / 2) < π
)) |