Step | Hyp | Ref
| Expression |
1 | | nfmpt1 5214 |
. . 3
β’
β²π(π β π β¦ -(πΉβπ)) |
2 | | liminfltlem.m |
. . 3
β’ (π β π β β€) |
3 | | liminfltlem.z |
. . 3
β’ π =
(β€β₯βπ) |
4 | | liminfltlem.f |
. . . . . 6
β’ (π β πΉ:πβΆβ) |
5 | 4 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
6 | 5 | renegcld 11587 |
. . . 4
β’ ((π β§ π β π) β -(πΉβπ) β β) |
7 | 6 | fmpttd 7064 |
. . 3
β’ (π β (π β π β¦ -(πΉβπ)):πβΆβ) |
8 | 3 | fvexi 6857 |
. . . . . . 7
β’ π β V |
9 | 8 | mptex 7174 |
. . . . . 6
β’ (π β π β¦ -(πΉβπ)) β V |
10 | 9 | limsupcli 44084 |
. . . . 5
β’ (lim
supβ(π β π β¦ -(πΉβπ))) β
β* |
11 | 10 | a1i 11 |
. . . 4
β’ (π β (lim supβ(π β π β¦ -(πΉβπ))) β
β*) |
12 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
13 | | nfcv 2904 |
. . . . . 6
β’
β²ππΉ |
14 | 12, 13, 2, 3, 4 | liminfvaluz4 44126 |
. . . . 5
β’ (π β (lim infβπΉ) = -π(lim
supβ(π β π β¦ -(πΉβπ)))) |
15 | | liminfltlem.r |
. . . . 5
β’ (π β (lim infβπΉ) β
β) |
16 | 14, 15 | eqeltrrd 2835 |
. . . 4
β’ (π β -π(lim
supβ(π β π β¦ -(πΉβπ))) β β) |
17 | 11, 16 | xnegrecl2d 43788 |
. . 3
β’ (π β (lim supβ(π β π β¦ -(πΉβπ))) β β) |
18 | | liminfltlem.x |
. . 3
β’ (π β π β
β+) |
19 | 1, 2, 3, 7, 17, 18 | limsupgt 44105 |
. 2
β’ (π β βπ β π βπ β (β€β₯βπ)(((π β π β¦ -(πΉβπ))βπ) β π) < (lim supβ(π β π β¦ -(πΉβπ)))) |
20 | | simpll 766 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π) |
21 | 3 | uztrn2 12787 |
. . . . . 6
β’ ((π β π β§ π β (β€β₯βπ)) β π β π) |
22 | 21 | adantll 713 |
. . . . 5
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β π β π) |
23 | | negex 11404 |
. . . . . . . . . . 11
β’ -(πΉβπ) β V |
24 | | fvmpt4 43551 |
. . . . . . . . . . 11
β’ ((π β π β§ -(πΉβπ) β V) β ((π β π β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
25 | 23, 24 | mpan2 690 |
. . . . . . . . . 10
β’ (π β π β ((π β π β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
26 | 25 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β π β¦ -(πΉβπ))βπ) = -(πΉβπ)) |
27 | 26 | oveq1d 7373 |
. . . . . . . 8
β’ ((π β§ π β π) β (((π β π β¦ -(πΉβπ))βπ) β π) = (-(πΉβπ) β π)) |
28 | 5 | recnd 11188 |
. . . . . . . . 9
β’ ((π β§ π β π) β (πΉβπ) β β) |
29 | 18 | rpred 12962 |
. . . . . . . . . . 11
β’ (π β π β β) |
30 | 29 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β β) |
31 | 30 | recnd 11188 |
. . . . . . . . 9
β’ ((π β§ π β π) β π β β) |
32 | 28, 31 | negdi2d 11531 |
. . . . . . . 8
β’ ((π β§ π β π) β -((πΉβπ) + π) = (-(πΉβπ) β π)) |
33 | 27, 32 | eqtr4d 2776 |
. . . . . . 7
β’ ((π β§ π β π) β (((π β π β¦ -(πΉβπ))βπ) β π) = -((πΉβπ) + π)) |
34 | 17 | recnd 11188 |
. . . . . . . . . 10
β’ (π β (lim supβ(π β π β¦ -(πΉβπ))) β β) |
35 | 17 | rexnegd 43441 |
. . . . . . . . . . 11
β’ (π β -π(lim
supβ(π β π β¦ -(πΉβπ))) = -(lim supβ(π β π β¦ -(πΉβπ)))) |
36 | 14, 35 | eqtr2d 2774 |
. . . . . . . . . 10
β’ (π β -(lim supβ(π β π β¦ -(πΉβπ))) = (lim infβπΉ)) |
37 | 34, 36 | negcon1ad 11512 |
. . . . . . . . 9
β’ (π β -(lim infβπΉ) = (lim supβ(π β π β¦ -(πΉβπ)))) |
38 | 37 | eqcomd 2739 |
. . . . . . . 8
β’ (π β (lim supβ(π β π β¦ -(πΉβπ))) = -(lim infβπΉ)) |
39 | 38 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β (lim supβ(π β π β¦ -(πΉβπ))) = -(lim infβπΉ)) |
40 | 33, 39 | breq12d 5119 |
. . . . . 6
β’ ((π β§ π β π) β ((((π β π β¦ -(πΉβπ))βπ) β π) < (lim supβ(π β π β¦ -(πΉβπ))) β -((πΉβπ) + π) < -(lim infβπΉ))) |
41 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π) β (lim infβπΉ) β β) |
42 | 5, 30 | readdcld 11189 |
. . . . . . 7
β’ ((π β§ π β π) β ((πΉβπ) + π) β β) |
43 | 41, 42 | ltnegd 11738 |
. . . . . 6
β’ ((π β§ π β π) β ((lim infβπΉ) < ((πΉβπ) + π) β -((πΉβπ) + π) < -(lim infβπΉ))) |
44 | 40, 43 | bitr4d 282 |
. . . . 5
β’ ((π β§ π β π) β ((((π β π β¦ -(πΉβπ))βπ) β π) < (lim supβ(π β π β¦ -(πΉβπ))) β (lim infβπΉ) < ((πΉβπ) + π))) |
45 | 20, 22, 44 | syl2anc 585 |
. . . 4
β’ (((π β§ π β π) β§ π β (β€β₯βπ)) β ((((π β π β¦ -(πΉβπ))βπ) β π) < (lim supβ(π β π β¦ -(πΉβπ))) β (lim infβπΉ) < ((πΉβπ) + π))) |
46 | 45 | ralbidva 3169 |
. . 3
β’ ((π β§ π β π) β (βπ β (β€β₯βπ)(((π β π β¦ -(πΉβπ))βπ) β π) < (lim supβ(π β π β¦ -(πΉβπ))) β βπ β (β€β₯βπ)(lim infβπΉ) < ((πΉβπ) + π))) |
47 | 46 | rexbidva 3170 |
. 2
β’ (π β (βπ β π βπ β (β€β₯βπ)(((π β π β¦ -(πΉβπ))βπ) β π) < (lim supβ(π β π β¦ -(πΉβπ))) β βπ β π βπ β (β€β₯βπ)(lim infβπΉ) < ((πΉβπ) + π))) |
48 | 19, 47 | mpbid 231 |
1
β’ (π β βπ β π βπ β (β€β₯βπ)(lim infβπΉ) < ((πΉβπ) + π)) |