Metamath Proof Explorer

Theorem smflimsuplem4

Description: If H converges, the limsup of F is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses smflimsuplem4.1 
|- F/ n ph
smflimsuplem4.m 
|- ( ph -> M e. ZZ )
smflimsuplem4.z 
|- Z = ( ZZ>= ` M )
smflimsuplem4.s 
|- ( ph -> S e. SAlg )
smflimsuplem4.f 
|- ( ph -> F : Z --> ( SMblFn ` S ) )
smflimsuplem4.e 
|- E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
smflimsuplem4.h 
|- H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
smflimsuplem4.n 
|- ( ph -> N e. Z )
smflimsuplem4.i 
|- ( ph -> x e. |^|_ n e. ( ZZ>= ` N ) dom ( H ` n ) )
smflimsuplem4.c 
|- ( ph -> ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> )
Assertion smflimsuplem4 
|- ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )

Proof

Step Hyp Ref Expression
1 smflimsuplem4.1 
 |-  F/ n ph
2 smflimsuplem4.m 
 |-  ( ph -> M e. ZZ )
3 smflimsuplem4.z 
 |-  Z = ( ZZ>= ` M )
4 smflimsuplem4.s 
 |-  ( ph -> S e. SAlg )
5 smflimsuplem4.f 
 |-  ( ph -> F : Z --> ( SMblFn ` S ) )
6 smflimsuplem4.e 
 |-  E = ( n e. Z |-> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
7 smflimsuplem4.h 
 |-  H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
8 smflimsuplem4.n 
 |-  ( ph -> N e. Z )
9 smflimsuplem4.i 
 |-  ( ph -> x e. |^|_ n e. ( ZZ>= ` N ) dom ( H ` n ) )
10 smflimsuplem4.c 
 |-  ( ph -> ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> )
11 nfv 
 |-  F/ m ph
12 3 8 eluzelz2d 
 |-  ( ph -> N e. ZZ )
13 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
14 fvexd 
 |-  ( ( ph /\ m e. Z ) -> ( ( F ` m ) ` x ) e. _V )
15 fvexd 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( ( F ` m ) ` x ) e. _V )
16 11 2 12 3 13 14 15 limsupequzmpt 
 |-  ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` x ) ) ) )
17 4 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> S e. SAlg )
18 3 8 uzssd2 
 |-  ( ph -> ( ZZ>= ` N ) C_ Z )
19 18 sselda 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> m e. Z )
20 5 ffvelcdmda 
 |-  ( ( ph /\ m e. Z ) -> ( F ` m ) e. ( SMblFn ` S ) )
21 19 20 syldan 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( F ` m ) e. ( SMblFn ` S ) )
22 eqid 
 |-  dom ( F ` m ) = dom ( F ` m )
23 17 21 22 smff 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( F ` m ) : dom ( F ` m ) --> RR )
24 3 6 7 19 smflimsuplem1 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> dom ( H ` m ) C_ dom ( F ` m ) )
25 9 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> x e. |^|_ n e. ( ZZ>= ` N ) dom ( H ` n ) )
26 simpr 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> m e. ( ZZ>= ` N ) )
27 fveq2 
 |-  ( n = m -> ( H ` n ) = ( H ` m ) )
28 27 dmeqd 
 |-  ( n = m -> dom ( H ` n ) = dom ( H ` m ) )
29 28 eleq2d 
 |-  ( n = m -> ( x e. dom ( H ` n ) <-> x e. dom ( H ` m ) ) )
30 25 26 29 eliind 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> x e. dom ( H ` m ) )
31 24 30 sseldd 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> x e. dom ( F ` m ) )
32 23 31 ffvelcdmd 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( ( F ` m ) ` x ) e. RR )
33 32 rexrd 
 |-  ( ( ph /\ m e. ( ZZ>= ` N ) ) -> ( ( F ` m ) ` x ) e. RR* )
34 11 12 13 33 limsupvaluzmpt 
 |-  ( ph -> ( limsup ` ( m e. ( ZZ>= ` N ) |-> ( ( F ` m ) ` x ) ) ) = inf ( ran ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) , RR* , < ) )
