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 3 W = N 2 0 ..^ W + 2 - 1 = 0 ..^ W 1 W 1 W

Proof

Step Hyp Ref Expression
1 eluzelcn N 3 N
2 2cnd N 3 2
3 1 2 subcld N 3 N 2
4 3 adantr N 3 W = N 2 N 2
5 eleq1 W = N 2 W N 2
6 5 adantl N 3 W = N 2 W N 2
7 4 6 mpbird N 3 W = N 2 W
8 2cnd N 3 W = N 2 2
9 1cnd N 3 W = N 2 1
10 7 8 9 addsubd N 3 W = N 2 W + 2 - 1 = W - 1 + 2
11 10 oveq2d N 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 3 W = N 2 W 1 = N - 2 - 1
14 uznn0sub N 3 N 3 0
15 1cnd N 3 1
16 1 2 15 subsub4d N 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 3 N - 2 - 1 = N 3
20 nn0uz 0 = 0
21 20 eqcomi 0 = 0
22 21 a1i N 3 0 = 0
23 14 19 22 3eltr4d N 3 N - 2 - 1 0
24 23 adantr N 3 W = N 2 N - 2 - 1 0
25 13 24 eqeltrd N 3 W = N 2 W 1 0
26 fzosplitpr W 1 0 0 ..^ W - 1 + 2 = 0 ..^ W 1 W 1 W - 1 + 1
27 25 26 syl N 3 W = N 2 0 ..^ W - 1 + 2 = 0 ..^ W 1 W 1 W - 1 + 1
28 7 9 npcand N 3 W = N 2 W - 1 + 1 = W
29 28 preq2d N 3 W = N 2 W 1 W - 1 + 1 = W 1 W
30 29 uneq2d N 3 W = N 2 0 ..^ W 1 W 1 W - 1 + 1 = 0 ..^ W 1 W 1 W
31 11 27 30 3eqtrd N 3 W = N 2 0 ..^ W + 2 - 1 = 0 ..^ W 1 W 1 W