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 ( 𝑀 ∈ ℤ → ( { 𝑀 , 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 elfz3 ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( 𝑀 ... 𝑀 ) )
2 fznuz ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑀 ) → ¬ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
3 1 2 syl ⊢ ( 𝑀 ∈ ℤ → ¬ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
4 3 3mix1d ⊢ ( 𝑀 ∈ ℤ → ( ¬ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∨ ¬ 𝑁 ∈ ℤ ∨ ¬ 𝑀 < 𝑁 ) )
5 3ianor ⊢ ( ¬ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ↔ ( ¬ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∨ ¬ 𝑁 ∈ ℤ ∨ ¬ 𝑀 < 𝑁 ) )
6 elfzo2 ⊢ ( 𝑀 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ↔ ( 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) )
7 5 6 xchnxbir ⊢ ( ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ↔ ( ¬ 𝑀 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ∨ ¬ 𝑁 ∈ ℤ ∨ ¬ 𝑀 < 𝑁 ) )
8 4 7 sylibr ⊢ ( 𝑀 ∈ ℤ → ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
9 incom ⊢ ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ( ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∩ { 𝑀 } )
10 9 eqeq1i ⊢ ( ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ↔ ( ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∩ { 𝑀 } ) = ∅ )
11 disjsn ⊢ ( ( ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
12 10 11 bitri ⊢ ( ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ↔ ¬ 𝑀 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
13 8 12 sylibr ⊢ ( 𝑀 ∈ ℤ → ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ )
14 fzonel ⊢ ¬ 𝑁 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 )
15 14 a1i ⊢ ( 𝑀 ∈ ℤ → ¬ 𝑁 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
16 incom ⊢ ( { 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ( ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∩ { 𝑁 } )
17 16 eqeq1i ⊢ ( ( { 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ↔ ( ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ )
18 disjsn ⊢ ( ( ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∩ { 𝑁 } ) = ∅ ↔ ¬ 𝑁 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
19 17 18 bitri ⊢ ( ( { 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ↔ ¬ 𝑁 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
20 15 19 sylibr ⊢ ( 𝑀 ∈ ℤ → ( { 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ )
21 df-pr ⊢ { 𝑀 , 𝑁 } = ( { 𝑀 } ∪ { 𝑁 } )
22 21 ineq1i ⊢ ( { 𝑀 , 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ( ( { 𝑀 } ∪ { 𝑁 } ) ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) )
23 22 eqeq1i ⊢ ( ( { 𝑀 , 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ↔ ( ( { 𝑀 } ∪ { 𝑁 } ) ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ )
24 undisj1 ⊢ ( ( ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ∧ ( { 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ) ↔ ( ( { 𝑀 } ∪ { 𝑁 } ) ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ )
25 23 24 bitr4i ⊢ ( ( { 𝑀 , 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ↔ ( ( { 𝑀 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ∧ ( { 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ ) )
26 13 20 25 sylanbrc ⊢ ( 𝑀 ∈ ℤ → ( { 𝑀 , 𝑁 } ∩ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) = ∅ )