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 bilani 
 |-  ( ( ph /\ F e. dom ~~>* ) -> F ~~>* ( ~~>* ` F ) )
6 1 adantr 
 |-  ( ( ph /\ F e. dom ~~>* ) -> F e. ( RR* ^pm CC ) )
7 2 adantr 
 |-  ( ( ph /\ F e. dom ~~>* ) -> M e. ZZ )
8 6 7 xlimres 
 |-  ( ( ph /\ F e. dom ~~>* ) -> ( F ~~>* ( ~~>* ` F ) <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` F ) ) )
9 5 8 mpbid 
 |-  ( ( ph /\ F e. dom ~~>* ) -> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` F ) )
10 releldm 
 |-  ( ( Rel ~~>* /\ ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` F ) ) -> ( F |` ( ZZ>= ` M ) ) e. dom ~~>* )
11 3 9 10 sylancr 
 |-  ( ( ph /\ F e. dom ~~>* ) -> ( F |` ( ZZ>= ` M ) ) e. dom ~~>* )
12 xlimdm 
 |-  ( ( F |` ( ZZ>= ` M ) ) e. dom ~~>* <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) )
13 12 bilani 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) )
14 1 2 xlimres 
 |-  ( ph -> ( F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) ) )
15 14 adantr 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> ( F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) <-> ( F |` ( ZZ>= ` M ) ) ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) ) )
16 13 15 mpbird 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) )
17 releldm 
 |-  ( ( Rel ~~>* /\ F ~~>* ( ~~>* ` ( F |` ( ZZ>= ` M ) ) ) ) -> F e. dom ~~>* )
18 3 16 17 sylancr 
 |-  ( ( ph /\ ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) -> F e. dom ~~>* )
19 11 18 impbida 
 |-  ( ph -> ( F e. dom ~~>* <-> ( F |` ( ZZ>= ` M ) ) e. dom ~~>* ) )