35 16 34 eqtrd 
 |-  ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) = inf ( ran ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) , RR* , < ) )
36 18 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ZZ>= ` N ) C_ Z )
37 simpr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. ( ZZ>= ` N ) )
38 36 37 sseldd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. Z )
39 7 a1i 
 |-  ( ph -> H = ( n e. Z |-> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ) )
40 fvex 
 |-  ( E ` n ) e. _V
41 40 mptex 
 |-  ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V
42 41 a1i 
 |-  ( ( ph /\ n e. Z ) -> ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. _V )
43 39 42 fvmpt2d 
 |-  ( ( ph /\ n e. Z ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
44 38 43 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( H ` n ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
45 44 dmeqd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> dom ( H ` n ) = dom ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
46 xrltso 
 |-  < Or RR*
47 46 supex 
 |-  sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. _V
48 eqid 
 |-  ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
49 47 48 dmmpti 
 |-  dom ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( E ` n )
50 49 a1i 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> dom ( x e. ( E ` n ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) = ( E ` n ) )
51 45 50 eqtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> dom ( H ` n ) = ( E ` n ) )
52 1 51 iineq2d 
 |-  ( ph -> |^|_ n e. ( ZZ>= ` N ) dom ( H ` n ) = |^|_ n e. ( ZZ>= ` N ) ( E ` n ) )
53 9 52 eleqtrd 
 |-  ( ph -> x e. |^|_ n e. ( ZZ>= ` N ) ( E ` n ) )
54 53 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> x e. |^|_ n e. ( ZZ>= ` N ) ( E ` n ) )
55 eliinid 
 |-  ( ( x e. |^|_ n e. ( ZZ>= ` N ) ( E ` n ) /\ n e. ( ZZ>= ` N ) ) -> x e. ( E ` n ) )
56 54 37 55 syl2anc 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> x e. ( E ` n ) )
57 47 a1i 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ x e. ( E ` n ) ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. _V )
58 44 57 fvmpt2d 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ x e. ( E ` n ) ) -> ( ( H ` n ) ` x ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
59 56 58 mpdan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` x ) = sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
60 eqid 
 |-  { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR }
61 3 eluzelz2 
 |-  ( n e. Z -> n e. ZZ )
62 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
63 61 62 uzn0d 
 |-  ( n e. Z -> ( ZZ>= ` n ) =/= (/) )
64 fvex 
 |-  ( F ` m ) e. _V
65 64 dmex 
 |-  dom ( F ` m ) e. _V
66 65 rgenw 
 |-  A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V
67 66 a1i 
 |-  ( n e. Z -> A. m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
68 63 67 iinexd 
 |-  ( n e. Z -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
69 68 adantl 
 |-  ( ( ph /\ n e. Z ) -> |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) e. _V )
70 60 69 rabexd 
 |-  ( ( ph /\ n e. Z ) -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V )
71 38 70 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V )
72 6 fvmpt2 
 |-  ( ( n e. Z /\ { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } e. _V ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
73 38 71 72 syl2anc 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( E ` n ) = { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
74 56 73 eleqtrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> x e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } )
75 rabid 
 |-  ( x e. { x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) | sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR } <-> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) )
76 74 75 sylib 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( x e. |^|_ m e. ( ZZ>= ` n ) dom ( F ` m ) /\ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR ) )
77 76 simprd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) e. RR )
78 59 77 eqeltrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` x ) e. RR )
79 1 59 mpteq2da 
 |-  ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` x ) ) = ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) )
80 nfv 
 |-  F/ k ph
81 fveq2 
 |-  ( n = k -> ( ZZ>= ` n ) = ( ZZ>= ` k ) )
82 81 mpteq1d 
 |-  ( n = k -> ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) )
83 82 rneqd 
 |-  ( n = k -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) )
84 83 supeq1d 
 |-  ( n = k -> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) = sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
85 nfv 
 |-  F/ m ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) )
