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

Metamath Proof Explorer

Theorem uzsubfz0

Description: Membership of an integer greater than L decreased by L in a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 16-Sep-2018)

Ref Expression
Assertion uzsubfz0 
|- ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> ( N - L ) e. ( 0 ... N ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> L e. NN0 )
2 eluznn0 
 |-  ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> N e. NN0 )
3 eluzle 
 |-  ( N e. ( ZZ>= ` L ) -> L <_ N )
4 3 adantl 
 |-  ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> L <_ N )
5 elfz2nn0 
 |-  ( L e. ( 0 ... N ) <-> ( L e. NN0 /\ N e. NN0 /\ L <_ N ) )
6 1 2 4 5 syl3anbrc 
 |-  ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> L e. ( 0 ... N ) )
7 fznn0sub2 
 |-  ( L e. ( 0 ... N ) -> ( N - L ) e. ( 0 ... N ) )
8 6 7 syl 
 |-  ( ( L e. NN0 /\ N e. ( ZZ>= ` L ) ) -> ( N - L ) e. ( 0 ... N ) )