Step | Hyp | Ref
| Expression |
1 | | 1rp 12924 |
. . . 4
β’ 1 β
β+ |
2 | 1 | ne0ii 4298 |
. . 3
β’
β+ β β
|
3 | | caurcvg2.3 |
. . 3
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
4 | | r19.2z 4453 |
. . 3
β’
((β+ β β
β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
5 | 2, 3, 4 | sylancr 588 |
. 2
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
6 | | simpl 484 |
. . . . . 6
β’ (((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β (πΉβπ) β β) |
7 | 6 | ralimi 3083 |
. . . . 5
β’
(βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β (β€β₯βπ)(πΉβπ) β β) |
8 | | eqid 2733 |
. . . . . . . . 9
β’
(β€β₯βπ) = (β€β₯βπ) |
9 | | simprr 772 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β βπ β
(β€β₯βπ)(πΉβπ) β β) |
10 | | fveq2 6843 |
. . . . . . . . . . . . 13
β’ (π = π β (πΉβπ) = (πΉβπ)) |
11 | 10 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
12 | 11 | rspccva 3579 |
. . . . . . . . . . 11
β’
((βπ β
(β€β₯βπ)(πΉβπ) β β β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
13 | 9, 12 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β§ π β (β€β₯βπ)) β (πΉβπ) β β) |
14 | 13 | fmpttd 7064 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β (π β (β€β₯βπ) β¦ (πΉβπ)):(β€β₯βπ)βΆβ) |
15 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
16 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πΉβπ) = (πΉβπ)) |
17 | 16 | oveq2d 7374 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ((πΉβπ) β (πΉβπ)) = ((πΉβπ) β (πΉβπ))) |
18 | 17 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (absβ((πΉβπ) β (πΉβπ))) = (absβ((πΉβπ) β (πΉβπ)))) |
19 | 18 | breq1d 5116 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ((absβ((πΉβπ) β (πΉβπ))) < π₯ β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
20 | 19 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) |
21 | 15, 20 | raleqbidv 3318 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) |
22 | 21 | cbvrexvw 3225 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
23 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (πΉβπ) = (πΉβπ)) |
24 | 23 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((πΉβπ) β β β (πΉβπ) β β)) |
25 | 23 | fvoveq1d 7380 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (absβ((πΉβπ) β (πΉβπ))) = (absβ((πΉβπ) β (πΉβπ)))) |
26 | 25 | breq1d 5116 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((absβ((πΉβπ) β (πΉβπ))) < π₯ β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
27 | 24, 26 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) |
28 | 27 | cbvralvw 3224 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
29 | | recn 11146 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) β β β (πΉβπ) β β) |
30 | 29 | anim1i 616 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β ((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
31 | 30 | ralimi 3083 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
32 | 28, 31 | sylbi 216 |
. . . . . . . . . . . . . . . 16
β’
(βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
33 | 32 | reximi 3084 |
. . . . . . . . . . . . . . 15
β’
(βπ β
π βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
34 | 22, 33 | sylbi 216 |
. . . . . . . . . . . . . 14
β’
(βπ β
π βπ β
(β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
35 | 34 | ralimi 3083 |
. . . . . . . . . . . . 13
β’
(βπ₯ β
β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
36 | 3, 35 | syl 17 |
. . . . . . . . . . . 12
β’ (π β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
37 | 36 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
38 | | caucvg.1 |
. . . . . . . . . . . . 13
β’ π =
(β€β₯βπ) |
39 | 38, 8 | cau4 15247 |
. . . . . . . . . . . 12
β’ (π β π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) |
40 | 39 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β (βπ₯ β β+
βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯))) |
41 | 37, 40 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
42 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β (absβ((πΉβπ) β (πΉβπ))) < π₯) |
43 | 8 | uztrn2 12787 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β π β (β€β₯βπ)) |
44 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΉβπ) = (πΉβπ)) |
45 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯βπ) β¦ (πΉβπ)) = (π β (β€β₯βπ) β¦ (πΉβπ)) |
46 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉβπ) β V |
47 | 44, 45, 46 | fvmpt 6949 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ) = (πΉβπ)) |
48 | 43, 47 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ) = (πΉβπ)) |
49 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (πΉβπ) = (πΉβπ)) |
50 | | fvex 6856 |
. . . . . . . . . . . . . . . . . . 19
β’ (πΉβπ) β V |
51 | 49, 45, 50 | fvmpt 6949 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ) = (πΉβπ)) |
52 | 51 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ) = (πΉβπ)) |
53 | 48, 52 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β (((π β (β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ)) = ((πΉβπ) β (πΉβπ))) |
54 | 53 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β (absβ(((π β
(β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ))) = (absβ((πΉβπ) β (πΉβπ)))) |
55 | 54 | breq1d 5116 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β ((absβ(((π β
(β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ))) < π₯ β (absβ((πΉβπ) β (πΉβπ))) < π₯)) |
56 | 42, 55 | syl5ibr 246 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯βπ) β§ π β (β€β₯βπ)) β (((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β (absβ(((π β (β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ))) < π₯)) |
57 | 56 | ralimdva 3161 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯βπ) β (βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β (β€β₯βπ)(absβ(((π β
(β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ))) < π₯)) |
58 | 57 | reximia 3081 |
. . . . . . . . . . 11
β’
(βπ β
(β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ β (β€β₯βπ)βπ β (β€β₯βπ)(absβ(((π β
(β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ))) < π₯) |
59 | 58 | ralimi 3083 |
. . . . . . . . . 10
β’
(βπ₯ β
β+ βπ β (β€β₯βπ)βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β βπ₯ β β+ βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(absβ(((π β
(β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ))) < π₯) |
60 | 41, 59 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β βπ₯ β β+
βπ β
(β€β₯βπ)βπ β (β€β₯βπ)(absβ(((π β
(β€β₯βπ) β¦ (πΉβπ))βπ) β ((π β (β€β₯βπ) β¦ (πΉβπ))βπ))) < π₯) |
61 | 8, 14, 60 | caurcvg 15567 |
. . . . . . . 8
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β (π β (β€β₯βπ) β¦ (πΉβπ)) β (lim supβ(π β (β€β₯βπ) β¦ (πΉβπ)))) |
62 | | eluzelz 12778 |
. . . . . . . . . . 11
β’ (π β
(β€β₯βπ) β π β β€) |
63 | 62, 38 | eleq2s 2852 |
. . . . . . . . . 10
β’ (π β π β π β β€) |
64 | 63 | ad2antrl 727 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β π β β€) |
65 | | caurcvg2.2 |
. . . . . . . . . 10
β’ (π β πΉ β π) |
66 | 65 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β πΉ β π) |
67 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = π β (πΉβπ) = (πΉβπ)) |
68 | 67 | cbvmptv 5219 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β¦ (πΉβπ)) = (π β (β€β₯βπ) β¦ (πΉβπ)) |
69 | 8, 68 | climmpt 15459 |
. . . . . . . . 9
β’ ((π β β€ β§ πΉ β π) β (πΉ β (lim supβ(π β (β€β₯βπ) β¦ (πΉβπ))) β (π β (β€β₯βπ) β¦ (πΉβπ)) β (lim supβ(π β (β€β₯βπ) β¦ (πΉβπ))))) |
70 | 64, 66, 69 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β (πΉ β (lim supβ(π β (β€β₯βπ) β¦ (πΉβπ))) β (π β (β€β₯βπ) β¦ (πΉβπ)) β (lim supβ(π β (β€β₯βπ) β¦ (πΉβπ))))) |
71 | 61, 70 | mpbird 257 |
. . . . . . 7
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β πΉ β (lim supβ(π β (β€β₯βπ) β¦ (πΉβπ)))) |
72 | | climrel 15380 |
. . . . . . . 8
β’ Rel
β |
73 | 72 | releldmi 5904 |
. . . . . . 7
β’ (πΉ β (lim supβ(π β
(β€β₯βπ) β¦ (πΉβπ))) β πΉ β dom β ) |
74 | 71, 73 | syl 17 |
. . . . . 6
β’ ((π β§ (π β π β§ βπ β (β€β₯βπ)(πΉβπ) β β)) β πΉ β dom β ) |
75 | 74 | expr 458 |
. . . . 5
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(πΉβπ) β β β πΉ β dom β )) |
76 | 7, 75 | syl5 34 |
. . . 4
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β πΉ β dom β )) |
77 | 76 | rexlimdva 3149 |
. . 3
β’ (π β (βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β πΉ β dom β )) |
78 | 77 | rexlimdvw 3154 |
. 2
β’ (π β (βπ₯ β β+ βπ β π βπ β (β€β₯βπ)((πΉβπ) β β β§ (absβ((πΉβπ) β (πΉβπ))) < π₯) β πΉ β dom β )) |
79 | 5, 78 | mpd 15 |
1
β’ (π β πΉ β dom β ) |