Metamath Proof Explorer

Theorem fzsplit1nn0

Description: Split a finite 1-based set of integers in the middle, allowing either end to be empty ( ( 1 ... 0 ) ). (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion fzsplit1nn0 ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝐴 ∈ ℕ0 ↔ ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) )
2 1zzd ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 1 ∈ ℤ )
3 nn0z ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℤ )
4 3 ad2antrl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐵 ∈ ℤ )
5 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ∈ ℤ )
7 nnge1 ⊢ ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )
8 7 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 1 ≤ 𝐴 )
9 simprr ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ≤ 𝐵 )
10 2 4 6 8 9 elfzd ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ∈ ( 1 ... 𝐵 ) )
11 fzsplit ⊢ ( 𝐴 ∈ ( 1 ... 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
12 10 11 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
13 uncom ⊢ ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( ( ( 𝐴 + 1 ) ... 𝐵 ) ∪ ( 1 ... 𝐴 ) )
14 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 + 1 ) = ( 0 + 1 ) )
15 14 adantr ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 + 1 ) = ( 0 + 1 ) )
16 0p1e1 ⊢ ( 0 + 1 ) = 1
17 15 16 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 + 1 ) = 1 )
18 17 oveq1d ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( ( 𝐴 + 1 ) ... 𝐵 ) = ( 1 ... 𝐵 ) )
19 oveq2 ⊢ ( 𝐴 = 0 → ( 1 ... 𝐴 ) = ( 1 ... 0 ) )
20 19 adantr ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐴 ) = ( 1 ... 0 ) )
21 fz10 ⊢ ( 1 ... 0 ) = ∅
22 20 21 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐴 ) = ∅ )
23 18 22 uneq12d ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( ( ( 𝐴 + 1 ) ... 𝐵 ) ∪ ( 1 ... 𝐴 ) ) = ( ( 1 ... 𝐵 ) ∪ ∅ ) )
24 un0 ⊢ ( ( 1 ... 𝐵 ) ∪ ∅ ) = ( 1 ... 𝐵 )
25 23 24 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( ( ( 𝐴 + 1 ) ... 𝐵 ) ∪ ( 1 ... 𝐴 ) ) = ( 1 ... 𝐵 ) )
26 13 25 eqtr2id ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
27 12 26 jaoian ⊢ ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
28 27 ex ⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → ( ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) ) )
29 1 28 sylbi ⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) ) )
30 29 3impib ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )