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