Theorem 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 e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( I + N ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzoel2	|- ( Z e. ( M ..^ N ) -> N e. ZZ )
2		nn0pzuz	|- ( ( I e. NN0 /\ N e. ZZ ) -> ( I + N ) e. ( ZZ>= ` N ) )
3	1 2	sylan2	|- ( ( I e. NN0 /\ Z e. ( M ..^ N ) ) -> ( I + N ) e. ( ZZ>= ` N ) )
4		fzoss2	|- ( ( I + N ) e. ( ZZ>= ` N ) -> ( M ..^ N ) C_ ( M ..^ ( I + N ) ) )
5	3 4	syl	|- ( ( I e. NN0 /\ Z e. ( M ..^ N ) ) -> ( M ..^ N ) C_ ( M ..^ ( I + N ) ) )
6	5	sseld	|- ( ( I e. NN0 /\ Z e. ( M ..^ N ) ) -> ( Z e. ( M ..^ N ) -> Z e. ( M ..^ ( I + N ) ) ) )
7	6	syldbl2	|- ( ( I e. NN0 /\ Z e. ( M ..^ N ) ) -> Z e. ( M ..^ ( I + N ) ) )
8	7	ancoms	|- ( ( Z e. ( M ..^ N ) /\ I e. NN0 ) -> Z e. ( M ..^ ( I + N ) ) )