Description: Membership of an integer greater than 2 decreased by 2 in a 1-based finite set of sequential integers. (Contributed by Alexander van der Vekens, 14-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | ige3m2fz | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3m1e2 | ⊢ ( 3 − 1 ) = 2 | |
2 | 1 | eqcomi | ⊢ 2 = ( 3 − 1 ) |
3 | 2 | a1i | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 = ( 3 − 1 ) ) |
4 | 3 | oveq2d | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) = ( 𝑁 − ( 3 − 1 ) ) ) |
5 | 3nn | ⊢ 3 ∈ ℕ | |
6 | uzsubsubfz1 | ⊢ ( ( 3 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑁 − ( 3 − 1 ) ) ∈ ( 1 ... 𝑁 ) ) | |
7 | 5 6 | mpan | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − ( 3 − 1 ) ) ∈ ( 1 ... 𝑁 ) ) |
8 | 4 7 | eqeltrd | ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ( 1 ... 𝑁 ) ) |