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 N Pred < N = 1 N 1

Proof

Step Hyp Ref Expression
1 nnuz = 1
2 predeq2 = 1 Pred < N = Pred < 1 N
3 1 2 ax-mp Pred < N = Pred < 1 N
4 elnnuz N N 1
5 preduz N 1 Pred < 1 N = 1 N 1
6 4 5 sylbi N Pred < 1 N = 1 N 1
7 3 6 eqtrid N Pred < N = 1 N 1