pfxccat3

Description: The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018) (Revised by AV, 10-May-2020)

		Ref	Expression
	Hypothesis	swrdccatin2.l	$⊢ L = \|A\|$
	Assertion	pfxccat3	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L)))))$

Proof

Step	Hyp	Ref	Expression
1		swrdccatin2.l	$⊢ L = \|A\|$
2		simpll	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land N \leq L) \to (A \in Word V \land B \in Word V)$
3		simplrl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land N \leq L) \to M \in (0 \dots N)$
4		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
5		elfznn0	$⊢ N \in (0 \dots L + \|B\|) \to N \in ℕ_{0}$
6	5	adantr	$⊢ (N \in (0 \dots L + \|B\|) \land \|A\| \in ℕ_{0}) \to N \in ℕ_{0}$
7	6	adantr	$⊢ ((N \in (0 \dots L + \|B\|) \land \|A\| \in ℕ_{0}) \land N \leq L) \to N \in ℕ_{0}$
8		simplr	$⊢ ((N \in (0 \dots L + \|B\|) \land \|A\| \in ℕ_{0}) \land N \leq L) \to \|A\| \in ℕ_{0}$
9	1	breq2i	$⊢ N \leq L \leftrightarrow N \leq \|A\|$
10	9	biimpi	$⊢ N \leq L \to N \leq \|A\|$
11	10	adantl	$⊢ ((N \in (0 \dots L + \|B\|) \land \|A\| \in ℕ_{0}) \land N \leq L) \to N \leq \|A\|$
12		elfz2nn0	$⊢ N \in (0 \dots \|A\|) \leftrightarrow (N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|)$
13	7 8 11 12	syl3anbrc	$⊢ ((N \in (0 \dots L + \|B\|) \land \|A\| \in ℕ_{0}) \land N \leq L) \to N \in (0 \dots \|A\|)$
14	13	exp31	$⊢ N \in (0 \dots L + \|B\|) \to (\|A\| \in ℕ_{0} \to (N \leq L \to N \in (0 \dots \|A\|)))$
15	14	adantl	$⊢ (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (\|A\| \in ℕ_{0} \to (N \leq L \to N \in (0 \dots \|A\|)))$
16	4 15	syl5com	$⊢ A \in Word V \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (N \leq L \to N \in (0 \dots \|A\|)))$
17	16	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (N \leq L \to N \in (0 \dots \|A\|)))$
18	17	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (N \leq L \to N \in (0 \dots \|A\|))$
19	18	imp	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land N \leq L) \to N \in (0 \dots \|A\|)$
20	3 19	jca	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land N \leq L) \to (M \in (0 \dots N) \land N \in (0 \dots \|A\|))$
21		swrdccatin1	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots \|A\|)) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩)$
22	2 20 21	sylc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land N \leq L) \to (A ++ B) substr ⟨M, N⟩ = A substr ⟨M, N⟩$
23		simp1l	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land L \leq M) \to (A \in Word V \land B \in Word V)$
24	1	eleq1i	$⊢ L \in ℕ_{0} \leftrightarrow \|A\| \in ℕ_{0}$
25		elfz2nn0	$⊢ M \in (0 \dots N) \leftrightarrow (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N)$
26		nn0z	$⊢ L \in ℕ_{0} \to L \in ℤ$
27	26	adantl	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \to L \in ℤ$
28		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
29	28	3ad2ant2	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to N \in ℤ$
30	29	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \to N \in ℤ$
31		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
32	31	3ad2ant1	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to M \in ℤ$
33	32	adantr	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \to M \in ℤ$
34	27 30 33	3jca	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \to (L \in ℤ \land N \in ℤ \land M \in ℤ)$
35	34	adantr	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \land L \leq M) \to (L \in ℤ \land N \in ℤ \land M \in ℤ)$
36		simpl3	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \to M \leq N$
37	36	anim1ci	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \land L \leq M) \to (L \leq M \land M \leq N)$
38		elfz2	$⊢ M \in (L \dots N) \leftrightarrow ((L \in ℤ \land N \in ℤ \land M \in ℤ) \land (L \leq M \land M \leq N))$
39	35 37 38	sylanbrc	$⊢ (((M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \land L \in ℕ_{0}) \land L \leq M) \to M \in (L \dots N)$
40	39	exp31	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (L \in ℕ_{0} \to (L \leq M \to M \in (L \dots N)))$
41	25 40	sylbi	$⊢ M \in (0 \dots N) \to (L \in ℕ_{0} \to (L \leq M \to M \in (L \dots N)))$
42	41	adantr	$⊢ (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (L \in ℕ_{0} \to (L \leq M \to M \in (L \dots N)))$
43	42	com12	$⊢ L \in ℕ_{0} \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (L \leq M \to M \in (L \dots N)))$
44	24 43	sylbir	$⊢ \|A\| \in ℕ_{0} \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (L \leq M \to M \in (L \dots N)))$
45	4 44	syl	$⊢ A \in Word V \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (L \leq M \to M \in (L \dots N)))$
46	45	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (L \leq M \to M \in (L \dots N)))$
47	46	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (L \leq M \to M \in (L \dots N))$
48	47	a1d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (\neg N \leq L \to (L \leq M \to M \in (L \dots N)))$
49	48	3imp	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land L \leq M) \to M \in (L \dots N)$
50		elfz2nn0	$⊢ N \in (0 \dots L + \|B\|) \leftrightarrow (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)$
51		nn0z	$⊢ \|A\| \in ℕ_{0} \to \|A\| \in ℤ$
52	1 51	eqeltrid	$⊢ \|A\| \in ℕ_{0} \to L \in ℤ$
53	52	adantr	$⊢ (\|A\| \in ℕ_{0} \land \neg N \leq L) \to L \in ℤ$
54	53	adantl	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to L \in ℤ$
55		nn0z	$⊢ L + \|B\| \in ℕ_{0} \to L + \|B\| \in ℤ$
56	55	3ad2ant2	$⊢ (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to L + \|B\| \in ℤ$
57	56	adantr	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to L + \|B\| \in ℤ$
58	28	3ad2ant1	$⊢ (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to N \in ℤ$
59	58	adantr	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to N \in ℤ$
60	54 57 59	3jca	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ)$
61	1	eqcomi	$⊢ \|A\| = L$
62	61	eleq1i	$⊢ \|A\| \in ℕ_{0} \leftrightarrow L \in ℕ_{0}$
63		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
64		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
65		ltnle	$⊢ (L \in ℝ \land N \in ℝ) \to (L < N \leftrightarrow \neg N \leq L)$
66	63 64 65	syl2anr	$⊢ (N \in ℕ_{0} \land L \in ℕ_{0}) \to (L < N \leftrightarrow \neg N \leq L)$
67	66	bicomd	$⊢ (N \in ℕ_{0} \land L \in ℕ_{0}) \to (\neg N \leq L \leftrightarrow L < N)$
68		ltle	$⊢ (L \in ℝ \land N \in ℝ) \to (L < N \to L \leq N)$
69	63 64 68	syl2anr	$⊢ (N \in ℕ_{0} \land L \in ℕ_{0}) \to (L < N \to L \leq N)$
70	67 69	sylbid	$⊢ (N \in ℕ_{0} \land L \in ℕ_{0}) \to (\neg N \leq L \to L \leq N)$
71	70	ex	$⊢ N \in ℕ_{0} \to (L \in ℕ_{0} \to (\neg N \leq L \to L \leq N))$
72	62 71	syl5bi	$⊢ N \in ℕ_{0} \to (\|A\| \in ℕ_{0} \to (\neg N \leq L \to L \leq N))$
73	72	3ad2ant1	$⊢ (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to (\|A\| \in ℕ_{0} \to (\neg N \leq L \to L \leq N))$
74	73	imp32	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to L \leq N$
75		simpl3	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to N \leq L + \|B\|$
76	74 75	jca	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to (L \leq N \land N \leq L + \|B\|)$
77		elfz2	$⊢ N \in (L \dots L + \|B\|) \leftrightarrow ((L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ) \land (L \leq N \land N \leq L + \|B\|))$
78	60 76 77	sylanbrc	$⊢ ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \land (\|A\| \in ℕ_{0} \land \neg N \leq L)) \to N \in (L \dots L + \|B\|)$
79	78	exp32	$⊢ (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to (\|A\| \in ℕ_{0} \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
80	50 79	sylbi	$⊢ N \in (0 \dots L + \|B\|) \to (\|A\| \in ℕ_{0} \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
81	80	adantl	$⊢ (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (\|A\| \in ℕ_{0} \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
82	4 81	syl5com	$⊢ A \in Word V \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
83	82	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
84	83	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (\neg N \leq L \to N \in (L \dots L + \|B\|))$
85	84	a1dd	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (\neg N \leq L \to (L \leq M \to N \in (L \dots L + \|B\|)))$
86	85	3imp	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land L \leq M) \to N \in (L \dots L + \|B\|)$
87	49 86	jca	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land L \leq M) \to (M \in (L \dots N) \land N \in (L \dots L + \|B\|))$
88	1	swrdccatin2	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (L \dots N) \land N \in (L \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩)$
89	23 87 88	sylc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land L \leq M) \to (A ++ B) substr ⟨M, N⟩ = B substr ⟨M - L, N - L⟩$
90		simp1l	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land \neg L \leq M) \to (A \in Word V \land B \in Word V)$
91		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
92	91	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \in ℝ$
93		ltnle	$⊢ (M \in ℝ \land L \in ℝ) \to (M < L \leftrightarrow \neg L \leq M)$
94	92 63 93	syl2anr	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (M < L \leftrightarrow \neg L \leq M)$
95	94	bicomd	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (\neg L \leq M \leftrightarrow M < L)$
96		simpll	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land M < L) \to M \in ℕ_{0}$
97		simplr	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land M < L) \to L \in ℕ_{0}$
98		ltle	$⊢ (M \in ℝ \land L \in ℝ) \to (M < L \to M \leq L)$
99	91 63 98	syl2an	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (M < L \to M \leq L)$
100	99	imp	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land M < L) \to M \leq L$
101		elfz2nn0	$⊢ M \in (0 \dots L) \leftrightarrow (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)$
102	96 97 100 101	syl3anbrc	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0}) \land M < L) \to M \in (0 \dots L)$
103	102	exp31	$⊢ M \in ℕ_{0} \to (L \in ℕ_{0} \to (M < L \to M \in (0 \dots L)))$
104	103	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (L \in ℕ_{0} \to (M < L \to M \in (0 \dots L)))$
105	104	impcom	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (M < L \to M \in (0 \dots L))$
106	95 105	sylbid	$⊢ (L \in ℕ_{0} \land (M \in ℕ_{0} \land N \in ℕ_{0})) \to (\neg L \leq M \to M \in (0 \dots L))$
107	106	expcom	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (L \in ℕ_{0} \to (\neg L \leq M \to M \in (0 \dots L)))$
108	107	3adant3	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0} \land M \leq N) \to (L \in ℕ_{0} \to (\neg L \leq M \to M \in (0 \dots L)))$
109	25 108	sylbi	$⊢ M \in (0 \dots N) \to (L \in ℕ_{0} \to (\neg L \leq M \to M \in (0 \dots L)))$
110	62 109	syl5bi	$⊢ M \in (0 \dots N) \to (\|A\| \in ℕ_{0} \to (\neg L \leq M \to M \in (0 \dots L)))$
111	110	adantr	$⊢ (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (\|A\| \in ℕ_{0} \to (\neg L \leq M \to M \in (0 \dots L)))$
112	4 111	syl5com	$⊢ A \in Word V \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (\neg L \leq M \to M \in (0 \dots L)))$
113	112	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (\neg L \leq M \to M \in (0 \dots L)))$
114	113	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (\neg L \leq M \to M \in (0 \dots L))$
115	114	a1d	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (\neg N \leq L \to (\neg L \leq M \to M \in (0 \dots L)))$
116	115	3imp	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land \neg L \leq M) \to M \in (0 \dots L)$
117	64	3ad2ant1	$⊢ (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to N \in ℝ$
118	65	bicomd	$⊢ (L \in ℝ \land N \in ℝ) \to (\neg N \leq L \leftrightarrow L < N)$
119	63 117 118	syl2an	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to (\neg N \leq L \leftrightarrow L < N)$
120	26	adantr	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to L \in ℤ$
121	56	adantl	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to L + \|B\| \in ℤ$
122	58	adantl	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to N \in ℤ$
123	120 121 122	3jca	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ)$
124	123	adantr	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \land L < N) \to (L \in ℤ \land L + \|B\| \in ℤ \land N \in ℤ)$
125	63 117 68	syl2an	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to (L < N \to L \leq N)$
126	125	imp	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \land L < N) \to L \leq N$
127		simplr3	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \land L < N) \to N \leq L + \|B\|$
128	126 127	jca	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \land L < N) \to (L \leq N \land N \leq L + \|B\|)$
129	124 128 77	sylanbrc	$⊢ ((L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \land L < N) \to N \in (L \dots L + \|B\|)$
130	129	ex	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to (L < N \to N \in (L \dots L + \|B\|))$
131	119 130	sylbid	$⊢ (L \in ℕ_{0} \land (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|)) \to (\neg N \leq L \to N \in (L \dots L + \|B\|))$
132	131	ex	$⊢ L \in ℕ_{0} \to ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
133	62 132	sylbi	$⊢ \|A\| \in ℕ_{0} \to ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
134	4 133	syl	$⊢ A \in Word V \to ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
135	134	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
136	135	com12	$⊢ (N \in ℕ_{0} \land L + \|B\| \in ℕ_{0} \land N \leq L + \|B\|) \to ((A \in Word V \land B \in Word V) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
137	50 136	sylbi	$⊢ N \in (0 \dots L + \|B\|) \to ((A \in Word V \land B \in Word V) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
138	137	adantl	$⊢ (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to ((A \in Word V \land B \in Word V) \to (\neg N \leq L \to N \in (L \dots L + \|B\|)))$
139	138	impcom	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (\neg N \leq L \to N \in (L \dots L + \|B\|))$
140	139	a1dd	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (\neg N \leq L \to (\neg L \leq M \to N \in (L \dots L + \|B\|)))$
141	140	3imp	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land \neg L \leq M) \to N \in (L \dots L + \|B\|)$
142	116 141	jca	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land \neg L \leq M) \to (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))$
143	1	pfxccatin12	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, L⟩) ++ (B prefix (N - L)))$
144	90 142 143	sylc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \land \neg N \leq L \land \neg L \leq M) \to (A ++ B) substr ⟨M, N⟩ = (A substr ⟨M, L⟩) ++ (B prefix (N - L))$
145	22 89 144	2if2	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots N) \land N \in (0 \dots L + \|B\|))) \to (A ++ B) substr ⟨M, N⟩ = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L))))$
146	145	ex	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots N) \land N \in (0 \dots L + \|B\|)) \to (A ++ B) substr ⟨M, N⟩ = if (N \leq L, A substr ⟨M, N⟩, if (L \leq M, B substr ⟨M - L, N - L⟩, (A substr ⟨M, L⟩) ++ (B prefix (N - L)))))$

Metamath Proof Explorer

Theorem pfxccat3

Proof