Metamath Proof Explorer

Theorem fzosplitsnm1

Description: Removing a singleton from a half-open integer range at the end. (Contributed by Alexander van der Vekens, 23-Mar-2018)

Ref Expression
Assertion fzosplitsnm1 
|- ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( A ..^ B ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) } ) )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( B e. ( ZZ>= ` ( A + 1 ) ) -> B e. ZZ )
2 1 zcnd 
 |-  ( B e. ( ZZ>= ` ( A + 1 ) ) -> B e. CC )
3 2 adantl 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> B e. CC )
4 ax-1cn 
 |-  1 e. CC
5 npcan 
 |-  ( ( B e. CC /\ 1 e. CC ) -> ( ( B - 1 ) + 1 ) = B )
6 5 eqcomd 
 |-  ( ( B e. CC /\ 1 e. CC ) -> B = ( ( B - 1 ) + 1 ) )
7 3 4 6 sylancl 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> B = ( ( B - 1 ) + 1 ) )
8 7 oveq2d 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( A ..^ B ) = ( A ..^ ( ( B - 1 ) + 1 ) ) )
9 eluzp1m1 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( B - 1 ) e. ( ZZ>= ` A ) )
10 1 adantl 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> B e. ZZ )
11 peano2zm 
 |-  ( B e. ZZ -> ( B - 1 ) e. ZZ )
12 uzid 
 |-  ( ( B - 1 ) e. ZZ -> ( B - 1 ) e. ( ZZ>= ` ( B - 1 ) ) )
13 peano2uz 
 |-  ( ( B - 1 ) e. ( ZZ>= ` ( B - 1 ) ) -> ( ( B - 1 ) + 1 ) e. ( ZZ>= ` ( B - 1 ) ) )
14 10 11 12 13 4syl 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( ( B - 1 ) + 1 ) e. ( ZZ>= ` ( B - 1 ) ) )
15 elfzuzb 
 |-  ( ( B - 1 ) e. ( A ... ( ( B - 1 ) + 1 ) ) <-> ( ( B - 1 ) e. ( ZZ>= ` A ) /\ ( ( B - 1 ) + 1 ) e. ( ZZ>= ` ( B - 1 ) ) ) )
16 9 14 15 sylanbrc 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( B - 1 ) e. ( A ... ( ( B - 1 ) + 1 ) ) )
17 fzosplit 
 |-  ( ( B - 1 ) e. ( A ... ( ( B - 1 ) + 1 ) ) -> ( A ..^ ( ( B - 1 ) + 1 ) ) = ( ( A ..^ ( B - 1 ) ) u. ( ( B - 1 ) ..^ ( ( B - 1 ) + 1 ) ) ) )
18 16 17 syl 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( A ..^ ( ( B - 1 ) + 1 ) ) = ( ( A ..^ ( B - 1 ) ) u. ( ( B - 1 ) ..^ ( ( B - 1 ) + 1 ) ) ) )
19 1 11 syl 
 |-  ( B e. ( ZZ>= ` ( A + 1 ) ) -> ( B - 1 ) e. ZZ )
20 19 adantl 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( B - 1 ) e. ZZ )
21 fzosn 
 |-  ( ( B - 1 ) e. ZZ -> ( ( B - 1 ) ..^ ( ( B - 1 ) + 1 ) ) = { ( B - 1 ) } )
22 20 21 syl 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( ( B - 1 ) ..^ ( ( B - 1 ) + 1 ) ) = { ( B - 1 ) } )
23 22 uneq2d 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( ( A ..^ ( B - 1 ) ) u. ( ( B - 1 ) ..^ ( ( B - 1 ) + 1 ) ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) } ) )
24 8 18 23 3eqtrd 
 |-  ( ( A e. ZZ /\ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( A ..^ B ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) } ) )