Metamath Proof Explorer


Theorem lpadlem3

Description: Lemma for lpadlen1 . (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadlen.1 φ L 0
lpadlen.2 φ W Word S
lpadlen.3 φ C S
lpadlen1.1 φ L W
Assertion lpadlem3 φ 0 ..^ L W × C =

Proof

Step Hyp Ref Expression
1 lpadlen.1 φ L 0
2 lpadlen.2 φ W Word S
3 lpadlen.3 φ C S
4 lpadlen1.1 φ L W
5 lencl W Word S W 0
6 2 5 syl φ W 0
7 6 nn0zd φ W
8 1 nn0zd φ L
9 fzo0n W L L W 0 ..^ L W =
10 9 biimpa W L L W 0 ..^ L W =
11 7 8 4 10 syl21anc φ 0 ..^ L W =
12 11 xpeq1d φ 0 ..^ L W × C = × C
13 0xp × C =
14 12 13 eqtrdi φ 0 ..^ L W × C =