This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Order sets Finite intervals of integers 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 ⊢ ( ( 𝐿 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 1 ) ) ∈ ( 1 ... 𝑁 ) )
Proof
Step
Hyp
Ref
Expression
1
elnnuz ⊢ ( 𝐿 ∈ ℕ ↔ 𝐿 ∈ ( ℤ≥ ‘ 1 ) )
2
uzsubsubfz ⊢ ( ( 𝐿 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 1 ) ) ∈ ( 1 ... 𝑁 ) )
3
1 2
sylanb ⊢ ( ( 𝐿 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐿 ) ) → ( 𝑁 − ( 𝐿 − 1 ) ) ∈ ( 1 ... 𝑁 ) )