Metamath Proof Explorer

Theorem fzosplitprm1

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

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> A e. ZZ )
2 peano2zm 
 |-  ( B e. ZZ -> ( B - 1 ) e. ZZ )
3 2 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> ( B - 1 ) e. ZZ )
4 zltlem1 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> A <_ ( B - 1 ) ) )
5 4 biimp3a 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> A <_ ( B - 1 ) )
6 eluz2 
 |-  ( ( B - 1 ) e. ( ZZ>= ` A ) <-> ( A e. ZZ /\ ( B - 1 ) e. ZZ /\ A <_ ( B - 1 ) ) )
7 1 3 5 6 syl3anbrc 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> ( B - 1 ) e. ( ZZ>= ` A ) )
8 fzosplitpr 
 |-  ( ( B - 1 ) e. ( ZZ>= ` A ) -> ( A ..^ ( ( B - 1 ) + 2 ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , ( ( B - 1 ) + 1 ) } ) )
9 7 8 syl 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> ( A ..^ ( ( B - 1 ) + 2 ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , ( ( B - 1 ) + 1 ) } ) )
10 zcn 
 |-  ( B e. ZZ -> B e. CC )
11 1cnd 
 |-  ( B e. ZZ -> 1 e. CC )
12 2cnd 
 |-  ( B e. ZZ -> 2 e. CC )
13 10 11 12 subadd23d 
 |-  ( B e. ZZ -> ( ( B - 1 ) + 2 ) = ( B + ( 2 - 1 ) ) )
14 2m1e1 
 |-  ( 2 - 1 ) = 1
15 14 oveq2i 
 |-  ( B + ( 2 - 1 ) ) = ( B + 1 )
16 13 15 eqtr2di 
 |-  ( B e. ZZ -> ( B + 1 ) = ( ( B - 1 ) + 2 ) )
17 16 oveq2d 
 |-  ( B e. ZZ -> ( A ..^ ( B + 1 ) ) = ( A ..^ ( ( B - 1 ) + 2 ) ) )
18 npcan1 
 |-  ( B e. CC -> ( ( B - 1 ) + 1 ) = B )
19 10 18 syl 
 |-  ( B e. ZZ -> ( ( B - 1 ) + 1 ) = B )
20 19 eqcomd 
 |-  ( B e. ZZ -> B = ( ( B - 1 ) + 1 ) )
21 20 preq2d 
 |-  ( B e. ZZ -> { ( B - 1 ) , B } = { ( B - 1 ) , ( ( B - 1 ) + 1 ) } )
22 21 uneq2d 
 |-  ( B e. ZZ -> ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , B } ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , ( ( B - 1 ) + 1 ) } ) )
23 17 22 eqeq12d 
 |-  ( B e. ZZ -> ( ( A ..^ ( B + 1 ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , B } ) <-> ( A ..^ ( ( B - 1 ) + 2 ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , ( ( B - 1 ) + 1 ) } ) ) )
24 23 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> ( ( A ..^ ( B + 1 ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , B } ) <-> ( A ..^ ( ( B - 1 ) + 2 ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , ( ( B - 1 ) + 1 ) } ) ) )
25 9 24 mpbird 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ A < B ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ ( B - 1 ) ) u. { ( B - 1 ) , B } ) )