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

Metamath Proof Explorer

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