Metamath Proof Explorer


Theorem limsupre3uzlem

Description: Given a function on the extended reals, its supremum limit is real if and only if two condition holds: 1. there is a real number that is less than or equal to the function, infinitely often; 2. there is a real number that is eventually greater than or equal to the function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupre3uzlem.1
|- F/_ j F
limsupre3uzlem.2
|- ( ph -> M e. ZZ )
limsupre3uzlem.3
|- Z = ( ZZ>= ` M )
limsupre3uzlem.4
|- ( ph -> F : Z --> RR* )
Assertion limsupre3uzlem
|- ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )

Proof

Step Hyp Ref Expression
1 limsupre3uzlem.1
 |-  F/_ j F
2 limsupre3uzlem.2
 |-  ( ph -> M e. ZZ )
3 limsupre3uzlem.3
 |-  Z = ( ZZ>= ` M )
4 limsupre3uzlem.4
 |-  ( ph -> F : Z --> RR* )
5 uzssre
 |-  ( ZZ>= ` M ) C_ RR
6 3 5 eqsstri
 |-  Z C_ RR
7 6 a1i
 |-  ( ph -> Z C_ RR )
8 1 7 4 limsupre3
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) ) )
9 breq1
 |-  ( y = k -> ( y <_ j <-> k <_ j ) )
10 9 anbi1d
 |-  ( y = k -> ( ( y <_ j /\ x <_ ( F ` j ) ) <-> ( k <_ j /\ x <_ ( F ` j ) ) ) )
11 10 rexbidv
 |-  ( y = k -> ( E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) <-> E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) ) )
12 11 cbvralvw
 |-  ( A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) <-> A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) )
13 12 biimpi
 |-  ( A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) -> A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) )
14 nfra1
 |-  F/ k A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) )
15 simpr
 |-  ( ( A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) /\ k e. Z ) -> k e. Z )
16 6 15 sseldi
 |-  ( ( A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) /\ k e. Z ) -> k e. RR )
17 rspa
 |-  ( ( A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) /\ k e. RR ) -> E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) )
18 16 17 syldan
 |-  ( ( A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) /\ k e. Z ) -> E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) )
19 nfv
 |-  F/ j k e. Z
20 nfre1
 |-  F/ j E. j e. ( ZZ>= ` k ) x <_ ( F ` j )
21 eqid
 |-  ( ZZ>= ` k ) = ( ZZ>= ` k )
22 3 eluzelz2
 |-  ( k e. Z -> k e. ZZ )
23 22 3ad2ant1
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> k e. ZZ )
24 3 eluzelz2
 |-  ( j e. Z -> j e. ZZ )
25 24 3ad2ant2
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> j e. ZZ )
26 simp3
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> k <_ j )
27 21 23 25 26 eluzd
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> j e. ( ZZ>= ` k ) )
28 27 3adant3r
 |-  ( ( k e. Z /\ j e. Z /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> j e. ( ZZ>= ` k ) )
29 simp3r
 |-  ( ( k e. Z /\ j e. Z /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> x <_ ( F ` j ) )
30 rspe
 |-  ( ( j e. ( ZZ>= ` k ) /\ x <_ ( F ` j ) ) -> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
31 28 29 30 syl2anc
 |-  ( ( k e. Z /\ j e. Z /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
32 31 3exp
 |-  ( k e. Z -> ( j e. Z -> ( ( k <_ j /\ x <_ ( F ` j ) ) -> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) ) )
33 19 20 32 rexlimd
 |-  ( k e. Z -> ( E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) -> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
34 33 imp
 |-  ( ( k e. Z /\ E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) ) -> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
35 15 18 34 syl2anc
 |-  ( ( A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) /\ k e. Z ) -> E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
36 14 35 ralrimia
 |-  ( A. k e. RR E. j e. Z ( k <_ j /\ x <_ ( F ` j ) ) -> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
37 13 36 syl
 |-  ( A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) -> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
38 37 a1i
 |-  ( ph -> ( A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) -> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
39 iftrue
 |-  ( M <_ ( |^ ` y ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) = ( |^ ` y ) )
40 39 adantl
 |-  ( ( ( ph /\ y e. RR ) /\ M <_ ( |^ ` y ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) = ( |^ ` y ) )
41 2 ad2antrr
 |-  ( ( ( ph /\ y e. RR ) /\ M <_ ( |^ ` y ) ) -> M e. ZZ )
42 ceilcl
 |-  ( y e. RR -> ( |^ ` y ) e. ZZ )
43 42 ad2antlr
 |-  ( ( ( ph /\ y e. RR ) /\ M <_ ( |^ ` y ) ) -> ( |^ ` y ) e. ZZ )
44 simpr
 |-  ( ( ( ph /\ y e. RR ) /\ M <_ ( |^ ` y ) ) -> M <_ ( |^ ` y ) )
45 3 41 43 44 eluzd
 |-  ( ( ( ph /\ y e. RR ) /\ M <_ ( |^ ` y ) ) -> ( |^ ` y ) e. Z )
46 40 45 eqeltrd
 |-  ( ( ( ph /\ y e. RR ) /\ M <_ ( |^ ` y ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z )
47 iffalse
 |-  ( -. M <_ ( |^ ` y ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) = M )
48 47 adantl
 |-  ( ( ph /\ -. M <_ ( |^ ` y ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) = M )
49 2 3 uzidd2
 |-  ( ph -> M e. Z )
50 49 adantr
 |-  ( ( ph /\ -. M <_ ( |^ ` y ) ) -> M e. Z )
51 48 50 eqeltrd
 |-  ( ( ph /\ -. M <_ ( |^ ` y ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z )
52 51 adantlr
 |-  ( ( ( ph /\ y e. RR ) /\ -. M <_ ( |^ ` y ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z )
53 46 52 pm2.61dan
 |-  ( ( ph /\ y e. RR ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z )
54 53 adantlr
 |-  ( ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) /\ y e. RR ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z )
55 simplr
 |-  ( ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) /\ y e. RR ) -> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
56 fveq2
 |-  ( k = if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) -> ( ZZ>= ` k ) = ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) )
57 56 rexeqdv
 |-  ( k = if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) -> ( E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> E. j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) x <_ ( F ` j ) ) )
58 57 rspcva
 |-  ( ( if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) -> E. j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) x <_ ( F ` j ) )
59 54 55 58 syl2anc
 |-  ( ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) /\ y e. RR ) -> E. j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) x <_ ( F ` j ) )
60 nfv
 |-  F/ j ph
61 19 nfci
 |-  F/_ j Z
62 61 20 nfralw
 |-  F/ j A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j )
63 60 62 nfan
 |-  F/ j ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) )
64 nfv
 |-  F/ j y e. RR
65 63 64 nfan
 |-  F/ j ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) /\ y e. RR )
66 nfre1
 |-  F/ j E. j e. Z ( y <_ j /\ x <_ ( F ` j ) )
67 2 ad2antrr
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> M e. ZZ )
68 eluzelz
 |-  ( j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) -> j e. ZZ )
69 68 adantl
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> j e. ZZ )
70 67 zred
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> M e. RR )
71 6 53 sseldi
 |-  ( ( ph /\ y e. RR ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. RR )
72 71 adantr
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. RR )
73 69 zred
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> j e. RR )
74 6 49 sseldi
 |-  ( ph -> M e. RR )
75 74 adantr
 |-  ( ( ph /\ y e. RR ) -> M e. RR )
76 42 zred
 |-  ( y e. RR -> ( |^ ` y ) e. RR )
77 76 adantl
 |-  ( ( ph /\ y e. RR ) -> ( |^ ` y ) e. RR )
78 max1
 |-  ( ( M e. RR /\ ( |^ ` y ) e. RR ) -> M <_ if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) )
79 75 77 78 syl2anc
 |-  ( ( ph /\ y e. RR ) -> M <_ if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) )
80 79 adantr
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> M <_ if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) )
81 eluzle
 |-  ( j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) <_ j )
82 81 adantl
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) <_ j )
83 70 72 73 80 82 letrd
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> M <_ j )
84 3 67 69 83 eluzd
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> j e. Z )
85 84 3adant3
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) /\ x <_ ( F ` j ) ) -> j e. Z )
86 simplr
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> y e. RR )
87 simpr
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
88 ceilge
 |-  ( y e. RR -> y <_ ( |^ ` y ) )
89 88 adantl
 |-  ( ( ph /\ y e. RR ) -> y <_ ( |^ ` y ) )
90 max2
 |-  ( ( M e. RR /\ ( |^ ` y ) e. RR ) -> ( |^ ` y ) <_ if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) )
91 75 77 90 syl2anc
 |-  ( ( ph /\ y e. RR ) -> ( |^ ` y ) <_ if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) )
92 87 77 71 89 91 letrd
 |-  ( ( ph /\ y e. RR ) -> y <_ if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) )
93 92 adantr
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> y <_ if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) )
94 86 72 73 93 82 letrd
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> y <_ j )
95 94 3adant3
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) /\ x <_ ( F ` j ) ) -> y <_ j )
96 simp3
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) /\ x <_ ( F ` j ) ) -> x <_ ( F ` j ) )
97 95 96 jca
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) /\ x <_ ( F ` j ) ) -> ( y <_ j /\ x <_ ( F ` j ) ) )
98 rspe
 |-  ( ( j e. Z /\ ( y <_ j /\ x <_ ( F ` j ) ) ) -> E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) )
99 85 97 98 syl2anc
 |-  ( ( ( ph /\ y e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) /\ x <_ ( F ` j ) ) -> E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) )
100 99 3exp
 |-  ( ( ph /\ y e. RR ) -> ( j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) -> ( x <_ ( F ` j ) -> E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) ) ) )
