elfzoext

Description: Membership of an integer in an extended open range of integers. (Contributed by AV, 30-Apr-2020)

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

Step	Hyp	Ref	Expression
1		elfzoel2	$⊢ Z \in (M ..^N) \to N \in ℤ$
2		zcn	$⊢ N \in ℤ \to N \in ℂ$
3		nn0cn	$⊢ I \in ℕ_{0} \to I \in ℂ$
4		addcom	$⊢ (N \in ℂ \land I \in ℂ) \to N + I = I + N$
5	2 3 4	syl2an	$⊢ (N \in ℤ \land I \in ℕ_{0}) \to N + I = I + N$
6		nn0pzuz	$⊢ (I \in ℕ_{0} \land N \in ℤ) \to I + N \in ℤ_{\geq N}$
7	6	ancoms	$⊢ (N \in ℤ \land I \in ℕ_{0}) \to I + N \in ℤ_{\geq N}$
8	5 7	eqeltrd	$⊢ (N \in ℤ \land I \in ℕ_{0}) \to N + I \in ℤ_{\geq N}$
9		fzoss2	$⊢ N + I \in ℤ_{\geq N} \to (M ..^N) \subseteq (M ..^N + I)$
10	8 9	syl	$⊢ (N \in ℤ \land I \in ℕ_{0}) \to (M ..^N) \subseteq (M ..^N + I)$
11	10	sselda	$⊢ ((N \in ℤ \land I \in ℕ_{0}) \land Z \in (M ..^N)) \to Z \in (M ..^N + I)$
12	11	expcom	$⊢ Z \in (M ..^N) \to ((N \in ℤ \land I \in ℕ_{0}) \to Z \in (M ..^N + I))$
13	1 12	mpand	$⊢ Z \in (M ..^N) \to (I \in ℕ_{0} \to Z \in (M ..^N + I))$
14	13	imp	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z \in (M ..^N + I)$

Metamath Proof Explorer