Metamath Proof Explorer

Theorem fzsplitnd

Description: Split a finite interval of integers into two parts. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypothesis fzsplitnd.1 
|- ( ph -> K e. ( M ... N ) )
Assertion fzsplitnd 
|- ( ph -> ( M ... N ) = ( ( M ... ( K - 1 ) ) u. ( K ... N ) ) )

Proof

Step Hyp Ref Expression
1 fzsplitnd.1 
 |-  ( ph -> K e. ( M ... N ) )
2 elfzuz 
 |-  ( K e. ( M ... N ) -> K e. ( ZZ>= ` M ) )
3 1 2 syl 
 |-  ( ph -> K e. ( ZZ>= ` M ) )
4 1 elfzelzd 
 |-  ( ph -> K e. ZZ )
5 4 zcnd 
 |-  ( ph -> K e. CC )
6 1cnd 
 |-  ( ph -> 1 e. CC )
7 5 6 npcand 
 |-  ( ph -> ( ( K - 1 ) + 1 ) = K )
8 7 eleq1d 
 |-  ( ph -> ( ( ( K - 1 ) + 1 ) e. ( ZZ>= ` M ) <-> K e. ( ZZ>= ` M ) ) )
9 3 8 mpbird 
 |-  ( ph -> ( ( K - 1 ) + 1 ) e. ( ZZ>= ` M ) )
10 1zzd 
 |-  ( ph -> 1 e. ZZ )
11 4 10 zsubcld 
 |-  ( ph -> ( K - 1 ) e. ZZ )
12 elfzuz3 
 |-  ( K e. ( M ... N ) -> N e. ( ZZ>= ` K ) )
13 1 12 syl 
 |-  ( ph -> N e. ( ZZ>= ` K ) )
14 7 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( K - 1 ) + 1 ) ) = ( ZZ>= ` K ) )
15 14 eleq2d 
 |-  ( ph -> ( N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) <-> N e. ( ZZ>= ` K ) ) )
16 13 15 mpbird 
 |-  ( ph -> N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) )
17 peano2uzr 
 |-  ( ( ( K - 1 ) e. ZZ /\ N e. ( ZZ>= ` ( ( K - 1 ) + 1 ) ) ) -> N e. ( ZZ>= ` ( K - 1 ) ) )
18 11 16 17 syl2anc 
 |-  ( ph -> N e. ( ZZ>= ` ( K - 1 ) ) )
19 fzsplit2 
 |-  ( ( ( ( K - 1 ) + 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` ( K - 1 ) ) ) -> ( M ... N ) = ( ( M ... ( K - 1 ) ) u. ( ( ( K - 1 ) + 1 ) ... N ) ) )
20 9 18 19 syl2anc 
 |-  ( ph -> ( M ... N ) = ( ( M ... ( K - 1 ) ) u. ( ( ( K - 1 ) + 1 ) ... N ) ) )
21 7 oveq1d 
 |-  ( ph -> ( ( ( K - 1 ) + 1 ) ... N ) = ( K ... N ) )
22 21 uneq2d 
 |-  ( ph -> ( ( M ... ( K - 1 ) ) u. ( ( ( K - 1 ) + 1 ) ... N ) ) = ( ( M ... ( K - 1 ) ) u. ( K ... N ) ) )
23 20 22 eqtrd 
 |-  ( ph -> ( M ... N ) = ( ( M ... ( K - 1 ) ) u. ( K ... N ) ) )