Metamath Proof Explorer

Theorem uzin

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

Ref Expression
Assertion uzin ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 uztric ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
2 uzss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
3 sseqin2 ⊢ ( ( ℤ≥ ‘ 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) ↔ ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ 𝑁 ) )
4 2 3 sylib ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ 𝑁 ) )
5 eluzle ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑁 )
6 iftrue ⊢ ( 𝑀 ≤ 𝑁 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = 𝑁 )
7 5 6 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = 𝑁 )
8 7 fveq2d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) = ( ℤ≥ ‘ 𝑁 ) )
9 4 8 eqtr4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
10 uzss ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 𝑁 ) )
11 dfss2 ⊢ ( ( ℤ≥ ‘ 𝑀 ) ⊆ ( ℤ≥ ‘ 𝑁 ) ↔ ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ 𝑀 ) )
12 10 11 sylib ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ 𝑀 ) )
13 eluzle ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑀 )
14 eluzel2 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ℤ )
15 eluzelz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑀 ∈ ℤ )
16 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
17 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
18 letri3 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 = 𝑀 ↔ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
19 16 17 18 syl2an ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 = 𝑀 ↔ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
20 14 15 19 syl2anc ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 = 𝑀 ↔ ( 𝑁 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁 ) ) )
21 13 20 mpbirand ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑁 = 𝑀 ↔ 𝑀 ≤ 𝑁 ) )
22 21 biimprcd ⊢ ( 𝑀 ≤ 𝑁 → ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 = 𝑀 ) )
23 6 eqeq1d ⊢ ( 𝑀 ≤ 𝑁 → ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = 𝑀 ↔ 𝑁 = 𝑀 ) )
24 22 23 sylibrd ⊢ ( 𝑀 ≤ 𝑁 → ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = 𝑀 ) )
25 24 com12 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 𝑀 ≤ 𝑁 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = 𝑀 ) )
26 iffalse ⊢ ( ¬ 𝑀 ≤ 𝑁 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = 𝑀 )
27 25 26 pm2.61d1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) = 𝑀 )
28 27 fveq2d ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ℤ≥ ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) = ( ℤ≥ ‘ 𝑀 ) )
29 12 28 eqtr4d ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
30 9 29 jaoi ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∨ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
31 1 30 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ℤ≥ ‘ 𝑀 ) ∩ ( ℤ≥ ‘ 𝑁 ) ) = ( ℤ≥ ‘ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )