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

Metamath Proof Explorer

Theorem uzsplit

Description: Express an upper integer set as the disjoint (see uzdisj ) union of the first N values and the rest. (Contributed by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion uzsplit ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑀 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 eluzelre ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℝ )
2 eluzelre ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℝ )
3 lelttric ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑁 ≤ 𝑘 ∨ 𝑘 < 𝑁 ) )
4 1 2 3 syl2an ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑁 ≤ 𝑘 ∨ 𝑘 < 𝑁 ) )
5 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
6 eluzelz ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑘 ∈ ℤ )
7 eluz ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑘 ) )
8 5 6 7 syl2an ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ 𝑁 ≤ 𝑘 ) )
9 eluzle ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ≤ 𝑘 )
10 6 9 jca ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) )
11 10 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) )
12 eluzel2 ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
13 elfzm11 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < 𝑁 ) ) )
14 df-3an ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ∧ 𝑘 < 𝑁 ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑘 < 𝑁 ) )
15 13 14 bitrdi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑘 < 𝑁 ) ) )
16 12 5 15 syl2anr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ ( ( 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘 ) ∧ 𝑘 < 𝑁 ) ) )
17 11 16 mpbirand ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ 𝑘 < 𝑁 ) )
18 8 17 orbi12d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∨ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) ↔ ( 𝑁 ≤ 𝑘 ∨ 𝑘 < 𝑁 ) ) )
19 4 18 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∨ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) )
20 19 orcomd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
21 20 ex ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) )
22 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
23 22 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
24 uztrn ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
25 24 expcom ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
26 23 25 jaod ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) )
27 21 26 impbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) ) )
28 elun ⊢ ( 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ↔ ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
29 27 28 bitr4di ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ↔ 𝑘 ∈ ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) ) )
30 29 eqrdv ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑀 ) = ( ( 𝑀 ... ( 𝑁 − 1 ) ) ∪ ( ℤ≥ ‘ 𝑁 ) ) )