Metamath Proof Explorer

Theorem uzin

Description: Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013)

Ref Expression
Assertion uzin 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` if ( M <_ N , N , M ) ) )

Proof

Step Hyp Ref Expression
1 uztric 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) )
2 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
3 sseqin2 
 |-  ( ( ZZ>= ` N ) C_ ( ZZ>= ` M ) <-> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` N ) )
4 2 3 sylib 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` N ) )
5 eluzle 
 |-  ( N e. ( ZZ>= ` M ) -> M <_ N )
6 iftrue 
 |-  ( M <_ N -> if ( M <_ N , N , M ) = N )
7 5 6 syl 
 |-  ( N e. ( ZZ>= ` M ) -> if ( M <_ N , N , M ) = N )
8 7 fveq2d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` if ( M <_ N , N , M ) ) = ( ZZ>= ` N ) )
9 4 8 eqtr4d 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` if ( M <_ N , N , M ) ) )
10 uzss 
 |-  ( M e. ( ZZ>= ` N ) -> ( ZZ>= ` M ) C_ ( ZZ>= ` N ) )
11 df-ss 
 |-  ( ( ZZ>= ` M ) C_ ( ZZ>= ` N ) <-> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` M ) )
12 10 11 sylib 
 |-  ( M e. ( ZZ>= ` N ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` M ) )
13 eluzle 
 |-  ( M e. ( ZZ>= ` N ) -> N <_ M )
14 eluzel2 
 |-  ( M e. ( ZZ>= ` N ) -> N e. ZZ )
15 eluzelz 
 |-  ( M e. ( ZZ>= ` N ) -> M e. ZZ )
16 zre 
 |-  ( N e. ZZ -> N e. RR )
17 zre 
 |-  ( M e. ZZ -> M e. RR )
18 letri3 
 |-  ( ( N e. RR /\ M e. RR ) -> ( N = M <-> ( N <_ M /\ M <_ N ) ) )
19 16 17 18 syl2an 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N = M <-> ( N <_ M /\ M <_ N ) ) )
20 14 15 19 syl2anc 
 |-  ( M e. ( ZZ>= ` N ) -> ( N = M <-> ( N <_ M /\ M <_ N ) ) )
21 13 20 mpbirand 
 |-  ( M e. ( ZZ>= ` N ) -> ( N = M <-> M <_ N ) )
22 21 biimprcd 
 |-  ( M <_ N -> ( M e. ( ZZ>= ` N ) -> N = M ) )
23 6 eqeq1d 
 |-  ( M <_ N -> ( if ( M <_ N , N , M ) = M <-> N = M ) )
24 22 23 sylibrd 
 |-  ( M <_ N -> ( M e. ( ZZ>= ` N ) -> if ( M <_ N , N , M ) = M ) )
25 24 com12 
 |-  ( M e. ( ZZ>= ` N ) -> ( M <_ N -> if ( M <_ N , N , M ) = M ) )
26 iffalse 
 |-  ( -. M <_ N -> if ( M <_ N , N , M ) = M )
27 25 26 pm2.61d1 
 |-  ( M e. ( ZZ>= ` N ) -> if ( M <_ N , N , M ) = M )
28 27 fveq2d 
 |-  ( M e. ( ZZ>= ` N ) -> ( ZZ>= ` if ( M <_ N , N , M ) ) = ( ZZ>= ` M ) )
29 12 28 eqtr4d 
 |-  ( M e. ( ZZ>= ` N ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` if ( M <_ N , N , M ) ) )
30 9 29 jaoi 
 |-  ( ( N e. ( ZZ>= ` M ) \/ M e. ( ZZ>= ` N ) ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` if ( M <_ N , N , M ) ) )
31 1 30 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ZZ>= ` M ) i^i ( ZZ>= ` N ) ) = ( ZZ>= ` if ( M <_ N , N , M ) ) )