Metamath Proof Explorer

Theorem addlenrevpfx

Description: The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018) (Revised by AV, 3-May-2020)

Ref Expression
Assertion addlenrevpfx ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W + W prefix M = W

Proof

Step Hyp Ref Expression
1 swrdrlen ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W = W − M
2 pfxlen ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M = M
3 1 2 oveq12d ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W + W prefix M = W - M + M
4 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
5 elfzelz ⊢ M ∈ 0 … W → M ∈ ℤ
6 nn0cn ⊢ W ∈ ℕ 0 → W ∈ ℂ
7 zcn ⊢ M ∈ ℤ → M ∈ ℂ
8 npcan ⊢ W ∈ ℂ ∧ M ∈ ℂ → W - M + M = W
9 6 7 8 syl2an ⊢ W ∈ ℕ 0 ∧ M ∈ ℤ → W - M + M = W
10 4 5 9 syl2an ⊢ W ∈ Word V ∧ M ∈ 0 … W → W - M + M = W
11 3 10 eqtrd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W + W prefix M = W