Step | Hyp | Ref
| Expression |
1 | | caurcvgr.2 |
. . . . . . 7
β’ (π β πΉ:π΄βΆβ) |
2 | | caurcvgr.1 |
. . . . . . . 8
β’ (π β π΄ β β) |
3 | | reex 11147 |
. . . . . . . . 9
β’ β
β V |
4 | 3 | ssex 5279 |
. . . . . . . 8
β’ (π΄ β β β π΄ β V) |
5 | 2, 4 | syl 17 |
. . . . . . 7
β’ (π β π΄ β V) |
6 | 3 | a1i 11 |
. . . . . . 7
β’ (π β β β
V) |
7 | | fex2 7871 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β V β§ β β V) β
πΉ β
V) |
8 | 1, 5, 6, 7 | syl3anc 1372 |
. . . . . 6
β’ (π β πΉ β V) |
9 | | limsupcl 15361 |
. . . . . 6
β’ (πΉ β V β (lim
supβπΉ) β
β*) |
10 | 8, 9 | syl 17 |
. . . . 5
β’ (π β (lim supβπΉ) β
β*) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β (lim supβπΉ) β
β*) |
12 | 1 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β πΉ:π΄βΆβ) |
13 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β π β π΄) |
14 | 12, 13 | ffvelcdmd 7037 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β (πΉβπ) β β) |
15 | | caucvgrlem.4 |
. . . . . . 7
β’ (π β π
β
β+) |
16 | 15 | rpred 12962 |
. . . . . 6
β’ (π β π
β β) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β π
β β) |
18 | 14, 17 | readdcld 11189 |
. . . 4
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β ((πΉβπ) + π
) β β) |
19 | | mnfxr 11217 |
. . . . . 6
β’ -β
β β* |
20 | 19 | a1i 11 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β -β β
β*) |
21 | 14, 17 | resubcld 11588 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β ((πΉβπ) β π
) β β) |
22 | 21 | rexrd 11210 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β ((πΉβπ) β π
) β
β*) |
23 | 21 | mnfltd 13050 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β -β < ((πΉβπ) β π
)) |
24 | 2 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β π΄ β β) |
25 | | ressxr 11204 |
. . . . . . . 8
β’ β
β β* |
26 | | fss 6686 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ β β
β*) β πΉ:π΄βΆβ*) |
27 | 1, 25, 26 | sylancl 587 |
. . . . . . 7
β’ (π β πΉ:π΄βΆβ*) |
28 | 27 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β πΉ:π΄βΆβ*) |
29 | | caurcvgr.3 |
. . . . . . 7
β’ (π β sup(π΄, β*, < ) =
+β) |
30 | 29 | adantr 482 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β sup(π΄, β*, < ) =
+β) |
31 | 24, 13 | sseldd 3946 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β π β β) |
32 | | simprr 772 |
. . . . . . . . 9
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
)) |
33 | | breq2 5110 |
. . . . . . . . . . 11
β’ (π = π β (π β€ π β π β€ π)) |
34 | 33 | imbrov2fvoveq 7383 |
. . . . . . . . . 10
β’ (π = π β ((π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
) β (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) |
35 | 34 | cbvralvw 3224 |
. . . . . . . . 9
β’
(βπ β
π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
)) |
36 | 32, 35 | sylib 217 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
)) |
37 | 12 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β (πΉβπ) β β) |
38 | 14 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β (πΉβπ) β β) |
39 | 37, 38 | resubcld 11588 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β ((πΉβπ) β (πΉβπ)) β β) |
40 | 39 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β ((πΉβπ) β (πΉβπ)) β β) |
41 | 40 | abscld 15327 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β (absβ((πΉβπ) β (πΉβπ))) β β) |
42 | 17 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β π
β β) |
43 | | ltle 11248 |
. . . . . . . . . . . . 13
β’
(((absβ((πΉβπ) β (πΉβπ))) β β β§ π
β β) β ((absβ((πΉβπ) β (πΉβπ))) < π
β (absβ((πΉβπ) β (πΉβπ))) β€ π
)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β ((absβ((πΉβπ) β (πΉβπ))) < π
β (absβ((πΉβπ) β (πΉβπ))) β€ π
)) |
45 | 37, 38, 42 | absdifled 15325 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β ((absβ((πΉβπ) β (πΉβπ))) β€ π
β (((πΉβπ) β π
) β€ (πΉβπ) β§ (πΉβπ) β€ ((πΉβπ) + π
)))) |
46 | 44, 45 | sylibd 238 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β ((absβ((πΉβπ) β (πΉβπ))) < π
β (((πΉβπ) β π
) β€ (πΉβπ) β§ (πΉβπ) β€ ((πΉβπ) + π
)))) |
47 | | simpl 484 |
. . . . . . . . . . 11
β’ ((((πΉβπ) β π
) β€ (πΉβπ) β§ (πΉβπ) β€ ((πΉβπ) + π
)) β ((πΉβπ) β π
) β€ (πΉβπ)) |
48 | 46, 47 | syl6 35 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β ((absβ((πΉβπ) β (πΉβπ))) < π
β ((πΉβπ) β π
) β€ (πΉβπ))) |
49 | 48 | imim2d 57 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β ((π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
) β (π β€ π β ((πΉβπ) β π
) β€ (πΉβπ)))) |
50 | 49 | ralimdva 3161 |
. . . . . . . 8
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β (βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
) β βπ β π΄ (π β€ π β ((πΉβπ) β π
) β€ (πΉβπ)))) |
51 | 36, 50 | mpd 15 |
. . . . . . 7
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β π΄ (π β€ π β ((πΉβπ) β π
) β€ (πΉβπ))) |
52 | | breq1 5109 |
. . . . . . . 8
β’ (π = π β (π β€ π β π β€ π)) |
53 | 52 | rspceaimv 3584 |
. . . . . . 7
β’ ((π β β β§
βπ β π΄ (π β€ π β ((πΉβπ) β π
) β€ (πΉβπ))) β βπ β β βπ β π΄ (π β€ π β ((πΉβπ) β π
) β€ (πΉβπ))) |
54 | 31, 51, 53 | syl2anc 585 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β β βπ β π΄ (π β€ π β ((πΉβπ) β π
) β€ (πΉβπ))) |
55 | 24, 28, 22, 30, 54 | limsupbnd2 15371 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β ((πΉβπ) β π
) β€ (lim supβπΉ)) |
56 | 20, 22, 11, 23, 55 | xrltletrd 13086 |
. . . 4
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β -β < (lim
supβπΉ)) |
57 | 18 | rexrd 11210 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β ((πΉβπ) + π
) β
β*) |
58 | 41 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((πΉβπ) β (πΉβπ))) β β) |
59 | 17 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β π
β β) |
60 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β π β€ π) |
61 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
)) |
62 | | simprl 770 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β π β π΄) |
63 | 34, 61, 62 | rspcdva 3581 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
)) |
64 | 60, 63 | mpd 15 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((πΉβπ) β (πΉβπ))) < π
) |
65 | 58, 59, 64 | ltled 11308 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((πΉβπ) β (πΉβπ))) β€ π
) |
66 | 37 | adantrr 716 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (πΉβπ) β β) |
67 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (πΉβπ) β β) |
68 | 66, 67, 59 | absdifled 15325 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((absβ((πΉβπ) β (πΉβπ))) β€ π
β (((πΉβπ) β π
) β€ (πΉβπ) β§ (πΉβπ) β€ ((πΉβπ) + π
)))) |
69 | 65, 68 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (((πΉβπ) β π
) β€ (πΉβπ) β§ (πΉβπ) β€ ((πΉβπ) + π
))) |
70 | 69 | simprd 497 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (πΉβπ) β€ ((πΉβπ) + π
)) |
71 | 70 | expr 458 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β (π β€ π β (πΉβπ) β€ ((πΉβπ) + π
))) |
72 | 71 | ralrimiva 3140 |
. . . . . 6
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β π΄ (π β€ π β (πΉβπ) β€ ((πΉβπ) + π
))) |
73 | 52 | rspceaimv 3584 |
. . . . . 6
β’ ((π β β β§
βπ β π΄ (π β€ π β (πΉβπ) β€ ((πΉβπ) + π
))) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ ((πΉβπ) + π
))) |
74 | 31, 72, 73 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β β βπ β π΄ (π β€ π β (πΉβπ) β€ ((πΉβπ) + π
))) |
75 | 24, 28, 57, 74 | limsupbnd1 15370 |
. . . 4
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β (lim supβπΉ) β€ ((πΉβπ) + π
)) |
76 | | xrre 13094 |
. . . 4
β’ ((((lim
supβπΉ) β
β* β§ ((πΉβπ) + π
) β β) β§ (-β < (lim
supβπΉ) β§ (lim
supβπΉ) β€ ((πΉβπ) + π
))) β (lim supβπΉ) β β) |
77 | 11, 18, 56, 75, 76 | syl22anc 838 |
. . 3
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β (lim supβπΉ) β β) |
78 | 77 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (lim supβπΉ) β β) |
79 | 66, 78 | resubcld 11588 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β (lim supβπΉ)) β β) |
80 | 79 | recnd 11188 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β (lim supβπΉ)) β β) |
81 | 80 | abscld 15327 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((πΉβπ) β (lim supβπΉ))) β β) |
82 | | 2re 12232 |
. . . . . . . 8
β’ 2 β
β |
83 | | remulcl 11141 |
. . . . . . . 8
β’ ((2
β β β§ π
β β) β (2 Β· π
) β β) |
84 | 82, 59, 83 | sylancr 588 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (2 Β· π
) β β) |
85 | | 3re 12238 |
. . . . . . . 8
β’ 3 β
β |
86 | | remulcl 11141 |
. . . . . . . 8
β’ ((3
β β β§ π
β β) β (3 Β· π
) β β) |
87 | 85, 59, 86 | sylancr 588 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (3 Β· π
) β β) |
88 | 66 | recnd 11188 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (πΉβπ) β β) |
89 | 78 | recnd 11188 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (lim supβπΉ) β β) |
90 | 88, 89 | abssubd 15344 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((πΉβπ) β (lim supβπΉ))) = (absβ((lim supβπΉ) β (πΉβπ)))) |
91 | 66, 84 | resubcld 11588 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β (2 Β· π
)) β β) |
92 | 21 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β π
) β β) |
93 | 59 | recnd 11188 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β π
β β) |
94 | 93 | 2timesd 12401 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (2 Β· π
) = (π
+ π
)) |
95 | 94 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β (2 Β· π
)) = ((πΉβπ) β (π
+ π
))) |
96 | 88, 93, 93 | subsub4d 11548 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (((πΉβπ) β π
) β π
) = ((πΉβπ) β (π
+ π
))) |
97 | 95, 96 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β (2 Β· π
)) = (((πΉβπ) β π
) β π
)) |
98 | 66, 59 | resubcld 11588 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β π
) β β) |
99 | 66, 59, 67 | lesubaddd 11757 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (((πΉβπ) β π
) β€ (πΉβπ) β (πΉβπ) β€ ((πΉβπ) + π
))) |
100 | 70, 99 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β π
) β€ (πΉβπ)) |
101 | 98, 67, 59, 100 | lesub1dd 11776 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (((πΉβπ) β π
) β π
) β€ ((πΉβπ) β π
)) |
102 | 97, 101 | eqbrtrd 5128 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β (2 Β· π
)) β€ ((πΉβπ) β π
)) |
103 | 55 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β π
) β€ (lim supβπΉ)) |
104 | 91, 92, 78, 102, 103 | letrd 11317 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β (2 Β· π
)) β€ (lim supβπΉ)) |
105 | 18 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) + π
) β β) |
106 | 66, 84 | readdcld 11189 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) + (2 Β· π
)) β β) |
107 | 75 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (lim supβπΉ) β€ ((πΉβπ) + π
)) |
108 | 66, 59 | readdcld 11189 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) + π
) β β) |
109 | 69, 47 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) β π
) β€ (πΉβπ)) |
110 | 67, 59, 66 | lesubaddd 11757 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (((πΉβπ) β π
) β€ (πΉβπ) β (πΉβπ) β€ ((πΉβπ) + π
))) |
111 | 109, 110 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (πΉβπ) β€ ((πΉβπ) + π
)) |
112 | 67, 108, 59, 111 | leadd1dd 11774 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) + π
) β€ (((πΉβπ) + π
) + π
)) |
113 | 88, 93, 93 | addassd 11182 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (((πΉβπ) + π
) + π
) = ((πΉβπ) + (π
+ π
))) |
114 | 94 | oveq2d 7374 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) + (2 Β· π
)) = ((πΉβπ) + (π
+ π
))) |
115 | 113, 114 | eqtr4d 2776 |
. . . . . . . . . . 11
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (((πΉβπ) + π
) + π
) = ((πΉβπ) + (2 Β· π
))) |
116 | 112, 115 | breqtrd 5132 |
. . . . . . . . . 10
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((πΉβπ) + π
) β€ ((πΉβπ) + (2 Β· π
))) |
117 | 78, 105, 106, 107, 116 | letrd 11317 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (lim supβπΉ) β€ ((πΉβπ) + (2 Β· π
))) |
118 | 78, 66, 84 | absdifled 15325 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β ((absβ((lim supβπΉ) β (πΉβπ))) β€ (2 Β· π
) β (((πΉβπ) β (2 Β· π
)) β€ (lim supβπΉ) β§ (lim supβπΉ) β€ ((πΉβπ) + (2 Β· π
))))) |
119 | 104, 117,
118 | mpbir2and 712 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((lim supβπΉ) β (πΉβπ))) β€ (2 Β· π
)) |
120 | 90, 119 | eqbrtrd 5128 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((πΉβπ) β (lim supβπΉ))) β€ (2 Β· π
)) |
121 | | 2lt3 12330 |
. . . . . . . 8
β’ 2 <
3 |
122 | 82 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β 2 β β) |
123 | 85 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β 3 β β) |
124 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β π
β
β+) |
125 | 124 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β π
β
β+) |
126 | 122, 123,
125 | ltmul1d 13003 |
. . . . . . . 8
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (2 < 3 β (2 Β· π
) < (3 Β· π
))) |
127 | 121, 126 | mpbii 232 |
. . . . . . 7
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (2 Β· π
) < (3 Β· π
)) |
128 | 81, 84, 87, 120, 127 | lelttrd 11318 |
. . . . . 6
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ (π β π΄ β§ π β€ π)) β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
)) |
129 | 128 | expr 458 |
. . . . 5
β’ (((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β§ π β π΄) β (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
))) |
130 | 129 | ralrimiva 3140 |
. . . 4
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
))) |
131 | 33 | imbrov2fvoveq 7383 |
. . . . 5
β’ (π = π β ((π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
)) β (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
)))) |
132 | 131 | cbvralvw 3224 |
. . . 4
β’
(βπ β
π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
)) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
))) |
133 | 130, 132 | sylibr 233 |
. . 3
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
))) |
134 | 77, 133 | jca 513 |
. 2
β’ ((π β§ (π β π΄ β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) β ((lim supβπΉ) β β β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
)))) |
135 | | breq2 5110 |
. . . . 5
β’ (π₯ = π
β ((absβ((πΉβπ) β (πΉβπ))) < π₯ β (absβ((πΉβπ) β (πΉβπ))) < π
)) |
136 | 135 | imbi2d 341 |
. . . 4
β’ (π₯ = π
β ((π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯) β (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) |
137 | 136 | rexralbidv 3211 |
. . 3
β’ (π₯ = π
β (βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
))) |
138 | | caurcvgr.4 |
. . 3
β’ (π β βπ₯ β β+ βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
139 | 137, 138,
15 | rspcdva 3581 |
. 2
β’ (π β βπ β π΄ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (πΉβπ))) < π
)) |
140 | 134, 139 | reximddv 3165 |
1
β’ (π β βπ β π΄ ((lim supβπΉ) β β β§ βπ β π΄ (π β€ π β (absβ((πΉβπ) β (lim supβπΉ))) < (3 Β· π
)))) |