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 
|- ( ( A e. NN0 /\ B e. NN0 /\ A <_ B ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( A e. NN0 <-> ( A e. NN \/ A = 0 ) )
2 1zzd 
 |-  ( ( A e. NN /\ ( B e. NN0 /\ A <_ B ) ) -> 1 e. ZZ )
3 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
4 3 ad2antrl 
 |-  ( ( A e. NN /\ ( B e. NN0 /\ A <_ B ) ) -> B e. ZZ )
5 nnz 
 |-  ( A e. NN -> A e. ZZ )
6 5 adantr 
 |-  ( ( A e. NN /\ ( B e. NN0 /\ A <_ B ) ) -> A e. ZZ )
7 nnge1 
 |-  ( A e. NN -> 1 <_ A )
8 7 adantr 
 |-  ( ( A e. NN /\ ( B e. NN0 /\ A <_ B ) ) -> 1 <_ A )
9 simprr 
 |-  ( ( A e. NN /\ ( B e. NN0 /\ A <_ B ) ) -> A <_ B )
10 2 4 6 8 9 elfzd 
 |-  ( ( A e. NN /\ ( B e. NN0 /\ A <_ B ) ) -> A e. ( 1 ... B ) )
11 fzsplit 
 |-  ( A e. ( 1 ... B ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )
12 10 11 syl 
 |-  ( ( A e. NN /\ ( B e. NN0 /\ A <_ B ) ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )
13 uncom 
 |-  ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) = ( ( ( A + 1 ) ... B ) u. ( 1 ... A ) )
14 oveq1 
 |-  ( A = 0 -> ( A + 1 ) = ( 0 + 1 ) )
15 14 adantr 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( A + 1 ) = ( 0 + 1 ) )
16 0p1e1 
 |-  ( 0 + 1 ) = 1
17 15 16 eqtrdi 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( A + 1 ) = 1 )
18 17 oveq1d 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( ( A + 1 ) ... B ) = ( 1 ... B ) )
19 oveq2 
 |-  ( A = 0 -> ( 1 ... A ) = ( 1 ... 0 ) )
20 19 adantr 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( 1 ... A ) = ( 1 ... 0 ) )
21 fz10 
 |-  ( 1 ... 0 ) = (/)
22 20 21 eqtrdi 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( 1 ... A ) = (/) )
23 18 22 uneq12d 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( ( ( A + 1 ) ... B ) u. ( 1 ... A ) ) = ( ( 1 ... B ) u. (/) ) )
24 un0 
 |-  ( ( 1 ... B ) u. (/) ) = ( 1 ... B )
25 23 24 eqtrdi 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( ( ( A + 1 ) ... B ) u. ( 1 ... A ) ) = ( 1 ... B ) )
26 13 25 eqtr2id 
 |-  ( ( A = 0 /\ ( B e. NN0 /\ A <_ B ) ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )
27 12 26 jaoian 
 |-  ( ( ( A e. NN \/ A = 0 ) /\ ( B e. NN0 /\ A <_ B ) ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )
28 27 ex 
 |-  ( ( A e. NN \/ A = 0 ) -> ( ( B e. NN0 /\ A <_ B ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) ) )
29 1 28 sylbi 
 |-  ( A e. NN0 -> ( ( B e. NN0 /\ A <_ B ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) ) )
30 29 3impib 
 |-  ( ( A e. NN0 /\ B e. NN0 /\ A <_ B ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )