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 ) ) = (/) )