Metamath Proof Explorer

Theorem clwwlknonex2lem1

Description: Lemma 1 for clwwlknonex2 : Transformation of a special half-open integer range into a union of a smaller half-open integer range and an unordered pair. This Lemma would not hold for N = 2 , i.e., ( #W ) = 0 , because ( 0 ..^ ( ( ( #W ) + 2 ) - 1 ) ) = ( 0 ..^ ( ( 0 + 2 ) - 1 ) ) = ( 0 ..^ 1 ) = { 0 } =/= { -u 1 , 0 } = ( (/) u. { -u 1 , 0 } ) = ( ( 0 ..^ ( 0 - 1 ) ) u. { ( 0 - 1 ) , 0 } ) = ( ( 0 ..^ ( ( #W ) - 1 ) ) u. { ( ( #W ) - 1 ) , ( #W ) } ) . (Contributed by AV, 22-Sep-2018) (Revised by AV, 26-Jan-2022)

Ref Expression
Assertion clwwlknonex2lem1 
|- ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( 0 ..^ ( ( ( # ` W ) + 2 ) - 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) )

Proof

Step Hyp Ref Expression
1 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
2 2cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
3 1 2 subcld 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. CC )
4 3 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( N - 2 ) e. CC )
5 eleq1 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( ( # ` W ) e. CC <-> ( N - 2 ) e. CC ) )
6 5 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( # ` W ) e. CC <-> ( N - 2 ) e. CC ) )
7 4 6 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( # ` W ) e. CC )
8 2cnd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> 2 e. CC )
9 1cnd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> 1 e. CC )
10 7 8 9 addsubd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( ( # ` W ) + 2 ) - 1 ) = ( ( ( # ` W ) - 1 ) + 2 ) )
11 10 oveq2d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( 0 ..^ ( ( ( # ` W ) + 2 ) - 1 ) ) = ( 0 ..^ ( ( ( # ` W ) - 1 ) + 2 ) ) )
12 oveq1 
 |-  ( ( # ` W ) = ( N - 2 ) -> ( ( # ` W ) - 1 ) = ( ( N - 2 ) - 1 ) )
13 12 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( # ` W ) - 1 ) = ( ( N - 2 ) - 1 ) )
14 uznn0sub 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 3 ) e. NN0 )
15 1cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. CC )
16 1 2 15 subsub4d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) = ( N - ( 2 + 1 ) ) )
17 2p1e3 
 |-  ( 2 + 1 ) = 3
18 17 oveq2i 
 |-  ( N - ( 2 + 1 ) ) = ( N - 3 )
19 16 18 eqtrdi 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) = ( N - 3 ) )
20 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
21 20 eqcomi 
 |-  ( ZZ>= ` 0 ) = NN0
22 21 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ZZ>= ` 0 ) = NN0 )
23 14 19 22 3eltr4d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) - 1 ) e. ( ZZ>= ` 0 ) )
24 23 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( N - 2 ) - 1 ) e. ( ZZ>= ` 0 ) )
25 13 24 eqeltrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) )
26 fzosplitpr 
 |-  ( ( ( # ` W ) - 1 ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( ( # ` W ) - 1 ) + 2 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) } ) )
27 25 26 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( 0 ..^ ( ( ( # ` W ) - 1 ) + 2 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) } ) )
28 7 9 npcand 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
29 28 preq2d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> { ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) } = { ( ( # ` W ) - 1 ) , ( # ` W ) } )
30 29 uneq2d 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) } ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) )
31 11 27 30 3eqtrd 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ ( # ` W ) = ( N - 2 ) ) -> ( 0 ..^ ( ( ( # ` W ) + 2 ) - 1 ) ) = ( ( 0 ..^ ( ( # ` W ) - 1 ) ) u. { ( ( # ` W ) - 1 ) , ( # ` W ) } ) )