Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . 3
β’
β²ππΉ |
2 | | liminfreuz.2 |
. . 3
β’ (π β π β β€) |
3 | | liminfreuz.3 |
. . 3
β’ π =
(β€β₯βπ) |
4 | | liminfreuz.4 |
. . 3
β’ (π β πΉ:πβΆβ) |
5 | 1, 2, 3, 4 | liminfreuzlem 44129 |
. 2
β’ (π β ((lim infβπΉ) β β β
(βπ¦ β β
βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β§ βπ¦ β β βπ β π π¦ β€ (πΉβπ)))) |
6 | | breq2 5110 |
. . . . . . . 8
β’ (π¦ = π₯ β ((πΉβπ) β€ π¦ β (πΉβπ) β€ π₯)) |
7 | 6 | rexbidv 3172 |
. . . . . . 7
β’ (π¦ = π₯ β (βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
8 | 7 | ralbidv 3171 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
9 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (β€β₯βπ) =
(β€β₯βπ)) |
10 | 9 | rexeqdv 3313 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
11 | | liminfreuz.1 |
. . . . . . . . . . . . 13
β’
β²ππΉ |
12 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²ππ |
13 | 11, 12 | nffv 6853 |
. . . . . . . . . . . 12
β’
β²π(πΉβπ) |
14 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π
β€ |
15 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²ππ₯ |
16 | 13, 14, 15 | nfbr 5153 |
. . . . . . . . . . 11
β’
β²π(πΉβπ) β€ π₯ |
17 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π(πΉβπ) β€ π₯ |
18 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβπ) = (πΉβπ)) |
19 | 18 | breq1d 5116 |
. . . . . . . . . . 11
β’ (π = π β ((πΉβπ) β€ π₯ β (πΉβπ) β€ π₯)) |
20 | 16, 17, 19 | cbvrexw 3289 |
. . . . . . . . . 10
β’
(βπ β
(β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
21 | 20 | a1i 11 |
. . . . . . . . 9
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
22 | 10, 21 | bitrd 279 |
. . . . . . . 8
β’ (π = π β (βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
23 | 22 | cbvralvw 3224 |
. . . . . . 7
β’
(βπ β
π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
24 | 23 | a1i 11 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
25 | 8, 24 | bitrd 279 |
. . . . 5
β’ (π¦ = π₯ β (βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯)) |
26 | 25 | cbvrexvw 3225 |
. . . 4
β’
(βπ¦ β
β βπ β
π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯) |
27 | | breq1 5109 |
. . . . . . 7
β’ (π¦ = π₯ β (π¦ β€ (πΉβπ) β π₯ β€ (πΉβπ))) |
28 | 27 | ralbidv 3171 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π π¦ β€ (πΉβπ) β βπ β π π₯ β€ (πΉβπ))) |
29 | 15, 14, 13 | nfbr 5153 |
. . . . . . . 8
β’
β²π π₯ β€ (πΉβπ) |
30 | | nfv 1918 |
. . . . . . . 8
β’
β²π π₯ β€ (πΉβπ) |
31 | 18 | breq2d 5118 |
. . . . . . . 8
β’ (π = π β (π₯ β€ (πΉβπ) β π₯ β€ (πΉβπ))) |
32 | 29, 30, 31 | cbvralw 3288 |
. . . . . . 7
β’
(βπ β
π π₯ β€ (πΉβπ) β βπ β π π₯ β€ (πΉβπ)) |
33 | 32 | a1i 11 |
. . . . . 6
β’ (π¦ = π₯ β (βπ β π π₯ β€ (πΉβπ) β βπ β π π₯ β€ (πΉβπ))) |
34 | 28, 33 | bitrd 279 |
. . . . 5
β’ (π¦ = π₯ β (βπ β π π¦ β€ (πΉβπ) β βπ β π π₯ β€ (πΉβπ))) |
35 | 34 | cbvrexvw 3225 |
. . . 4
β’
(βπ¦ β
β βπ β
π π¦ β€ (πΉβπ) β βπ₯ β β βπ β π π₯ β€ (πΉβπ)) |
36 | 26, 35 | anbi12i 628 |
. . 3
β’
((βπ¦ β
β βπ β
π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β§ βπ¦ β β βπ β π π¦ β€ (πΉβπ)) β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ))) |
37 | 36 | a1i 11 |
. 2
β’ (π β ((βπ¦ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π¦ β§ βπ¦ β β βπ β π π¦ β€ (πΉβπ)) β (βπ₯ β β βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ)))) |
38 | 5, 37 | bitrd 279 |
1
β’ (π β ((lim infβπΉ) β β β
(βπ₯ β β
βπ β π βπ β (β€β₯βπ)(πΉβπ) β€ π₯ β§ βπ₯ β β βπ β π π₯ β€ (πΉβπ)))) |