Theorem fzp1disj

Description: ( M ... ( N + 1 ) ) is the disjoint union of ( M ... N ) with { ( N + 1 ) } . (Contributed by Mario Carneiro, 7-Mar-2014)

	Ref	Expression
Assertion	fzp1disj	|- ( ( M ... N ) i^i { ( N + 1 ) } ) = (/)

Proof

Step	Hyp	Ref	Expression
1		elfzle2	|- ( ( N + 1 ) e. ( M ... N ) -> ( N + 1 ) <_ N )
2		elfzel2	|- ( ( N + 1 ) e. ( M ... N ) -> N e. ZZ )
3	2	zred	|- ( ( N + 1 ) e. ( M ... N ) -> N e. RR )
4		ltp1	|- ( N e. RR -> N < ( N + 1 ) )
5		peano2re	|- ( N e. RR -> ( N + 1 ) e. RR )
6		ltnle	|- ( ( N e. RR /\ ( N + 1 ) e. RR ) -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
7	5 6	mpdan	|- ( N e. RR -> ( N < ( N + 1 ) <-> -. ( N + 1 ) <_ N ) )
8	4 7	mpbid	|- ( N e. RR -> -. ( N + 1 ) <_ N )
9	3 8	syl	|- ( ( N + 1 ) e. ( M ... N ) -> -. ( N + 1 ) <_ N )
10	1 9	pm2.65i	|- -. ( N + 1 ) e. ( M ... N )
11		disjsn	|- ( ( ( M ... N ) i^i { ( N + 1 ) } ) = (/) <-> -. ( N + 1 ) e. ( M ... N ) )
12	10 11	mpbir	|- ( ( M ... N ) i^i { ( N + 1 ) } ) = (/)