Step | Hyp | Ref
| Expression |
1 | | psercn.m |
. . . 4
β’ π = if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)) |
2 | | psercn.s |
. . . . . . . . . . 11
β’ π = (β‘abs β (0[,)π
)) |
3 | | cnvimass 6037 |
. . . . . . . . . . . 12
β’ (β‘abs β (0[,)π
)) β dom abs |
4 | | absf 15231 |
. . . . . . . . . . . . 13
β’
abs:ββΆβ |
5 | 4 | fdmi 6684 |
. . . . . . . . . . . 12
β’ dom abs =
β |
6 | 3, 5 | sseqtri 3984 |
. . . . . . . . . . 11
β’ (β‘abs β (0[,)π
)) β β |
7 | 2, 6 | eqsstri 3982 |
. . . . . . . . . 10
β’ π β
β |
8 | 7 | a1i 11 |
. . . . . . . . 9
β’ (π β π β β) |
9 | 8 | sselda 3948 |
. . . . . . . 8
β’ ((π β§ π β π) β π β β) |
10 | 9 | abscld 15330 |
. . . . . . 7
β’ ((π β§ π β π) β (absβπ) β β) |
11 | | readdcl 11142 |
. . . . . . 7
β’
(((absβπ)
β β β§ π
β β) β ((absβπ) + π
) β β) |
12 | 10, 11 | sylan 581 |
. . . . . 6
β’ (((π β§ π β π) β§ π
β β) β ((absβπ) + π
) β β) |
13 | 12 | rehalfcld 12408 |
. . . . 5
β’ (((π β§ π β π) β§ π
β β) β (((absβπ) + π
) / 2) β β) |
14 | | peano2re 11336 |
. . . . . . 7
β’
((absβπ)
β β β ((absβπ) + 1) β β) |
15 | 10, 14 | syl 17 |
. . . . . 6
β’ ((π β§ π β π) β ((absβπ) + 1) β β) |
16 | 15 | adantr 482 |
. . . . 5
β’ (((π β§ π β π) β§ Β¬ π
β β) β ((absβπ) + 1) β
β) |
17 | 13, 16 | ifclda 4525 |
. . . 4
β’ ((π β§ π β π) β if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)) β β) |
18 | 1, 17 | eqeltrid 2838 |
. . 3
β’ ((π β§ π β π) β π β β) |
19 | | 0re 11165 |
. . . . 5
β’ 0 β
β |
20 | 19 | a1i 11 |
. . . 4
β’ ((π β§ π β π) β 0 β β) |
21 | 9 | absge0d 15338 |
. . . 4
β’ ((π β§ π β π) β 0 β€ (absβπ)) |
22 | | breq2 5113 |
. . . . . 6
β’
((((absβπ) +
π
) / 2) = if(π
β β,
(((absβπ) + π
) / 2), ((absβπ) + 1)) β ((absβπ) < (((absβπ) + π
) / 2) β (absβπ) < if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)))) |
23 | | breq2 5113 |
. . . . . 6
β’
(((absβπ) + 1)
= if(π
β β,
(((absβπ) + π
) / 2), ((absβπ) + 1)) β ((absβπ) < ((absβπ) + 1) β (absβπ) < if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)))) |
24 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β π) |
25 | 24, 2 | eleqtrdi 2844 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π β (β‘abs β (0[,)π
))) |
26 | | ffn 6672 |
. . . . . . . . . . . . 13
β’
(abs:ββΆβ β abs Fn β) |
27 | | elpreima 7012 |
. . . . . . . . . . . . 13
β’ (abs Fn
β β (π β
(β‘abs β (0[,)π
)) β (π β β β§ (absβπ) β (0[,)π
)))) |
28 | 4, 26, 27 | mp2b 10 |
. . . . . . . . . . . 12
β’ (π β (β‘abs β (0[,)π
)) β (π β β β§ (absβπ) β (0[,)π
))) |
29 | 25, 28 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π β β β§ (absβπ) β (0[,)π
))) |
30 | 29 | simprd 497 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (absβπ) β (0[,)π
)) |
31 | | iccssxr 13356 |
. . . . . . . . . . . 12
β’
(0[,]+β) β β* |
32 | | pserf.g |
. . . . . . . . . . . . . 14
β’ πΊ = (π₯ β β β¦ (π β β0 β¦ ((π΄βπ) Β· (π₯βπ)))) |
33 | | pserf.a |
. . . . . . . . . . . . . 14
β’ (π β π΄:β0βΆβ) |
34 | | pserf.r |
. . . . . . . . . . . . . 14
β’ π
= sup({π β β β£ seq0( + , (πΊβπ)) β dom β }, β*,
< ) |
35 | 32, 33, 34 | radcnvcl 25799 |
. . . . . . . . . . . . 13
β’ (π β π
β (0[,]+β)) |
36 | 35 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β π
β (0[,]+β)) |
37 | 31, 36 | sselid 3946 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π
β
β*) |
38 | | elico2 13337 |
. . . . . . . . . . 11
β’ ((0
β β β§ π
β β*) β ((absβπ) β (0[,)π
) β ((absβπ) β β β§ 0 β€
(absβπ) β§
(absβπ) < π
))) |
39 | 19, 37, 38 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((absβπ) β (0[,)π
) β ((absβπ) β β β§ 0 β€
(absβπ) β§
(absβπ) < π
))) |
40 | 30, 39 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((absβπ) β β β§ 0 β€
(absβπ) β§
(absβπ) < π
)) |
41 | 40 | simp3d 1145 |
. . . . . . . 8
β’ ((π β§ π β π) β (absβπ) < π
) |
42 | 41 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β π) β§ π
β β) β (absβπ) < π
) |
43 | | avglt1 12399 |
. . . . . . . 8
β’
(((absβπ)
β β β§ π
β β) β ((absβπ) < π
β (absβπ) < (((absβπ) + π
) / 2))) |
44 | 10, 43 | sylan 581 |
. . . . . . 7
β’ (((π β§ π β π) β§ π
β β) β ((absβπ) < π
β (absβπ) < (((absβπ) + π
) / 2))) |
45 | 42, 44 | mpbid 231 |
. . . . . 6
β’ (((π β§ π β π) β§ π
β β) β (absβπ) < (((absβπ) + π
) / 2)) |
46 | 10 | ltp1d 12093 |
. . . . . . 7
β’ ((π β§ π β π) β (absβπ) < ((absβπ) + 1)) |
47 | 46 | adantr 482 |
. . . . . 6
β’ (((π β§ π β π) β§ Β¬ π
β β) β (absβπ) < ((absβπ) + 1)) |
48 | 22, 23, 45, 47 | ifbothda 4528 |
. . . . 5
β’ ((π β§ π β π) β (absβπ) < if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1))) |
49 | 48, 1 | breqtrrdi 5151 |
. . . 4
β’ ((π β§ π β π) β (absβπ) < π) |
50 | 20, 10, 18, 21, 49 | lelttrd 11321 |
. . 3
β’ ((π β§ π β π) β 0 < π) |
51 | 18, 50 | elrpd 12962 |
. 2
β’ ((π β§ π β π) β π β
β+) |
52 | | breq1 5112 |
. . . 4
β’
((((absβπ) +
π
) / 2) = if(π
β β,
(((absβπ) + π
) / 2), ((absβπ) + 1)) β
((((absβπ) + π
) / 2) < π
β if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)) < π
)) |
53 | | breq1 5112 |
. . . 4
β’
(((absβπ) + 1)
= if(π
β β,
(((absβπ) + π
) / 2), ((absβπ) + 1)) β
(((absβπ) + 1) <
π
β if(π
β β,
(((absβπ) + π
) / 2), ((absβπ) + 1)) < π
)) |
54 | | avglt2 12400 |
. . . . . 6
β’
(((absβπ)
β β β§ π
β β) β ((absβπ) < π
β (((absβπ) + π
) / 2) < π
)) |
55 | 10, 54 | sylan 581 |
. . . . 5
β’ (((π β§ π β π) β§ π
β β) β ((absβπ) < π
β (((absβπ) + π
) / 2) < π
)) |
56 | 42, 55 | mpbid 231 |
. . . 4
β’ (((π β§ π β π) β§ π
β β) β (((absβπ) + π
) / 2) < π
) |
57 | 15 | rexrd 11213 |
. . . . . . . 8
β’ ((π β§ π β π) β ((absβπ) + 1) β
β*) |
58 | 37, 57 | xrlenltd 11229 |
. . . . . . 7
β’ ((π β§ π β π) β (π
β€ ((absβπ) + 1) β Β¬ ((absβπ) + 1) < π
)) |
59 | | 0xr 11210 |
. . . . . . . . . . . . 13
β’ 0 β
β* |
60 | | pnfxr 11217 |
. . . . . . . . . . . . 13
β’ +β
β β* |
61 | | elicc1 13317 |
. . . . . . . . . . . . 13
β’ ((0
β β* β§ +β β β*) β
(π
β (0[,]+β)
β (π
β
β* β§ 0 β€ π
β§ π
β€ +β))) |
62 | 59, 60, 61 | mp2an 691 |
. . . . . . . . . . . 12
β’ (π
β (0[,]+β) β
(π
β
β* β§ 0 β€ π
β§ π
β€ +β)) |
63 | 35, 62 | sylib 217 |
. . . . . . . . . . 11
β’ (π β (π
β β* β§ 0 β€
π
β§ π
β€ +β)) |
64 | 63 | simp2d 1144 |
. . . . . . . . . 10
β’ (π β 0 β€ π
) |
65 | 64 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β 0 β€ π
) |
66 | | ge0gtmnf 13100 |
. . . . . . . . 9
β’ ((π
β β*
β§ 0 β€ π
) β
-β < π
) |
67 | 37, 65, 66 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β π) β -β < π
) |
68 | | xrre 13097 |
. . . . . . . . 9
β’ (((π
β β*
β§ ((absβπ) + 1)
β β) β§ (-β < π
β§ π
β€ ((absβπ) + 1))) β π
β β) |
69 | 68 | expr 458 |
. . . . . . . 8
β’ (((π
β β*
β§ ((absβπ) + 1)
β β) β§ -β < π
) β (π
β€ ((absβπ) + 1) β π
β β)) |
70 | 37, 15, 67, 69 | syl21anc 837 |
. . . . . . 7
β’ ((π β§ π β π) β (π
β€ ((absβπ) + 1) β π
β β)) |
71 | 58, 70 | sylbird 260 |
. . . . . 6
β’ ((π β§ π β π) β (Β¬ ((absβπ) + 1) < π
β π
β β)) |
72 | 71 | con1d 145 |
. . . . 5
β’ ((π β§ π β π) β (Β¬ π
β β β ((absβπ) + 1) < π
)) |
73 | 72 | imp 408 |
. . . 4
β’ (((π β§ π β π) β§ Β¬ π
β β) β ((absβπ) + 1) < π
) |
74 | 52, 53, 56, 73 | ifbothda 4528 |
. . 3
β’ ((π β§ π β π) β if(π
β β, (((absβπ) + π
) / 2), ((absβπ) + 1)) < π
) |
75 | 1, 74 | eqbrtrid 5144 |
. 2
β’ ((π β§ π β π) β π < π
) |
76 | 51, 49, 75 | 3jca 1129 |
1
β’ ((π β§ π β π) β (π β β+ β§
(absβπ) < π β§ π < π
)) |