Metamath Proof Explorer

Theorem clwlkclwwlklem2a3

Description: Lemma 3 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018)

Ref Expression
Hypothesis clwlkclwwlklem2.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
Assertion clwlkclwwlklem2a3 ⊢ P ∈ Word V ∧ 2 ≤ P → P ⁡ F = lastS ⁡ P

Proof

Step Hyp Ref Expression
1 clwlkclwwlklem2.f ⊢ F = x ∈ 0 ..^ P − 1 ⟼ if x < P − 2 E -1 ⁡ P ⁡ x P ⁡ x + 1 E -1 ⁡ P ⁡ x P ⁡ 0
2 lsw ⊢ P ∈ Word V → lastS ⁡ P = P ⁡ P − 1
3 2 adantr ⊢ P ∈ Word V ∧ 2 ≤ P → lastS ⁡ P = P ⁡ P − 1
4 1 clwlkclwwlklem2a2 ⊢ P ∈ Word V ∧ 2 ≤ P → F = P − 1
5 4 eqcomd ⊢ P ∈ Word V ∧ 2 ≤ P → P − 1 = F
6 5 fveq2d ⊢ P ∈ Word V ∧ 2 ≤ P → P ⁡ P − 1 = P ⁡ F
7 3 6 eqtr2d ⊢ P ∈ Word V ∧ 2 ≤ P → P ⁡ F = lastS ⁡ P