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

Metamath Proof Explorer

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 ) ) )