Metamath Proof Explorer

Theorem elfzoext

Description: Membership of an integer in an extended open range of integers, extension added to the right. (Contributed by AV, 30-Apr-2020) (Proof shortened by AV, 23-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		elfzoextl	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z \in (M ..^I + N)$
2		elfzoel2	$⊢ Z \in (M ..^N) \to N \in ℤ$
3	2	zcnd	$⊢ Z \in (M ..^N) \to N \in ℂ$
4	3	adantr	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to N \in ℂ$
5		nn0cn	$⊢ I \in ℕ_{0} \to I \in ℂ$
6	5	adantl	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to I \in ℂ$
7	4 6	addcomd	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to N + I = I + N$
8	7	oveq2d	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to (M ..^N + I) = (M ..^I + N)$
9	1 8	eleqtrrd	$⊢ (Z \in (M ..^N) \land I \in ℕ_{0}) \to Z \in (M ..^N + I)$