This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzpreddisj

Description: A finite set of sequential integers is disjoint with its predecessor. (Contributed by AV, 24-Aug-2019)

Ref Expression
Assertion fzpreddisj 
|- ( N e. ( ZZ>= ` M ) -> ( { M } i^i ( ( M + 1 ) ... N ) ) = (/) )

Proof

Step Hyp Ref Expression
1 incom 
 |-  ( { M } i^i ( ( M + 1 ) ... N ) ) = ( ( ( M + 1 ) ... N ) i^i { M } )
2 0lt1 
 |-  0 < 1
3 0re 
 |-  0 e. RR
4 1re 
 |-  1 e. RR
5 3 4 ltnlei 
 |-  ( 0 < 1 <-> -. 1 <_ 0 )
6 2 5 mpbi 
 |-  -. 1 <_ 0
7 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
8 7 zred 
 |-  ( N e. ( ZZ>= ` M ) -> M e. RR )
9 leaddle0 
 |-  ( ( M e. RR /\ 1 e. RR ) -> ( ( M + 1 ) <_ M <-> 1 <_ 0 ) )
10 8 4 9 sylancl 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( M + 1 ) <_ M <-> 1 <_ 0 ) )
11 6 10 mtbiri 
 |-  ( N e. ( ZZ>= ` M ) -> -. ( M + 1 ) <_ M )
12 11 intnanrd 
 |-  ( N e. ( ZZ>= ` M ) -> -. ( ( M + 1 ) <_ M /\ M <_ N ) )
13 12 intnand 
 |-  ( N e. ( ZZ>= ` M ) -> -. ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( ( M + 1 ) <_ M /\ M <_ N ) ) )
14 elfz2 
 |-  ( M e. ( ( M + 1 ) ... N ) <-> ( ( ( M + 1 ) e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( ( M + 1 ) <_ M /\ M <_ N ) ) )
15 13 14 sylnibr 
 |-  ( N e. ( ZZ>= ` M ) -> -. M e. ( ( M + 1 ) ... N ) )
16 disjsn 
 |-  ( ( ( ( M + 1 ) ... N ) i^i { M } ) = (/) <-> -. M e. ( ( M + 1 ) ... N ) )
17 15 16 sylibr 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ( M + 1 ) ... N ) i^i { M } ) = (/) )
18 1 17 eqtrid 
 |-  ( N e. ( ZZ>= ` M ) -> ( { M } i^i ( ( M + 1 ) ... N ) ) = (/) )