Metamath Proof Explorer


Theorem elfzelzd

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

Ref Expression
Hypothesis elfzelzd.1 φKMN
Assertion elfzelzd φK

Proof

Step Hyp Ref Expression
1 elfzelzd.1 φKMN
2 elfzelz KMNK
3 1 2 syl φK