pfxccatin12lem3

Description: Lemma 3 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 27-May-2018)

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

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 L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to (A \in Word V \land B \in Word V)$
3		elfzo0	$⊢ K \in (0 ..^L - M) \leftrightarrow (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M)$
4		lencl	$⊢ A \in Word V \to \|A\| \in ℕ_{0}$
5		elfz2nn0	$⊢ M \in (0 \dots L) \leftrightarrow (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)$
6		nn0addcl	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to K + M \in ℕ_{0}$
7	6	ex	$⊢ K \in ℕ_{0} \to (M \in ℕ_{0} \to K + M \in ℕ_{0})$
8	7	3ad2ant1	$⊢ (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (M \in ℕ_{0} \to K + M \in ℕ_{0})$
9	8	com12	$⊢ M \in ℕ_{0} \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to K + M \in ℕ_{0})$
10	9	3ad2ant1	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to K + M \in ℕ_{0})$
11	10	imp	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \land (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M)) \to K + M \in ℕ_{0}$
12		elnnz	$⊢ L - M \in ℕ \leftrightarrow (L - M \in ℤ \land 0 < L - M)$
13		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
14		nn0re	$⊢ L \in ℕ_{0} \to L \in ℝ$
15		posdif	$⊢ (M \in ℝ \land L \in ℝ) \to (M < L \leftrightarrow 0 < L - M)$
16	13 14 15	syl2an	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (M < L \leftrightarrow 0 < L - M)$
17		elnn0z	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℤ \land 0 \leq M)$
18		0re	$⊢ 0 \in ℝ$
19		zre	$⊢ M \in ℤ \to M \in ℝ$
20		lelttr	$⊢ (0 \in ℝ \land M \in ℝ \land L \in ℝ) \to ((0 \leq M \land M < L) \to 0 < L)$
21	18 19 14 20	mp3an3an	$⊢ (M \in ℤ \land L \in ℕ_{0}) \to ((0 \leq M \land M < L) \to 0 < L)$
22		nn0z	$⊢ L \in ℕ_{0} \to L \in ℤ$
23	22	anim1i	$⊢ (L \in ℕ_{0} \land 0 < L) \to (L \in ℤ \land 0 < L)$
24		elnnz	$⊢ L \in ℕ \leftrightarrow (L \in ℤ \land 0 < L)$
25	23 24	sylibr	$⊢ (L \in ℕ_{0} \land 0 < L) \to L \in ℕ$
26	25	ex	$⊢ L \in ℕ_{0} \to (0 < L \to L \in ℕ)$
27	26	adantl	$⊢ (M \in ℤ \land L \in ℕ_{0}) \to (0 < L \to L \in ℕ)$
28	21 27	syld	$⊢ (M \in ℤ \land L \in ℕ_{0}) \to ((0 \leq M \land M < L) \to L \in ℕ)$
29	28	expd	$⊢ (M \in ℤ \land L \in ℕ_{0}) \to (0 \leq M \to (M < L \to L \in ℕ))$
30	29	impancom	$⊢ (M \in ℤ \land 0 \leq M) \to (L \in ℕ_{0} \to (M < L \to L \in ℕ))$
31	17 30	sylbi	$⊢ M \in ℕ_{0} \to (L \in ℕ_{0} \to (M < L \to L \in ℕ))$
32	31	imp	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (M < L \to L \in ℕ)$
33	16 32	sylbird	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to (0 < L - M \to L \in ℕ)$
34	33	com12	$⊢ 0 < L - M \to ((M \in ℕ_{0} \land L \in ℕ_{0}) \to L \in ℕ)$
35	12 34	simplbiim	$⊢ L - M \in ℕ \to ((M \in ℕ_{0} \land L \in ℕ_{0}) \to L \in ℕ)$
36	35	3ad2ant2	$⊢ (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to ((M \in ℕ_{0} \land L \in ℕ_{0}) \to L \in ℕ)$
37	36	com12	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0}) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to L \in ℕ)$
38	37	3adant3	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to L \in ℕ)$
39	38	imp	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \land (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M)) \to L \in ℕ$
40		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
41	40	adantr	$⊢ (K \in ℕ_{0} \land (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)) \to K \in ℝ$
42	13	3ad2ant1	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to M \in ℝ$
43	42	adantl	$⊢ (K \in ℕ_{0} \land (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)) \to M \in ℝ$
44	14	3ad2ant2	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to L \in ℝ$
45	44	adantl	$⊢ (K \in ℕ_{0} \land (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)) \to L \in ℝ$
46	41 43 45	ltaddsubd	$⊢ (K \in ℕ_{0} \land (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L)) \to (K + M < L \leftrightarrow K < L - M)$
47	46	exbiri	$⊢ K \in ℕ_{0} \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (K < L - M \to K + M < L))$
48	47	com23	$⊢ K \in ℕ_{0} \to (K < L - M \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to K + M < L))$
49	48	imp	$⊢ (K \in ℕ_{0} \land K < L - M) \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to K + M < L)$
50	49	3adant2	$⊢ (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to K + M < L)$
51	50	impcom	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \land (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M)) \to K + M < L$
52	11 39 51	3jca	$⊢ ((M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \land (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M)) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L)$
53	52	ex	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L))$
54	53	a1d	$⊢ (M \in ℕ_{0} \land L \in ℕ_{0} \land M \leq L) \to (N \in (L \dots L + \|B\|) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L)))$
55	5 54	sylbi	$⊢ M \in (0 \dots L) \to (N \in (L \dots L + \|B\|) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L)))$
56	55	imp	$⊢ (M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L))$
57	56	2a1i	$⊢ \|A\| = L \to (L \in ℕ_{0} \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L))))$
58		eleq1	$⊢ \|A\| = L \to (\|A\| \in ℕ_{0} \leftrightarrow L \in ℕ_{0})$
59		eleq1	$⊢ \|A\| = L \to (\|A\| \in ℕ \leftrightarrow L \in ℕ)$
60		breq2	$⊢ \|A\| = L \to (K + M < \|A\| \leftrightarrow K + M < L)$
61	59 60	3anbi23d	$⊢ \|A\| = L \to ((K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|) \leftrightarrow (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L))$
62	61	imbi2d	$⊢ \|A\| = L \to (((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|)) \leftrightarrow ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L)))$
63	62	imbi2d	$⊢ \|A\| = L \to (((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|))) \leftrightarrow ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land L \in ℕ \land K + M < L))))$
64	57 58 63	3imtr4d	$⊢ \|A\| = L \to (\|A\| \in ℕ_{0} \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|))))$
65	64	eqcoms	$⊢ L = \|A\| \to (\|A\| \in ℕ_{0} \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|))))$
66	1 4 65	mpsyl	$⊢ A \in Word V \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|)))$
67	66	adantr	$⊢ (A \in Word V \land B \in Word V) \to ((M \in (0 \dots L) \land N \in (L \dots L + \|B\|)) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|)))$
68	67	imp	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|))$
69	68	com12	$⊢ (K \in ℕ_{0} \land L - M \in ℕ \land K < L - M) \to (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|))$
70	3 69	sylbi	$⊢ K \in (0 ..^L - M) \to (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|))$
71	70	adantl	$⊢ (K \in (0 ..^N - M) \land K \in (0 ..^L - M)) \to (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|))$
72	71	impcom	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|)$
73		elfzo0	$⊢ K + M \in (0 ..^\|A\|) \leftrightarrow (K + M \in ℕ_{0} \land \|A\| \in ℕ \land K + M < \|A\|)$
74	72 73	sylibr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to K + M \in (0 ..^\|A\|)$
75		df-3an	$⊢ (A \in Word V \land B \in Word V \land K + M \in (0 ..^\|A\|)) \leftrightarrow ((A \in Word V \land B \in Word V) \land K + M \in (0 ..^\|A\|))$
76	2 74 75	sylanbrc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to (A \in Word V \land B \in Word V \land K + M \in (0 ..^\|A\|))$
77		ccatval1	$⊢ (A \in Word V \land B \in Word V \land K + M \in (0 ..^\|A\|)) \to (A ++ B) (K + M) = A (K + M)$
78	76 77	syl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to (A ++ B) (K + M) = A (K + M)$
79	1	pfxccatin12lem2c	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to (A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|))$
80		simpl	$⊢ (K \in (0 ..^N - M) \land K \in (0 ..^L - M)) \to K \in (0 ..^N - M)$
81		swrdfv	$⊢ ((A ++ B \in Word V \land M \in (0 \dots N) \land N \in (0 \dots \|A ++ B\|)) \land K \in (0 ..^N - M)) \to ((A ++ B) substr ⟨M, N⟩) (K) = (A ++ B) (K + M)$
82	79 80 81	syl2an	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to ((A ++ B) substr ⟨M, N⟩) (K) = (A ++ B) (K + M)$
83		simplll	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to A \in Word V$
84		simplrl	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to M \in (0 \dots L)$
85	1	eleq1i	$⊢ L \in ℕ_{0} \leftrightarrow \|A\| \in ℕ_{0}$
86		elnn0uz	$⊢ L \in ℕ_{0} \leftrightarrow L \in ℤ_{\geq 0}$
87		eluzfz2	$⊢ L \in ℤ_{\geq 0} \to L \in (0 \dots L)$
88	86 87	sylbi	$⊢ L \in ℕ_{0} \to L \in (0 \dots L)$
89	1	oveq2i	$⊢ (0 \dots L) = (0 \dots \|A\|)$
90	88 89	eleqtrdi	$⊢ L \in ℕ_{0} \to L \in (0 \dots \|A\|)$
91	85 90	sylbir	$⊢ \|A\| \in ℕ_{0} \to L \in (0 \dots \|A\|)$
92	4 91	syl	$⊢ A \in Word V \to L \in (0 \dots \|A\|)$
93	92	ad3antrrr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to L \in (0 \dots \|A\|)$
94		simprr	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to K \in (0 ..^L - M)$
95		swrdfv	$⊢ ((A \in Word V \land M \in (0 \dots L) \land L \in (0 \dots \|A\|)) \land K \in (0 ..^L - M)) \to (A substr ⟨M, L⟩) (K) = A (K + M)$
96	83 84 93 94 95	syl31anc	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to (A substr ⟨M, L⟩) (K) = A (K + M)$
97	78 82 96	3eqtr4d	$⊢ (((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \land (K \in (0 ..^N - M) \land K \in (0 ..^L - M))) \to ((A ++ B) substr ⟨M, N⟩) (K) = (A substr ⟨M, L⟩) (K)$
98	97	ex	$⊢ ((A \in Word V \land B \in Word V) \land (M \in (0 \dots L) \land N \in (L \dots L + \|B\|))) \to ((K \in (0 ..^N - M) \land K \in (0 ..^L - M)) \to ((A ++ B) substr ⟨M, N⟩) (K) = (A substr ⟨M, L⟩) (K))$

Metamath Proof Explorer

Theorem pfxccatin12lem3

Proof