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