Metamath Proof Explorer


Theorem prednn

Description: The value of the predecessor class over the naturals. (Contributed by Scott Fenton, 6-Aug-2013)

Ref Expression
Assertion prednn ( 𝑁 ∈ ℕ → Pred ( < , ℕ , 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 nnuz ℕ = ( ℤ ‘ 1 )
2 predeq2 ( ℕ = ( ℤ ‘ 1 ) → Pred ( < , ℕ , 𝑁 ) = Pred ( < , ( ℤ ‘ 1 ) , 𝑁 ) )
3 1 2 ax-mp Pred ( < , ℕ , 𝑁 ) = Pred ( < , ( ℤ ‘ 1 ) , 𝑁 )
4 elnnuz ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ ‘ 1 ) )
5 preduz ( 𝑁 ∈ ( ℤ ‘ 1 ) → Pred ( < , ( ℤ ‘ 1 ) , 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
6 4 5 sylbi ( 𝑁 ∈ ℕ → Pred ( < , ( ℤ ‘ 1 ) , 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )
7 3 6 eqtrid ( 𝑁 ∈ ℕ → Pred ( < , ℕ , 𝑁 ) = ( 1 ... ( 𝑁 − 1 ) ) )