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 ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) )

Proof

Step Hyp Ref Expression
1 eluzelcn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℂ )
2 2cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 ∈ ℂ )
3 1 2 subcld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℂ )
4 3 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 𝑁 − 2 ) ∈ ℂ )
5 eleq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ↔ ( 𝑁 − 2 ) ∈ ℂ ) )
6 5 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( ♯ ‘ 𝑊 ) ∈ ℂ ↔ ( 𝑁 − 2 ) ∈ ℂ ) )
7 4 6 mpbird ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
8 2cnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → 2 ∈ ℂ )
9 1cnd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → 1 ∈ ℂ )
10 7 8 9 addsubd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) = ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 2 ) )
11 10 oveq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) ) = ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 2 ) ) )
12 oveq1 ⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 − 2 ) − 1 ) )
13 12 adantl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 − 2 ) − 1 ) )
14 uznn0sub ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 3 ) ∈ ℕ0 )
15 1cnd ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℂ )
16 1 2 15 subsub4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑁 − 2 ) − 1 ) = ( 𝑁 − ( 2 + 1 ) ) )
17 2p1e3 ⊢ ( 2 + 1 ) = 3
18 17 oveq2i ⊢ ( 𝑁 − ( 2 + 1 ) ) = ( 𝑁 − 3 )
19 16 18 eqtrdi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑁 − 2 ) − 1 ) = ( 𝑁 − 3 ) )
20 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
21 20 eqcomi ⊢ ( ℤ≥ ‘ 0 ) = ℕ0
22 21 a1i ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ℤ≥ ‘ 0 ) = ℕ0 )
23 14 19 22 3eltr4d ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑁 − 2 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
24 23 adantr ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( 𝑁 − 2 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
25 13 24 eqeltrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
26 fzosplitpr ⊢ ( ( ( ♯ ‘ 𝑊 ) − 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 2 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) } ) )
27 25 26 syl ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 2 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) } ) )
28 7 9 npcand ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) = ( ♯ ‘ 𝑊 ) )
29 28 preq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) } = { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } )
30 29 uneq2d ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ( ( ♯ ‘ 𝑊 ) − 1 ) + 1 ) } ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) )
31 11 27 30 3eqtrd ⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ ( ♯ ‘ 𝑊 ) = ( 𝑁 − 2 ) ) → ( 0 ..^ ( ( ( ♯ ‘ 𝑊 ) + 2 ) − 1 ) ) = ( ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) ∪ { ( ( ♯ ‘ 𝑊 ) − 1 ) , ( ♯ ‘ 𝑊 ) } ) )