This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupresuz2

Description: If the domain of a function is a subset of the integers, the superior limit doesn't change when the function is restricted to an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupresuz2.1	$⊢ φ \to M \in ℤ$
	limsupresuz2.2	$⊢ Z = ℤ_{\geq M}$
	limsupresuz2.3	$⊢ φ \to F \in V$
	limsupresuz2.4	$⊢ φ \to dom F \subseteq ℤ$
Assertion	limsupresuz2	$⊢ φ \to lim sup ({F ↾}_{Z}) = lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		limsupresuz2.1	$⊢ φ \to M \in ℤ$
2		limsupresuz2.2	$⊢ Z = ℤ_{\geq M}$
3		limsupresuz2.3	$⊢ φ \to F \in V$
4		limsupresuz2.4	$⊢ φ \to dom F \subseteq ℤ$
5		dmresss	$⊢ dom ({F ↾}_{ℝ}) \subseteq dom F$
6	5	a1i	$⊢ φ \to dom ({F ↾}_{ℝ}) \subseteq dom F$
7	6 4	sstrd	$⊢ φ \to dom ({F ↾}_{ℝ}) \subseteq ℤ$
8	1 2 3 7	limsupresuz	$⊢ φ \to lim sup ({F ↾}_{Z}) = lim sup (F)$