Metamath Proof Explorer

Theorem fzone1

Description: Elementhood in a half-open interval, except its lower bound. (Contributed by Thierry Arnoux, 1-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 elfzofz 
 |-  ( K e. ( M ..^ N ) -> K e. ( M ... N ) )
2 1 adantr 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. ( M ... N ) )
3 elfzlmr 
 |-  ( K e. ( M ... N ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) )
4 2 3 syl 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) )
5 df-3or 
 |-  ( ( K = M \/ K e. ( ( M + 1 ) ..^ N ) \/ K = N ) <-> ( ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) \/ K = N ) )
6 4 5 sylib 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) \/ K = N ) )
7 2 elfzelzd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. ZZ )
8 7 zred 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. RR )
9 elfzolt2 
 |-  ( K e. ( M ..^ N ) -> K < N )
10 9 adantr 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K < N )
11 8 10 ltned 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K =/= N )
12 11 neneqd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> -. K = N )
13 6 12 olcnd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) )
14 simpr 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K =/= M )
15 14 neneqd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> -. K = M )
16 13 15 orcnd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. ( ( M + 1 ) ..^ N ) )