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 ) ) ∪ ( ℤ𝑁 ) ) )