Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β π β
β) |
2 | | simpl 483 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β π β
β) |
3 | 1, 2 | ifcld 4530 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β β) |
4 | 3 | adantll 712 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β if(π β€ π, π, π) β β) |
5 | | liminflelimsuplem.2 |
. . . . . . . . . . 11
β’ (π β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
) |
6 | 5 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β β) β βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
) |
7 | | oveq1 7360 |
. . . . . . . . . . . 12
β’ (π = if(π β€ π, π, π) β (π[,)+β) = (if(π β€ π, π, π)[,)+β)) |
8 | 7 | rexeqdv 3312 |
. . . . . . . . . . 11
β’ (π = if(π β€ π, π, π) β (βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
β βπ
β (if(π β€ π, π, π)[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
)) |
9 | 8 | rspcva 3577 |
. . . . . . . . . 10
β’
((if(π β€ π, π, π) β β β§ βπ β β βπ β (π[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
) β βπ
β (if(π β€ π, π, π)[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
) |
10 | 4, 6, 9 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β βπ β (if(π β€ π, π, π)[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
) |
11 | | inss2 4187 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (π[,)+β)) β© β*)
β β* |
12 | | infxrcl 13244 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (π[,)+β)) β© β*)
β β* β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β β*) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
inf(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β
β* |
14 | 13 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β
β*) |
15 | | inss2 4187 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (π[,)+β)) β© β*)
β β* |
16 | | infxrcl 13244 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (π[,)+β)) β© β*)
β β* β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β β*) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
inf(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β
β* |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β
β*) |
19 | | inss2 4187 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (π[,)+β)) β© β*)
β β* |
20 | | supxrcl 13226 |
. . . . . . . . . . . . . 14
β’ (((πΉ β (π[,)+β)) β© β*)
β β* β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β β*) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β
β* |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β sup(((πΉ
β (π[,)+β))
β© β*), β*, < ) β
β*) |
23 | | rexr 11197 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β*) |
24 | 23 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β β*) |
25 | | pnfxr 11205 |
. . . . . . . . . . . . . . . . . 18
β’ +β
β β* |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β +β β
β*) |
27 | 3 | rexrd 11201 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β if(π β€ π, π, π) β
β*) |
28 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β if(π β€ π, π, π) β
β*) |
29 | | icossxr 13341 |
. . . . . . . . . . . . . . . . . . . 20
β’ (if(π β€ π, π, π)[,)+β) β
β* |
30 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (if(π β€ π, π, π)[,)+β) β π β (if(π β€ π, π, π)[,)+β)) |
31 | 29, 30 | sselid 3940 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (if(π β€ π, π, π)[,)+β) β π β β*) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β β*) |
33 | | max1 13096 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β) β π β€ if(π β€ π, π, π)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β€ if(π β€ π, π, π)) |
35 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β (if(π β€ π, π, π)[,)+β)) |
36 | 28, 26, 35 | icogelbd 43728 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β if(π β€ π, π, π) β€ π) |
37 | 24, 28, 32, 34, 36 | xrletrd 13073 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β€ π) |
38 | 24, 26, 37 | icossico2 43734 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β (π[,)+β) β (π[,)+β)) |
39 | 38 | imass2d 43427 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β (πΉ β (π[,)+β)) β (πΉ β (π[,)+β))) |
40 | 39 | ssrind 4193 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β ((πΉ β (π[,)+β)) β© β*)
β ((πΉ β (π[,)+β)) β©
β*)) |
41 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β ((πΉ β (π[,)+β)) β© β*)
β β*) |
42 | | infxrss 13250 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β (π[,)+β)) β© β*)
β ((πΉ β (π[,)+β)) β©
β*) β§ ((πΉ β (π[,)+β)) β© β*)
β β*) β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
43 | 40, 41, 42 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
44 | 43 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
45 | | supxrcl 13226 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β (π[,)+β)) β© β*)
β β* β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β β*) |
46 | 15, 45 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β
β* |
47 | 46 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β sup(((πΉ
β (π[,)+β))
β© β*), β*, < ) β
β*) |
48 | 15 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β ((πΉ β
(π[,)+β)) β©
β*) β β*) |
49 | | simpr 485 |
. . . . . . . . . . . . . 14
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β ((πΉ β
(π[,)+β)) β©
β*) β β
) |
50 | 48, 49 | infxrlesupxr 43607 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
51 | | rexr 11197 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β*) |
52 | 51 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β β*) |
53 | | max2 13098 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ π β β) β π β€ if(π β€ π, π, π)) |
54 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β€ if(π β€ π, π, π)) |
55 | 52, 28, 32, 54, 36 | xrletrd 13073 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β π β€ π) |
56 | 52, 26, 55 | icossico2 43734 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β (π[,)+β) β (π[,)+β)) |
57 | 56 | imass2d 43427 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β (πΉ β (π[,)+β)) β (πΉ β (π[,)+β))) |
58 | 57 | ssrind 4193 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β ((πΉ β (π[,)+β)) β© β*)
β ((πΉ β (π[,)+β)) β©
β*)) |
59 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β ((πΉ β (π[,)+β)) β© β*)
β β*) |
60 | | supxrss 13243 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β (π[,)+β)) β© β*)
β ((πΉ β (π[,)+β)) β©
β*) β§ ((πΉ β (π[,)+β)) β© β*)
β β*) β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
61 | 58, 59, 60 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . 13
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β sup(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
63 | 18, 47, 22, 50, 62 | xrletrd 13073 |
. . . . . . . . . . . 12
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
64 | 14, 18, 22, 44, 63 | xrletrd 13073 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
65 | 64 | ad5ant2345 1370 |
. . . . . . . . . 10
β’
(((((π β§ π β β) β§ π β β) β§ π β (if(π β€ π, π, π)[,)+β)) β§ ((πΉ β (π[,)+β)) β© β*) β
β
) β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
66 | 65 | rexlimdva2 3152 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β β) β (βπ β (if(π β€ π, π, π)[,)+β)((πΉ β (π[,)+β)) β© β*) β
β
β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
67 | 10, 66 | mpd 15 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β β) β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
68 | 67 | ralrimiva 3141 |
. . . . . . 7
β’ ((π β§ π β β) β βπ β β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
69 | | nfv 1917 |
. . . . . . . . 9
β’
β²ππ |
70 | | xrltso 13052 |
. . . . . . . . . . 11
β’ < Or
β* |
71 | 70 | supex 9395 |
. . . . . . . . . 10
β’
sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β V |
72 | 71 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β β) β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β V) |
73 | | breq2 5107 |
. . . . . . . . 9
β’ (π¦ = sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β (inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦ β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
74 | 69, 72, 73 | ralrnmpt3 43423 |
. . . . . . . 8
β’ (π β (βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦ β βπ β β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
75 | 74 | adantr 481 |
. . . . . . 7
β’ ((π β§ π β β) β (βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦ β βπ β β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))) |
76 | 68, 75 | mpbird 256 |
. . . . . 6
β’ ((π β§ π β β) β βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦) |
77 | | oveq1 7360 |
. . . . . . . . . . . . 13
β’ (π = π β (π[,)+β) = (π[,)+β)) |
78 | 77 | imaeq2d 6011 |
. . . . . . . . . . . 12
β’ (π = π β (πΉ β (π[,)+β)) = (πΉ β (π[,)+β))) |
79 | 78 | ineq1d 4169 |
. . . . . . . . . . 11
β’ (π = π β ((πΉ β (π[,)+β)) β© β*) =
((πΉ β (π[,)+β)) β©
β*)) |
80 | 79 | supeq1d 9378 |
. . . . . . . . . 10
β’ (π = π β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) = sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
81 | 80 | cbvmptv 5216 |
. . . . . . . . 9
β’ (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
82 | 81 | rneqi 5890 |
. . . . . . . 8
β’ ran
(π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) = ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
83 | 82 | raleqi 3309 |
. . . . . . 7
β’
(βπ¦ β
ran (π β β
β¦ sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦ β βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦) |
84 | 83 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β (βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦ β βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦)) |
85 | 76, 84 | mpbid 231 |
. . . . 5
β’ ((π β§ π β β) β βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦) |
86 | | supxrcl 13226 |
. . . . . . . . . 10
β’ (((πΉ β (π[,)+β)) β© β*)
β β* β sup(((πΉ β (π[,)+β)) β© β*),
β*, < ) β β*) |
87 | 11, 86 | ax-mp 5 |
. . . . . . . . 9
β’
sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β
β* |
88 | 87 | rgenw 3066 |
. . . . . . . 8
β’
βπ β
β sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β
β* |
89 | | eqid 2736 |
. . . . . . . . 9
β’ (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) = (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
90 | 89 | rnmptss 7066 |
. . . . . . . 8
β’
(βπ β
β sup(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β β*
β ran (π β
β β¦ sup(((πΉ
β (π[,)+β))
β© β*), β*, < )) β
β*) |
91 | 88, 90 | ax-mp 5 |
. . . . . . 7
β’ ran
(π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) β
β* |
92 | 91 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β ran (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) β
β*) |
93 | 13 | a1i 11 |
. . . . . 6
β’ ((π β§ π β β) β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β β*) |
94 | | infxrgelb 13246 |
. . . . . 6
β’ ((ran
(π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) β β*
β§ inf(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β β*)
β (inf(((πΉ β
(π[,)+β)) β©
β*), β*, < ) β€ inf(ran (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, < )
β βπ¦ β ran
(π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦)) |
95 | 92, 93, 94 | syl2anc 584 |
. . . . 5
β’ ((π β§ π β β) β (inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ inf(ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < ) β βπ¦ β ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < ))inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ π¦)) |
96 | 85, 95 | mpbird 256 |
. . . 4
β’ ((π β§ π β β) β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ inf(ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
97 | 96 | ralrimiva 3141 |
. . 3
β’ (π β βπ β β inf(((πΉ β (π[,)+β)) β© β*),
β*, < ) β€ inf(ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
98 | | nfv 1917 |
. . . 4
β’
β²ππ |
99 | | nfcv 2905 |
. . . 4
β’
β²πβ |
100 | | nfmpt1 5211 |
. . . . . 6
β’
β²π(π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
101 | 100 | nfrn 5905 |
. . . . 5
β’
β²πran
(π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) |
102 | | nfcv 2905 |
. . . . 5
β’
β²πβ* |
103 | | nfcv 2905 |
. . . . 5
β’
β²π
< |
104 | 101, 102,
103 | nfinf 9414 |
. . . 4
β’
β²πinf(ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < ) |
105 | | infxrcl 13244 |
. . . . . 6
β’ (ran
(π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )) β β*
β inf(ran (π β
β β¦ sup(((πΉ
β (π[,)+β))
β© β*), β*, < )), β*,
< ) β β*) |
106 | 91, 105 | ax-mp 5 |
. . . . 5
β’ inf(ran
(π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, < )
β β* |
107 | 106 | a1i 11 |
. . . 4
β’ (π β inf(ran (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, < )
β β*) |
108 | 98, 99, 104, 93, 107 | supxrleubrnmptf 43622 |
. . 3
β’ (π β (sup(ran (π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, < )
β€ inf(ran (π β
β β¦ sup(((πΉ
β (π[,)+β))
β© β*), β*, < )), β*,
< ) β βπ
β β inf(((πΉ
β (π[,)+β))
β© β*), β*, < ) β€ inf(ran (π β β β¦
sup(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, <
))) |
109 | 97, 108 | mpbird 256 |
. 2
β’ (π β sup(ran (π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, < )
β€ inf(ran (π β
β β¦ sup(((πΉ
β (π[,)+β))
β© β*), β*, < )), β*,
< )) |
110 | | liminflelimsuplem.1 |
. . . 4
β’ (π β πΉ β π) |
111 | | eqid 2736 |
. . . 4
β’ (π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )) = (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )) |
112 | 110, 111 | liminfvald 43937 |
. . 3
β’ (π β (lim infβπΉ) = sup(ran (π β β β¦ inf(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
113 | 110, 89 | limsupvald 43928 |
. . 3
β’ (π β (lim supβπΉ) = inf(ran (π β β β¦ sup(((πΉ β (π[,)+β)) β© β*),
β*, < )), β*, < )) |
114 | 112, 113 | breq12d 5116 |
. 2
β’ (π β ((lim infβπΉ) β€ (lim supβπΉ) β sup(ran (π β β β¦
inf(((πΉ β (π[,)+β)) β©
β*), β*, < )), β*, < )
β€ inf(ran (π β
β β¦ sup(((πΉ
β (π[,)+β))
β© β*), β*, < )), β*,
< ))) |
115 | 109, 114 | mpbird 256 |
1
β’ (π β (lim infβπΉ) β€ (lim supβπΉ)) |