Metamath Proof Explorer


Theorem uzsubsubfz1

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

Ref Expression
Assertion uzsubsubfz1
|- ( ( L e. NN /\ N e. ( ZZ>= ` L ) ) -> ( N - ( L - 1 ) ) e. ( 1 ... N ) )

Proof

Step Hyp Ref Expression
1 elnnuz
 |-  ( L e. NN <-> L e. ( ZZ>= ` 1 ) )
2 uzsubsubfz
 |-  ( ( L e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` L ) ) -> ( N - ( L - 1 ) ) e. ( 1 ... N ) )
3 1 2 sylanb
 |-  ( ( L e. NN /\ N e. ( ZZ>= ` L ) ) -> ( N - ( L - 1 ) ) e. ( 1 ... N ) )