Theorem climresdm

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

	Ref	Expression
Hypotheses	climresdm.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climresdm.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion	climresdm	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) )

Proof

Step	Hyp	Ref	Expression
1		climresdm.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		climresdm.2	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		resexg	⊢ ( 𝐹 ∈ dom ⇝ → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ V )
4	3	adantl	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ V )
5		fvexd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ⇝ ‘ 𝐹 ) ∈ V )
6		climdm	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
7	6	bilani	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
9		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
10	8 9	climresd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ) )
11	7 10	mpbird	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ 𝐹 ) )
12	4 5 11	breldmd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ )
13	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
14		fvexd	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ∈ V )
15		climdm	⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
16	15	bilani	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
17	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
18	17 13	climresd	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ↔ 𝐹 ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) )
19	16 18	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
20	13 14 19	breldmd	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
21	12 20	impbida	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) )