Metamath Proof Explorer


Theorem elfz1

Description: Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005)

Ref Expression
Assertion elfz1 M N K M N K M K K N

Proof

Step Hyp Ref Expression
1 fzval M N M N = j | M j j N
2 1 eleq2d M N K M N K j | M j j N
3 breq2 j = K M j M K
4 breq1 j = K j N K N
5 3 4 anbi12d j = K M j j N M K K N
6 5 elrab K j | M j j N K M K K N
7 3anass K M K K N K M K K N
8 6 7 bitr4i K j | M j j N K M K K N
9 2 8 bitrdi M N K M N K M K K N