86 eluzelz 
 |-  ( n e. ( ZZ>= ` N ) -> n e. ZZ )
87 86 adantr 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> n e. ZZ )
88 simpr 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> k = ( n + 1 ) )
89 87 peano2zd 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> ( n + 1 ) e. ZZ )
90 88 89 eqeltrd 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> k e. ZZ )
91 87 zred 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> n e. RR )
92 90 zred 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> k e. RR )
93 91 ltp1d 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> n < ( n + 1 ) )
94 88 eqcomd 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> ( n + 1 ) = k )
95 93 94 breqtrd 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> n < k )
96 91 92 95 ltled 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> n <_ k )
97 62 87 90 96 eluzd 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> k e. ( ZZ>= ` n ) )
98 uzss 
 |-  ( k e. ( ZZ>= ` n ) -> ( ZZ>= ` k ) C_ ( ZZ>= ` n ) )
99 97 98 syl 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> ( ZZ>= ` k ) C_ ( ZZ>= ` n ) )
100 fvexd 
 |-  ( ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) /\ m e. ( ZZ>= ` k ) ) -> ( ( F ` m ) ` x ) e. _V )
101 85 99 100 rnmptss2 
 |-  ( ( n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) C_ ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) )
102 101 3adant1 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) C_ ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) )
103 nfv 
 |-  F/ m ( ph /\ n e. ( ZZ>= ` N ) )
104 eqid 
 |-  ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) = ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) )
105 simpll 
 |-  ( ( ( ph /\ n e. Z ) /\ m e. ( ZZ>= ` n ) ) -> ph )
106 38 105 syldanl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> ph )
107 13 uztrn2 
 |-  ( ( n e. ( ZZ>= ` N ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` N ) )
108 107 adantll 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> m e. ( ZZ>= ` N ) )
109 106 108 32 syl2anc 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ZZ>= ` n ) ) -> ( ( F ` m ) ` x ) e. RR )
110 103 104 109 rnmptssd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) C_ RR )
111 ressxr 
 |-  RR C_ RR*
112 111 a1i 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> RR C_ RR* )
113 110 112 sstrd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) C_ RR* )
114 113 3adant3 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) C_ RR* )
115 supxrss 
 |-  ( ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) C_ ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) /\ ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) C_ RR* ) -> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) <_ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
116 102 114 115 syl2anc 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) /\ k = ( n + 1 ) ) -> sup ( ran ( m e. ( ZZ>= ` k ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) <_ sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) )
117 3 fvexi 
 |-  Z e. _V
118 117 a1i 
 |-  ( ph -> Z e. _V )
119 fvexd 
 |-  ( ( ph /\ n e. Z ) -> ( ( H ` n ) ` x ) e. _V )
120 fvexd 
 |-  ( ph -> ( ZZ>= ` N ) e. _V )
121 1 37 ssdf 
 |-  ( ph -> ( ZZ>= ` N ) C_ ( ZZ>= ` N ) )
122 fvexd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` x ) e. _V )
123 eqidd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( ( H ` n ) ` x ) = ( ( H ` n ) ` x ) )
124 1 12 13 118 18 119 120 121 122 123 climeldmeqmpt 
 |-  ( ph -> ( ( n e. Z |-> ( ( H ` n ) ` x ) ) e. dom ~~> <-> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` x ) ) e. dom ~~> ) )
125 10 124 mpbid 
 |-  ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` x ) ) e. dom ~~> )
126 79 125 eqeltrrd 
 |-  ( ph -> ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) e. dom ~~> )
127 1 80 12 13 77 84 116 126 climinf2mpt 
 |-  ( ph -> ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) ~~> inf ( ran ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) , RR* , < ) )
128 79 127 eqbrtrd 
 |-  ( ph -> ( n e. ( ZZ>= ` N ) |-> ( ( H ` n ) ` x ) ) ~~> inf ( ran ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) , RR* , < ) )
129 1 12 13 78 128 climreclmpt 
 |-  ( ph -> inf ( ran ( n e. ( ZZ>= ` N ) |-> sup ( ran ( m e. ( ZZ>= ` n ) |-> ( ( F ` m ) ` x ) ) , RR* , < ) ) , RR* , < ) e. RR )
130 35 129 eqeltrd 
 |-  ( ph -> ( limsup ` ( m e. Z |-> ( ( F ` m ) ` x ) ) ) e. RR )