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	biimpi	⊢ ( 𝐹 ∈ dom ⇝ → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
8	7	adantl	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
10		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
11	9 10	climresd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ 𝐹 ) ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ) )
12	8 11	mpbird	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ 𝐹 ) )
13	4 5 12	breldmd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ dom ⇝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ )
14	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝐹 ∈ 𝑉 )
15		fvexd	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ∈ V )
16		climdm	⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
17	16	biimpi	⊢ ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
19	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝑀 ∈ ℤ )
20	19 14	climresd	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ↔ 𝐹 ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) ) )
21	18 20	mpbid	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝐹 ⇝ ( ⇝ ‘ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ) )
22	14 15 21	breldmd	⊢ ( ( 𝜑 ∧ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) → 𝐹 ∈ dom ⇝ )
23	13 22	impbida	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑀 ) ) ∈ dom ⇝ ) )