Metamath Proof Explorer

Theorem elfzelzd

Description: A member of a finite set of sequential integer is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypothesis elfzelzd.1 φ K M N
Assertion elfzelzd φ K


Step Hyp Ref Expression
1 elfzelzd.1 φ K M N
2 elfzelz K M N K
3 1 2 syl φ K