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	bilani	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → 𝑀 ∈ ℤ )
8	6 7	xlimres	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → ( 𝐹 ~~>* ( ~~>* ‘ 𝐹 ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ 𝐹 ) ) )
9	5 8	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ 𝐹 ) )
10		releldm	⊢ ( ( Rel ~~>* ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ 𝐹 ) ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* )
11	3 9 10	sylancr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ~~>* ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* )
12		xlimdm	⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
13	12	bilani	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
14	1 2	xlimres	⊢ ( 𝜑 → ( 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → ( 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) )
16	13 15	mpbird	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
17		releldm	⊢ ( ( Rel ~~>* ∧ 𝐹 ~~>* ( ~~>* ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) → 𝐹 ∈ dom ~~>* )
18	3 16 17	sylancr	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) → 𝐹 ∈ dom ~~>* )
19	11 18	impbida	⊢ ( 𝜑 → ( 𝐹 ∈ dom ~~>* ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ~~>* ) )