Theorem prinfzo0

Description: The intersection of a half-open integer range and the pair of its outer left borders is empty. (Contributed by AV, 9-Jan-2021)

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

Proof

Step	Hyp	Ref	Expression
1		elfz3	|- ( M e. ZZ -> M e. ( M ... M ) )
2		fznuz	|- ( M e. ( M ... M ) -> -. M e. ( ZZ>= ` ( M + 1 ) ) )
3	1 2	syl	|- ( M e. ZZ -> -. M e. ( ZZ>= ` ( M + 1 ) ) )
4	3	3mix1d	|- ( M e. ZZ -> ( -. M e. ( ZZ>= ` ( M + 1 ) ) \/ -. N e. ZZ \/ -. M < N ) )
5		3ianor	|- ( -. ( M e. ( ZZ>= ` ( M + 1 ) ) /\ N e. ZZ /\ M < N ) <-> ( -. M e. ( ZZ>= ` ( M + 1 ) ) \/ -. N e. ZZ \/ -. M < N ) )
6		elfzo2	|- ( M e. ( ( M + 1 ) ..^ N ) <-> ( M e. ( ZZ>= ` ( M + 1 ) ) /\ N e. ZZ /\ M < N ) )
7	5 6	xchnxbir	|- ( -. M e. ( ( M + 1 ) ..^ N ) <-> ( -. M e. ( ZZ>= ` ( M + 1 ) ) \/ -. N e. ZZ \/ -. M < N ) )
8	4 7	sylibr	|- ( M e. ZZ -> -. M e. ( ( M + 1 ) ..^ N ) )
9		incom	|- ( { M } i^i ( ( M + 1 ) ..^ N ) ) = ( ( ( M + 1 ) ..^ N ) i^i { M } )
10	9	eqeq1i	|- ( ( { M } i^i ( ( M + 1 ) ..^ N ) ) = (/) <-> ( ( ( M + 1 ) ..^ N ) i^i { M } ) = (/) )
11		disjsn	|- ( ( ( ( M + 1 ) ..^ N ) i^i { M } ) = (/) <-> -. M e. ( ( M + 1 ) ..^ N ) )
12	10 11	bitri	|- ( ( { M } i^i ( ( M + 1 ) ..^ N ) ) = (/) <-> -. M e. ( ( M + 1 ) ..^ N ) )
13	8 12	sylibr	|- ( M e. ZZ -> ( { M } i^i ( ( M + 1 ) ..^ N ) ) = (/) )
14		fzonel	|- -. N e. ( ( M + 1 ) ..^ N )
15	14	a1i	|- ( M e. ZZ -> -. N e. ( ( M + 1 ) ..^ N ) )
16		incom	|- ( { N } i^i ( ( M + 1 ) ..^ N ) ) = ( ( ( M + 1 ) ..^ N ) i^i { N } )
17	16	eqeq1i	|- ( ( { N } i^i ( ( M + 1 ) ..^ N ) ) = (/) <-> ( ( ( M + 1 ) ..^ N ) i^i { N } ) = (/) )
18		disjsn	|- ( ( ( ( M + 1 ) ..^ N ) i^i { N } ) = (/) <-> -. N e. ( ( M + 1 ) ..^ N ) )
19	17 18	bitri	|- ( ( { N } i^i ( ( M + 1 ) ..^ N ) ) = (/) <-> -. N e. ( ( M + 1 ) ..^ N ) )
20	15 19	sylibr	|- ( M e. ZZ -> ( { N } i^i ( ( M + 1 ) ..^ N ) ) = (/) )
21		df-pr	|- { M , N } = ( { M } u. { N } )
22	21	ineq1i	|- ( { M , N } i^i ( ( M + 1 ) ..^ N ) ) = ( ( { M } u. { N } ) i^i ( ( M + 1 ) ..^ N ) )
23	22	eqeq1i	|- ( ( { M , N } i^i ( ( M + 1 ) ..^ N ) ) = (/) <-> ( ( { M } u. { N } ) i^i ( ( M + 1 ) ..^ N ) ) = (/) )
24		undisj1	|- ( ( ( { M } i^i ( ( M + 1 ) ..^ N ) ) = (/) /\ ( { N } i^i ( ( M + 1 ) ..^ N ) ) = (/) ) <-> ( ( { M } u. { N } ) i^i ( ( M + 1 ) ..^ N ) ) = (/) )
25	23 24	bitr4i	|- ( ( { M , N } i^i ( ( M + 1 ) ..^ N ) ) = (/) <-> ( ( { M } i^i ( ( M + 1 ) ..^ N ) ) = (/) /\ ( { N } i^i ( ( M + 1 ) ..^ N ) ) = (/) ) )
26	13 20 25	sylanbrc	|- ( M e. ZZ -> ( { M , N } i^i ( ( M + 1 ) ..^ N ) ) = (/) )