This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzosplitsn

Description: Extending a half-open range by a singleton on the end. (Contributed by Stefan O'Rear, 23-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ( ZZ>= ` A ) )
2 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
3 uzid 
 |-  ( B e. ZZ -> B e. ( ZZ>= ` B ) )
4 peano2uz 
 |-  ( B e. ( ZZ>= ` B ) -> ( B + 1 ) e. ( ZZ>= ` B ) )
5 2 3 4 3syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( B + 1 ) e. ( ZZ>= ` B ) )
6 elfzuzb 
 |-  ( B e. ( A ... ( B + 1 ) ) <-> ( B e. ( ZZ>= ` A ) /\ ( B + 1 ) e. ( ZZ>= ` B ) ) )
7 1 5 6 sylanbrc 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ( A ... ( B + 1 ) ) )
8 fzosplit 
 |-  ( B e. ( A ... ( B + 1 ) ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. ( B ..^ ( B + 1 ) ) ) )
9 7 8 syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. ( B ..^ ( B + 1 ) ) ) )
10 fzosn 
 |-  ( B e. ZZ -> ( B ..^ ( B + 1 ) ) = { B } )
11 2 10 syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( B ..^ ( B + 1 ) ) = { B } )
12 11 uneq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A ..^ B ) u. ( B ..^ ( B + 1 ) ) ) = ( ( A ..^ B ) u. { B } ) )
13 9 12 eqtrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. { B } ) )