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	$⊢ φ \to M \in ℤ$
	climresdm.2	$⊢ φ \to F \in V$
Assertion	climresdm	$⊢ φ \to (F \in dom ⇝ \leftrightarrow {F ↾}_{ℤ_{\geq M}} \in dom ⇝)$

Proof

Step	Hyp	Ref	Expression
1		climresdm.1	$⊢ φ \to M \in ℤ$
2		climresdm.2	$⊢ φ \to F \in V$
3		resexg	$⊢ F \in dom ⇝ \to {F ↾}_{ℤ_{\geq M}} \in V$
4	3	adantl	$⊢ (φ \land F \in dom ⇝) \to {F ↾}_{ℤ_{\geq M}} \in V$
5		fvexd	$⊢ (φ \land F \in dom ⇝) \to ⇝ (F) \in V$
6		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
7	6	bilani	$⊢ (φ \land F \in dom ⇝) \to F ⇝ ⇝ (F)$
8	1	adantr	$⊢ (φ \land F \in dom ⇝) \to M \in ℤ$
9		simpr	$⊢ (φ \land F \in dom ⇝) \to F \in dom ⇝$
10	8 9	climresd	$⊢ (φ \land F \in dom ⇝) \to (({F ↾}_{ℤ_{\geq M}}) ⇝ ⇝ (F) \leftrightarrow F ⇝ ⇝ (F))$
11	7 10	mpbird	$⊢ (φ \land F \in dom ⇝) \to ({F ↾}_{ℤ_{\geq M}}) ⇝ ⇝ (F)$
12	4 5 11	breldmd	$⊢ (φ \land F \in dom ⇝) \to {F ↾}_{ℤ_{\geq M}} \in dom ⇝$
13	2	adantr	$⊢ (φ \land {F ↾}_{ℤ_{\geq M}} \in dom ⇝) \to F \in V$
14		fvexd	$⊢ (φ \land {F ↾}_{ℤ_{\geq M}} \in dom ⇝) \to ⇝ ({F ↾}_{ℤ_{\geq M}}) \in V$
15		climdm	$⊢ {F ↾}_{ℤ_{\geq M}} \in dom ⇝ \leftrightarrow ({F ↾}_{ℤ_{\geq M}}) ⇝ ⇝ ({F ↾}_{ℤ_{\geq M}})$
16	15	bilani	$⊢ (φ \land {F ↾}_{ℤ_{\geq M}} \in dom ⇝) \to ({F ↾}_{ℤ_{\geq M}}) ⇝ ⇝ ({F ↾}_{ℤ_{\geq M}})$
17	1	adantr	$⊢ (φ \land {F ↾}_{ℤ_{\geq M}} \in dom ⇝) \to M \in ℤ$
18	17 13	climresd	$⊢ (φ \land {F ↾}_{ℤ_{\geq M}} \in dom ⇝) \to (({F ↾}_{ℤ_{\geq M}}) ⇝ ⇝ ({F ↾}_{ℤ_{\geq M}}) \leftrightarrow F ⇝ ⇝ ({F ↾}_{ℤ_{\geq M}}))$
19	16 18	mpbid	$⊢ (φ \land {F ↾}_{ℤ_{\geq M}} \in dom ⇝) \to F ⇝ ⇝ ({F ↾}_{ℤ_{\geq M}})$
20	13 14 19	breldmd	$⊢ (φ \land {F ↾}_{ℤ_{\geq M}} \in dom ⇝) \to F \in dom ⇝$
21	12 20	impbida	$⊢ φ \to (F \in dom ⇝ \leftrightarrow {F ↾}_{ℤ_{\geq M}} \in dom ⇝)$

Metamath Proof Explorer

Theorem climresdm

Proof