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 nnge1 ⊢ ( 𝐴 ∈ ℕ → 1 ≤ 𝐴 )
3 2 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 1 ≤ 𝐴 )
4 simprr ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ≤ 𝐵 )
5 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
6 5 adantr ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ∈ ℤ )
7 1zzd ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 1 ∈ ℤ )
8 nn0z ⊢ ( 𝐵 ∈ ℕ0 → 𝐵 ∈ ℤ )
9 8 ad2antrl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐵 ∈ ℤ )
10 elfz ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∈ ( 1 ... 𝐵 ) ↔ ( 1 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
11 6 7 9 10 syl3anc ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 ∈ ( 1 ... 𝐵 ) ↔ ( 1 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
12 3 4 11 mpbir2and ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐴 ∈ ( 1 ... 𝐵 ) )
13 fzsplit ⊢ ( 𝐴 ∈ ( 1 ... 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
14 12 13 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
15 uncom ⊢ ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) = ( ( ( 𝐴 + 1 ) ... 𝐵 ) ∪ ( 1 ... 𝐴 ) )
16 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 + 1 ) = ( 0 + 1 ) )
17 16 adantr ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 + 1 ) = ( 0 + 1 ) )
18 0p1e1 ⊢ ( 0 + 1 ) = 1
19 17 18 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 𝐴 + 1 ) = 1 )
20 19 oveq1d ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( ( 𝐴 + 1 ) ... 𝐵 ) = ( 1 ... 𝐵 ) )
21 oveq2 ⊢ ( 𝐴 = 0 → ( 1 ... 𝐴 ) = ( 1 ... 0 ) )
22 21 adantr ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐴 ) = ( 1 ... 0 ) )
23 fz10 ⊢ ( 1 ... 0 ) = ∅
24 22 23 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐴 ) = ∅ )
25 20 24 uneq12d ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( ( ( 𝐴 + 1 ) ... 𝐵 ) ∪ ( 1 ... 𝐴 ) ) = ( ( 1 ... 𝐵 ) ∪ ∅ ) )
26 un0 ⊢ ( ( 1 ... 𝐵 ) ∪ ∅ ) = ( 1 ... 𝐵 )
27 25 26 eqtrdi ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( ( ( 𝐴 + 1 ) ... 𝐵 ) ∪ ( 1 ... 𝐴 ) ) = ( 1 ... 𝐵 ) )
28 15 27 syl5req ⊢ ( ( 𝐴 = 0 ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
29 14 28 jaoian ⊢ ( ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) ∧ ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )
30 29 ex ⊢ ( ( 𝐴 ∈ ℕ ∨ 𝐴 = 0 ) → ( ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) ) )
31 1 30 sylbi ⊢ ( 𝐴 ∈ ℕ0 → ( ( 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) ) )
32 31 3impib ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝐴 ≤ 𝐵 ) → ( 1 ... 𝐵 ) = ( ( 1 ... 𝐴 ) ∪ ( ( 𝐴 + 1 ) ... 𝐵 ) ) )