101 100 adantlr
 |-  ( ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) /\ y e. RR ) -> ( j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) -> ( x <_ ( F ` j ) -> E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) ) ) )
102 65 66 101 rexlimd
 |-  ( ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) /\ y e. RR ) -> ( E. j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) x <_ ( F ` j ) -> E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) ) )
103 59 102 mpd
 |-  ( ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) /\ y e. RR ) -> E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) )
104 103 ralrimiva
 |-  ( ( ph /\ A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) -> A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) )
105 104 ex
 |-  ( ph -> ( A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) -> A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) ) )
106 38 105 impbid
 |-  ( ph -> ( A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) <-> A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
107 106 rexbidv
 |-  ( ph -> ( E. x e. RR A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) <-> E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
108 53 adantr
 |-  ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) -> if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z )
109 60 64 nfan
 |-  F/ j ( ph /\ y e. RR )
110 nfra1
 |-  F/ j A. j e. Z ( y <_ j -> ( F ` j ) <_ x )
111 109 110 nfan
 |-  F/ j ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) )
112 94 adantlr
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> y <_ j )
113 simplr
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) )
114 84 adantlr
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> j e. Z )
115 rspa
 |-  ( ( A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) /\ j e. Z ) -> ( y <_ j -> ( F ` j ) <_ x ) )
116 113 114 115 syl2anc
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> ( y <_ j -> ( F ` j ) <_ x ) )
117 112 116 mpd
 |-  ( ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ) -> ( F ` j ) <_ x )
118 117 ex
 |-  ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) -> ( j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) -> ( F ` j ) <_ x ) )
119 111 118 ralrimi
 |-  ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) -> A. j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ( F ` j ) <_ x )
120 56 raleqdv
 |-  ( k = if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) -> ( A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> A. j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ( F ` j ) <_ x ) )
121 120 rspcev
 |-  ( ( if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) e. Z /\ A. j e. ( ZZ>= ` if ( M <_ ( |^ ` y ) , ( |^ ` y ) , M ) ) ( F ` j ) <_ x ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
122 108 119 121 syl2anc
 |-  ( ( ( ph /\ y e. RR ) /\ A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
123 122 rexlimdva2
 |-  ( ph -> ( E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
124 6 sseli
 |-  ( k e. Z -> k e. RR )
125 124 ad2antlr
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> k e. RR )
126 nfra1
 |-  F/ j A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x
127 19 126 nfan
 |-  F/ j ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
128 simp1r
 |-  ( ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) /\ j e. Z /\ k <_ j ) -> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
129 27 3adant1r
 |-  ( ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) /\ j e. Z /\ k <_ j ) -> j e. ( ZZ>= ` k ) )
130 rspa
 |-  ( ( A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x /\ j e. ( ZZ>= ` k ) ) -> ( F ` j ) <_ x )
131 128 129 130 syl2anc
 |-  ( ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) /\ j e. Z /\ k <_ j ) -> ( F ` j ) <_ x )
132 131 3exp
 |-  ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> ( j e. Z -> ( k <_ j -> ( F ` j ) <_ x ) ) )
133 127 132 ralrimi
 |-  ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) )
134 133 adantll
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) )
135 9 rspceaimv
 |-  ( ( k e. RR /\ A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) ) -> E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) )
136 125 134 135 syl2anc
 |-  ( ( ( ph /\ k e. Z ) /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) )
137 136 rexlimdva2
 |-  ( ph -> ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x -> E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) )
138 123 137 impbid
 |-  ( ph -> ( E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
139 138 rexbidv
 |-  ( ph -> ( E. x e. RR E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) <-> E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
140 107 139 anbi12d
 |-  ( ph -> ( ( E. x e. RR A. y e. RR E. j e. Z ( y <_ j /\ x <_ ( F ` j ) ) /\ E. x e. RR E. y e. RR A. j e. Z ( y <_ j -> ( F ` j ) <_ x ) ) <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
141 8 140 bitrd
 |-  ( ph -> ( ( limsup ` F ) e. RR <-> ( E. x e. RR A. k e. Z E. j e. ( ZZ>= ` k ) x <_ ( F ` j ) /\ E. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )