Metamath Proof Explorer

Theorem fzne1

Description: Elementhood in a finite set of sequential integers, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)

Ref Expression
Assertion fzne1 
|- ( ( K e. ( M ... N ) /\ K =/= M ) -> K e. ( ( M + 1 ) ... N ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( K =/= M <-> -. K = M )
2 elfzuz2 
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
3 elfzp12 
 |-  ( N e. ( ZZ>= ` M ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )
4 2 3 syl 
 |-  ( K e. ( M ... N ) -> ( K e. ( M ... N ) <-> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) ) )
5 4 ibi 
 |-  ( K e. ( M ... N ) -> ( K = M \/ K e. ( ( M + 1 ) ... N ) ) )
6 5 orcanai 
 |-  ( ( K e. ( M ... N ) /\ -. K = M ) -> K e. ( ( M + 1 ) ... N ) )
7 1 6 sylan2b 
 |-  ( ( K e. ( M ... N ) /\ K =/= M ) -> K e. ( ( M + 1 ) ... N ) )