Metamath Proof Explorer

Theorem elfzolborelfzop1

Description: An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a lower bound increased by 1. (Contributed by AV, 2-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 elfzo2 
 |-  ( K e. ( M ..^ N ) <-> ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) )
2 eluz2 
 |-  ( K e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ K e. ZZ /\ M <_ K ) )
3 zre 
 |-  ( M e. ZZ -> M e. RR )
4 zre 
 |-  ( K e. ZZ -> K e. RR )
5 leloe 
 |-  ( ( M e. RR /\ K e. RR ) -> ( M <_ K <-> ( M < K \/ M = K ) ) )
6 3 4 5 syl2an 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M <_ K <-> ( M < K \/ M = K ) ) )
7 peano2z 
 |-  ( M e. ZZ -> ( M + 1 ) e. ZZ )
8 7 adantr 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M + 1 ) e. ZZ )
9 8 ad2antrl 
 |-  ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) -> ( M + 1 ) e. ZZ )
10 simprlr 
 |-  ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) -> K e. ZZ )
11 simpl 
 |-  ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) -> M < K )
12 zltp1le 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M < K <-> ( M + 1 ) <_ K ) )
13 12 ad2antrl 
 |-  ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) -> ( M < K <-> ( M + 1 ) <_ K ) )
14 11 13 mpbid 
 |-  ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) -> ( M + 1 ) <_ K )
15 9 10 14 3jca 
 |-  ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) -> ( ( M + 1 ) e. ZZ /\ K e. ZZ /\ ( M + 1 ) <_ K ) )
16 15 adantr 
 |-  ( ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) /\ K < N ) -> ( ( M + 1 ) e. ZZ /\ K e. ZZ /\ ( M + 1 ) <_ K ) )
17 simplrr 
 |-  ( ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) /\ K < N ) -> N e. ZZ )
18 simpr 
 |-  ( ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) /\ K < N ) -> K < N )
19 elfzo2 
 |-  ( K e. ( ( M + 1 ) ..^ N ) <-> ( K e. ( ZZ>= ` ( M + 1 ) ) /\ N e. ZZ /\ K < N ) )
20 eluz2 
 |-  ( K e. ( ZZ>= ` ( M + 1 ) ) <-> ( ( M + 1 ) e. ZZ /\ K e. ZZ /\ ( M + 1 ) <_ K ) )
21 20 3anbi1i 
 |-  ( ( K e. ( ZZ>= ` ( M + 1 ) ) /\ N e. ZZ /\ K < N ) <-> ( ( ( M + 1 ) e. ZZ /\ K e. ZZ /\ ( M + 1 ) <_ K ) /\ N e. ZZ /\ K < N ) )
22 19 21 bitri 
 |-  ( K e. ( ( M + 1 ) ..^ N ) <-> ( ( ( M + 1 ) e. ZZ /\ K e. ZZ /\ ( M + 1 ) <_ K ) /\ N e. ZZ /\ K < N ) )
23 16 17 18 22 syl3anbrc 
 |-  ( ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) /\ K < N ) -> K e. ( ( M + 1 ) ..^ N ) )
24 23 olcd 
 |-  ( ( ( M < K /\ ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) ) /\ K < N ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) )
25 24 exp31 
 |-  ( M < K -> ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) )
26 orc 
 |-  ( K = M -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) )
27 26 eqcoms 
 |-  ( M = K -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) )
28 27 2a1d 
 |-  ( M = K -> ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) )
29 25 28 jaoi 
 |-  ( ( M < K \/ M = K ) -> ( ( ( M e. ZZ /\ K e. ZZ ) /\ N e. ZZ ) -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) )
30 29 expd 
 |-  ( ( M < K \/ M = K ) -> ( ( M e. ZZ /\ K e. ZZ ) -> ( N e. ZZ -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) ) )
31 30 com12 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( ( M < K \/ M = K ) -> ( N e. ZZ -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) ) )
32 6 31 sylbid 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M <_ K -> ( N e. ZZ -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) ) )
33 32 3impia 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ M <_ K ) -> ( N e. ZZ -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) )
34 2 33 sylbi 
 |-  ( K e. ( ZZ>= ` M ) -> ( N e. ZZ -> ( K < N -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) ) ) )
35 34 3imp 
 |-  ( ( K e. ( ZZ>= ` M ) /\ N e. ZZ /\ K < N ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) )
36 1 35 sylbi 
 |-  ( K e. ( M ..^ N ) -> ( K = M \/ K e. ( ( M + 1 ) ..^ N ) ) )