elfzoextl

Description: Membership of an integer in an extended open range of integers, extension added to the left. (Contributed by AV, 31-Aug-2025) Generalized by replacing the left border of the ranges. (Revised by SN, 18-Sep-2025)

		Ref	Expression
	Assertion	elfzoextl	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z \in (M ..^I + N)$

Proof

Step	Hyp	Ref	Expression
1		elfzoel2	$⊢ Z \in (M ..^N) \to N \in ℤ$
2		nn0pzuz	$⊢ (I \in ℕ_{0} \land N \in ℤ) \to I + N \in ℤ_{\geq N}$
3	1 2	sylan2	$⊢ (I \in ℕ_{0} \land Z \in (M ..^N)) \to I + N \in ℤ_{\geq N}$
4		fzoss2	$⊢ I + N \in ℤ_{\geq N} \to (M ..^N) \subseteq (M ..^I + N)$
5	3 4	syl	$⊢ (I \in ℕ_{0} \land Z \in (M ..^N)) \to (M ..^N) \subseteq (M ..^I + N)$
6	5	sseld	$⊢ (I \in ℕ_{0} \land Z \in (M ..^N)) \to (Z \in (M ..^N) \to Z \in (M ..^I + N))$
7	6	syldbl2	$⊢ (I \in ℕ_{0} \land Z \in (M ..^N)) \to Z \in (M ..^I + N)$
8	7	ancoms	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z \in (M ..^I + N)$

Metamath Proof Explorer

Theorem elfzoextl

Proof