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−1W

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−1W-1+1
27 25 26 syl ⊢N∈ℤ≥3∧W=N−2→0..^W-1+2=0..^W−1∪W−1W-1+1
28 7 9 npcand ⊢N∈ℤ≥3∧W=N−2→W-1+1=W
29 28 preq2d ⊢N∈ℤ≥3∧W=N−2→W−1W-1+1=W−1W
30 29 uneq2d ⊢N∈ℤ≥3∧W=N−2→0..^W−1∪W−1W-1+1=0..^W−1∪W−1W
31 11 27 30 3eqtrd ⊢N∈ℤ≥3∧W=N−2→0..^W+2-1=0..^W−1∪W−1W