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 elfzelz 
 |-  ( K e. ( M ... N ) -> K e. ZZ )
8 2 7 syl 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. ZZ )
9 8 zred 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. RR )
10 elfzolt2 
 |-  ( K e. ( M ..^ N ) -> K < N )
11 10 adantr 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K < N )
12 9 11 ltned 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K =/= N )
13 12 neneqd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> -. K = N )
14 6 13 olcnd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) )
15 simpr 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K =/= M )
16 15 neneqd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> -. K = M )
17 14 16 orcnd 
 |-  ( ( K e. ( M ..^ N ) /\ K =/= M ) -> K e. ( ( M + 1 ) ..^ N ) )