Metamath Proof Explorer

Theorem xlimresdm

Description: A function converges in the extended reals iff its restriction to an upper integers set converges. (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses xlimresdm.1 
|- ( ph -> F e. ( RR* ^pm CC ) )
xlimresdm.2 
|- ( ph -> M e. ZZ )
Assertion xlimresdm 
|- ( ph -> ( F e. dom ~~>* <-> ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) )

Proof

Step Hyp Ref Expression
1 xlimresdm.1 
 |-  ( ph -> F e. ( RR* ^pm CC ) )
2 xlimresdm.2 
 |-  ( ph -> M e. ZZ )
3 xlimrel 
 |-  Rel ~~>*
4 xlimdm 
 |-  ( F e. dom ~~>* <-> F ~~>* ( ~~>* ` F ) )
5 4 a1i 
 |-  ( ph -> ( F e. dom ~~>* <-> F ~~>* ( ~~>* ` F ) ) )
6 5 biimpa 
 |-  ( ( ph /\ F e. dom ~~>* ) -> F ~~>* ( ~~>* ` F ) )
7 1 adantr 
 |-  ( ( ph /\ F e. dom ~~>* ) -> F e. ( RR* ^pm CC ) )
8 2 adantr 
 |-  ( ( ph /\ F e. dom ~~>* ) -> M e. ZZ )
9 7 8 xlimres 
 |-  ( ( ph /\ F e. dom ~~>* ) -> ( F ~~>* ( ~~>* ` F ) <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` F ) ) )
10 6 9 mpbid 
 |-  ( ( ph /\ F e. dom ~~>* ) -> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` F ) )
11 releldm 
 |-  ( ( Rel ~~>* /\ ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` F ) ) -> ( F |` ( ZZ>= ` M ) ) e. dom ~~>* )
12 3 10 11 sylancr 
 |-  ( ( ph /\ F e. dom ~~>* ) -> ( F |` ( ZZ>= ` M ) ) e. dom ~~>* )
13 xlimdm 
 |-  ( ( F |` ( ZZ>= ` M ) ) e. dom ~~>* <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) )
14 13 biimpi 
 |-  ( ( F |` ( ZZ>= ` M ) ) e. dom ~~>* -> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) )
15 14 adantl 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) )
16 1 2 xlimres 
 |-  ( ph -> ( F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) ) )
17 16 adantr 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> ( F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) ) )
18 15 17 mpbird 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) )
19 releldm 
 |-  ( ( Rel ~~>* /\ F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) ) -> F e. dom ~~>* )
20 3 18 19 sylancr 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> F e. dom ~~>* )
21 12 20 impbida 
 |-  ( ph -> ( F e. dom ~~>* <-> ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) )