Metamath Proof Explorer


Theorem ige3m2fz

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

Proof

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