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 sselid 
 |-  ( ( 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 sselid 
 |-  ( ( 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 sselid 
 |-  ( 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 ) ) )