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