Metamath Proof Explorer

Theorem fzosplitpr

Description: Extending a half-open integer range by an unordered pair at the end. (Contributed by Alexander van der Vekens, 22-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1 a1i 
 |-  ( B e. ( ZZ>= ` A ) -> 2 = ( 1 + 1 ) )
3 2 oveq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( B + 2 ) = ( B + ( 1 + 1 ) ) )
4 eluzelcn 
 |-  ( B e. ( ZZ>= ` A ) -> B e. CC )
5 1cnd 
 |-  ( B e. ( ZZ>= ` A ) -> 1 e. CC )
6 add32r 
 |-  ( ( B e. CC /\ 1 e. CC /\ 1 e. CC ) -> ( B + ( 1 + 1 ) ) = ( ( B + 1 ) + 1 ) )
7 4 5 5 6 syl3anc 
 |-  ( B e. ( ZZ>= ` A ) -> ( B + ( 1 + 1 ) ) = ( ( B + 1 ) + 1 ) )
8 3 7 eqtrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( B + 2 ) = ( ( B + 1 ) + 1 ) )
9 8 oveq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 2 ) ) = ( A ..^ ( ( B + 1 ) + 1 ) ) )
10 peano2uz 
 |-  ( B e. ( ZZ>= ` A ) -> ( B + 1 ) e. ( ZZ>= ` A ) )
11 fzosplitsn 
 |-  ( ( B + 1 ) e. ( ZZ>= ` A ) -> ( A ..^ ( ( B + 1 ) + 1 ) ) = ( ( A ..^ ( B + 1 ) ) u. { ( B + 1 ) } ) )
12 10 11 syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ ( ( B + 1 ) + 1 ) ) = ( ( A ..^ ( B + 1 ) ) u. { ( B + 1 ) } ) )
13 fzosplitsn 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. { B } ) )
14 13 uneq1d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A ..^ ( B + 1 ) ) u. { ( B + 1 ) } ) = ( ( ( A ..^ B ) u. { B } ) u. { ( B + 1 ) } ) )
15 unass 
 |-  ( ( ( A ..^ B ) u. { B } ) u. { ( B + 1 ) } ) = ( ( A ..^ B ) u. ( { B } u. { ( B + 1 ) } ) )
16 15 a1i 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( ( A ..^ B ) u. { B } ) u. { ( B + 1 ) } ) = ( ( A ..^ B ) u. ( { B } u. { ( B + 1 ) } ) ) )
17 df-pr 
 |-  { B , ( B + 1 ) } = ( { B } u. { ( B + 1 ) } )
18 17 eqcomi 
 |-  ( { B } u. { ( B + 1 ) } ) = { B , ( B + 1 ) }
19 18 a1i 
 |-  ( B e. ( ZZ>= ` A ) -> ( { B } u. { ( B + 1 ) } ) = { B , ( B + 1 ) } )
20 19 uneq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A ..^ B ) u. ( { B } u. { ( B + 1 ) } ) ) = ( ( A ..^ B ) u. { B , ( B + 1 ) } ) )
21 14 16 20 3eqtrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A ..^ ( B + 1 ) ) u. { ( B + 1 ) } ) = ( ( A ..^ B ) u. { B , ( B + 1 ) } ) )
22 9 12 21 3eqtrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 2 ) ) = ( ( A ..^ B ) u. { B , ( B + 1 ) } ) )