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 ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
xlimresdm.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion xlimresdm ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) )

Proof

Step Hyp Ref Expression
1 xlimresdm.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
2 xlimresdm.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 xlimrel ⊢ Rel ~~>*
4 xlimdm ⊢ ( 𝐹 ∈ dom ~~>* ↔ 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
5 4 a1i ⊢ ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) ) )
6 5 biimpa ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
7 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
8 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → 𝑀 ∈ ℤ )
9 7 8 xlimres ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → ( 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ 𝐹 ) ) )
10 6 9 mpbid ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ 𝐹 ) )
11 releldm ⊢ ( ( Rel ~~>* ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ 𝐹 ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* )
12 3 10 11 sylancr ⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* )
13 xlimdm ⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
14 13 biimpi ⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
16 1 2 xlimres ⊢ ( 𝜑 → ( 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → ( 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) )
18 15 17 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
19 releldm ⊢ ( ( Rel ~~>* ∧ 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) → 𝐹 ∈ dom ~~>* )
20 3 18 19 sylancr ⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → 𝐹 ∈ dom ~~>* )
21 12 20 impbida ⊢ ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) )