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	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left(0..^\left|W\right|+2-1\right)=\left(0..^\left|W\right|-1\right)\cup \left\{\left|W\right|-1,\left|W\right|\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eluzelcn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in ℂ$$
2		2cnd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 2\in ℂ$$
3	1 2	subcld	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N-2\in ℂ$$
4	3	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to N-2\in ℂ$$
5		eleq1	$$⊢\left|W\right|=N-2\to \left(\left|W\right|\in ℂ\leftrightarrow N-2\in ℂ\right)$$
6	5	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left(\left|W\right|\in ℂ\leftrightarrow N-2\in ℂ\right)$$
7	4 6	mpbird	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left|W\right|\in ℂ$$
8		2cnd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to 2\in ℂ$$
9		1cnd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to 1\in ℂ$$
10	7 8 9	addsubd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left|W\right|+2-1=\left|W\right|-1+2$$
11	10	oveq2d	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left(0..^\left|W\right|+2-1\right)=\left(0..^\left|W\right|-1+2\right)$$
12		oveq1	$$⊢\left|W\right|=N-2\to \left|W\right|-1=N-2-1$$
13	12	adantl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left|W\right|-1=N-2-1$$
14		uznn0sub	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N-3\in {\mathbb{N}}_0$$
15		1cnd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 1\in ℂ$$
16	1 2 15	subsub4d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N-2-1=N-\left(2+1\right)$$
17		2p1e3	$$⊢2+1=3$$
18	17	oveq2i	$$⊢N-\left(2+1\right)=N-3$$
19	16 18	eqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N-2-1=N-3$$
20		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
21	20	eqcomi	$$⊢{\mathbb{Z}}_{\ge 0}={\mathbb{N}}_0$$
22	21	a1i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to {\mathbb{Z}}_{\ge 0}={\mathbb{N}}_0$$
23	14 19 22	3eltr4d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N-2-1\in {\mathbb{Z}}_{\ge 0}$$
24	23	adantr	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to N-2-1\in {\mathbb{Z}}_{\ge 0}$$
25	13 24	eqeltrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left|W\right|-1\in {\mathbb{Z}}_{\ge 0}$$
26		fzosplitpr	$$⊢\left|W\right|-1\in {\mathbb{Z}}_{\ge 0}\to \left(0..^\left|W\right|-1+2\right)=\left(0..^\left|W\right|-1\right)\cup \left\{\left|W\right|-1,\left|W\right|-1+1\right\}$$
27	25 26	syl	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left(0..^\left|W\right|-1+2\right)=\left(0..^\left|W\right|-1\right)\cup \left\{\left|W\right|-1,\left|W\right|-1+1\right\}$$
28	7 9	npcand	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left|W\right|-1+1=\left|W\right|$$
29	28	preq2d	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left\{\left|W\right|-1,\left|W\right|-1+1\right\}=\left\{\left|W\right|-1,\left|W\right|\right\}$$
30	29	uneq2d	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left(0..^\left|W\right|-1\right)\cup \left\{\left|W\right|-1,\left|W\right|-1+1\right\}=\left(0..^\left|W\right|-1\right)\cup \left\{\left|W\right|-1,\left|W\right|\right\}$$
31	11 27 30	3eqtrd	$$⊢\left(N\in {\mathbb{Z}}_{\ge 3}\wedge \left|W\right|=N-2\right)\to \left(0..^\left|W\right|+2-1\right)=\left(0..^\left|W\right|-1\right)\cup \left\{\left|W\right|-1,\left|W\right|\right\}$$