Theorem lpadlem3

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

	Ref	Expression
Hypotheses	lpadlen.1	$$⊢\phi \to L\in {\mathbb{N}}_0$$
	lpadlen.2	$$⊢\phi \to W\in \mathrm{Word}S$$
	lpadlen.3	$$⊢\phi \to C\in S$$
	lpadlen1.1	$$⊢\phi \to L\le \left|W\right|$$
Assertion	lpadlem3	$$⊢\phi \to \left(0..^L-\left|W\right|\right)\times \left\{C\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		lpadlen.1	$$⊢\phi \to L\in {\mathbb{N}}_0$$
2		lpadlen.2	$$⊢\phi \to W\in \mathrm{Word}S$$
3		lpadlen.3	$$⊢\phi \to C\in S$$
4		lpadlen1.1	$$⊢\phi \to L\le \left|W\right|$$
5		lencl	$$⊢W\in \mathrm{Word}S\to \left|W\right|\in {\mathbb{N}}_0$$
6	2 5	syl	$$⊢\phi \to \left|W\right|\in {\mathbb{N}}_0$$
7	6	nn0zd	$$⊢\phi \to \left|W\right|\in \mathbb{Z}$$
8	1	nn0zd	$$⊢\phi \to L\in \mathbb{Z}$$
9		fzo0n	$$⊢\left(\left|W\right|\in \mathbb{Z}\wedge L\in \mathbb{Z}\right)\to \left(L\le \left|W\right|\leftrightarrow \left(0..^L-\left|W\right|\right)=\varnothing \right)$$
10	9	biimpa	$$⊢\left(\left(\left|W\right|\in \mathbb{Z}\wedge L\in \mathbb{Z}\right)\wedge L\le \left|W\right|\right)\to \left(0..^L-\left|W\right|\right)=\varnothing$$
11	7 8 4 10	syl21anc	$$⊢\phi \to \left(0..^L-\left|W\right|\right)=\varnothing$$
12	11	xpeq1d	$$⊢\phi \to \left(0..^L-\left|W\right|\right)\times \left\{C\right\}=\varnothing \times \left\{C\right\}$$
13		0xp	$$⊢\varnothing \times \left\{C\right\}=\varnothing$$
14	12 13	syl6eq	$$⊢\phi \to \left(0..^L-\left|W\right|\right)\times \left\{C\right\}=\varnothing$$