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