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