swrdspsleq

Description: Two words have a common subword (starting at the same position with the same length) iff they have the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018) (Proof shortened by AV, 7-May-2020)

		Ref	Expression
	Assertion	swrdspsleq	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$

Proof

Step	Hyp	Ref	Expression
1		swrdsb0eq	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to W substr ⟨M, N⟩ = U substr ⟨M, N⟩$
2	1	3expa	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0})) \land N \leq M) \to W substr ⟨M, N⟩ = U substr ⟨M, N⟩$
3	2	ancoms	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}))) \to W substr ⟨M, N⟩ = U substr ⟨M, N⟩$
4	3	3adantr3	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to W substr ⟨M, N⟩ = U substr ⟨M, N⟩$
5		ral0	$⊢ \forall i \in \emptyset W (i) = U (i)$
6		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
7		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
8		fzon	$⊢ (M \in ℤ \land N \in ℤ) \to (N \leq M \leftrightarrow (M ..^N) = \emptyset)$
9	6 7 8	syl2an	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq M \leftrightarrow (M ..^N) = \emptyset)$
10	9	biimpa	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to (M ..^N) = \emptyset$
11	10	raleqdv	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to (\forall i \in (M ..^N) W (i) = U (i) \leftrightarrow \forall i \in \emptyset W (i) = U (i))$
12	5 11	mpbiri	$⊢ ((M \in ℕ_{0} \land N \in ℕ_{0}) \land N \leq M) \to \forall i \in (M ..^N) W (i) = U (i)$
13	12	ex	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (N \leq M \to \forall i \in (M ..^N) W (i) = U (i))$
14	13	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (N \leq M \to \forall i \in (M ..^N) W (i) = U (i))$
15	14	impcom	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to \forall i \in (M ..^N) W (i) = U (i)$
16	4 15	2thd	$⊢ (N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$
17		swrdcl	$⊢ W \in Word V \to W substr ⟨M, N⟩ \in Word V$
18		swrdcl	$⊢ U \in Word V \to U substr ⟨M, N⟩ \in Word V$
19		eqwrd	$⊢ (W substr ⟨M, N⟩ \in Word V \land U substr ⟨M, N⟩ \in Word V) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow (\|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\| \land \forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j)))$
20	17 18 19	syl2an	$⊢ (W \in Word V \land U \in Word V) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow (\|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\| \land \forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j)))$
21	20	3ad2ant1	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow (\|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\| \land \forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j)))$
22	21	adantl	$⊢ (\neg N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow (\|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\| \land \forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j)))$
23		swrdsbslen	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|$
24	23	adantl	$⊢ (\neg N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to \|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\|$
25	24	biantrurd	$⊢ (\neg N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to (\forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow (\|W substr ⟨M, N⟩\| = \|U substr ⟨M, N⟩\| \land \forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j)))$
26		nn0re	$⊢ M \in ℕ_{0} \to M \in ℝ$
27		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
28		ltnle	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \leftrightarrow \neg N \leq M)$
29		ltle	$⊢ (M \in ℝ \land N \in ℝ) \to (M < N \to M \leq N)$
30	28 29	sylbird	$⊢ (M \in ℝ \land N \in ℝ) \to (\neg N \leq M \to M \leq N)$
31	26 27 30	syl2an	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (\neg N \leq M \to M \leq N)$
32	31	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (\neg N \leq M \to M \leq N)$
33		simpl1l	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to W \in Word V$
34		simpl2l	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to M \in ℕ_{0}$
35	6 7	anim12i	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (M \in ℤ \land N \in ℤ)$
36	35	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (M \in ℤ \land N \in ℤ)$
37	36	anim1i	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to ((M \in ℤ \land N \in ℤ) \land M \leq N)$
38		df-3an	$⊢ (M \in ℤ \land N \in ℤ \land M \leq N) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land M \leq N)$
39	37 38	sylibr	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (M \in ℤ \land N \in ℤ \land M \leq N)$
40		eluz2	$⊢ N \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land N \in ℤ \land M \leq N)$
41	39 40	sylibr	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to N \in ℤ_{\geq M}$
42	34 41	jca	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (M \in ℕ_{0} \land N \in ℤ_{\geq M})$
43		simpl3l	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to N \leq \|W\|$
44		swrdlen2	$⊢ (W \in Word V \land (M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land N \leq \|W\|) \to \|W substr ⟨M, N⟩\| = N - M$
45	33 42 43 44	syl3anc	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to \|W substr ⟨M, N⟩\| = N - M$
46	45	oveq2d	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (0 ..^\|W substr ⟨M, N⟩\|) = (0 ..^N - M)$
47	46	raleqdv	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (\forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall j \in (0 ..^N - M) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j))$
48		0zd	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to 0 \in ℤ$
49		zsubcl	$⊢ (N \in ℤ \land M \in ℤ) \to N - M \in ℤ$
50	7 6 49	syl2anr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to N - M \in ℤ$
51	50	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to N - M \in ℤ$
52	6	adantr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to M \in ℤ$
53	52	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to M \in ℤ$
54		fzoshftral	$⊢ (0 \in ℤ \land N - M \in ℤ \land M \in ℤ) \to (\forall j \in (0 ..^N - M) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (0 + M ..^N - M + M) \underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j))$
55	48 51 53 54	syl3anc	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (\forall j \in (0 ..^N - M) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (0 + M ..^N - M + M) \underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j))$
56	55	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (\forall j \in (0 ..^N - M) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (0 + M ..^N - M + M) \underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j))$
57		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
58		nn0cn	$⊢ M \in ℕ_{0} \to M \in ℂ$
59		addid2	$⊢ M \in ℂ \to 0 + M = M$
60	59	adantl	$⊢ (N \in ℂ \land M \in ℂ) \to 0 + M = M$
61		npcan	$⊢ (N \in ℂ \land M \in ℂ) \to N - M + M = N$
62	60 61	oveq12d	$⊢ (N \in ℂ \land M \in ℂ) \to (0 + M ..^N - M + M) = (M ..^N)$
63	57 58 62	syl2anr	$⊢ (M \in ℕ_{0} \land N \in ℕ_{0}) \to (0 + M ..^N - M + M) = (M ..^N)$
64	63	3ad2ant2	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (0 + M ..^N - M + M) = (M ..^N)$
65	64	adantr	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (0 + M ..^N - M + M) = (M ..^N)$
66	65	raleqdv	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (\forall i \in (0 + M ..^N - M + M) \underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (M ..^N) \underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j))$
67		ovex	$⊢ i - M \in V$
68		sbceqg	$⊢ i - M \in V \to (\underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow ⦋ (i - M) / j ⦌ (W substr ⟨M, N⟩) (j) = ⦋ (i - M) / j ⦌ (U substr ⟨M, N⟩) (j))$
69		csbfv2g	$⊢ i - M \in V \to ⦋ (i - M) / j ⦌ (W substr ⟨M, N⟩) (j) = (W substr ⟨M, N⟩) (⦋ (i - M) / j ⦌ j)$
70		csbvarg	$⊢ i - M \in V \to ⦋ (i - M) / j ⦌ j = i - M$
71	70	fveq2d	$⊢ i - M \in V \to (W substr ⟨M, N⟩) (⦋ (i - M) / j ⦌ j) = (W substr ⟨M, N⟩) (i - M)$
72	69 71	eqtrd	$⊢ i - M \in V \to ⦋ (i - M) / j ⦌ (W substr ⟨M, N⟩) (j) = (W substr ⟨M, N⟩) (i - M)$
73		csbfv2g	$⊢ i - M \in V \to ⦋ (i - M) / j ⦌ (U substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (⦋ (i - M) / j ⦌ j)$
74	70	fveq2d	$⊢ i - M \in V \to (U substr ⟨M, N⟩) (⦋ (i - M) / j ⦌ j) = (U substr ⟨M, N⟩) (i - M)$
75	73 74	eqtrd	$⊢ i - M \in V \to ⦋ (i - M) / j ⦌ (U substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (i - M)$
76	72 75	eqeq12d	$⊢ i - M \in V \to (⦋ (i - M) / j ⦌ (W substr ⟨M, N⟩) (j) = ⦋ (i - M) / j ⦌ (U substr ⟨M, N⟩) (j) \leftrightarrow (W substr ⟨M, N⟩) (i - M) = (U substr ⟨M, N⟩) (i - M))$
77	68 76	bitrd	$⊢ i - M \in V \to (\underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow (W substr ⟨M, N⟩) (i - M) = (U substr ⟨M, N⟩) (i - M))$
78	67 77	mp1i	$⊢ ((((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \land i \in (M ..^N)) \to (\underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow (W substr ⟨M, N⟩) (i - M) = (U substr ⟨M, N⟩) (i - M))$
79	33 42 43	3jca	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (W \in Word V \land (M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land N \leq \|W\|)$
80		swrdfv2	$⊢ ((W \in Word V \land (M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land N \leq \|W\|) \land i \in (M ..^N)) \to (W substr ⟨M, N⟩) (i - M) = W (i)$
81	79 80	sylan	$⊢ ((((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \land i \in (M ..^N)) \to (W substr ⟨M, N⟩) (i - M) = W (i)$
82		simpl1r	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to U \in Word V$
83		simpl3r	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to N \leq \|U\|$
84	82 42 83	3jca	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (U \in Word V \land (M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land N \leq \|U\|)$
85		swrdfv2	$⊢ ((U \in Word V \land (M \in ℕ_{0} \land N \in ℤ_{\geq M}) \land N \leq \|U\|) \land i \in (M ..^N)) \to (U substr ⟨M, N⟩) (i - M) = U (i)$
86	84 85	sylan	$⊢ ((((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \land i \in (M ..^N)) \to (U substr ⟨M, N⟩) (i - M) = U (i)$
87	81 86	eqeq12d	$⊢ ((((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \land i \in (M ..^N)) \to ((W substr ⟨M, N⟩) (i - M) = (U substr ⟨M, N⟩) (i - M) \leftrightarrow W (i) = U (i))$
88	78 87	bitrd	$⊢ ((((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \land i \in (M ..^N)) \to (\underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow W (i) = U (i))$
89	88	ralbidva	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (\forall i \in (M ..^N) \underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$
90	66 89	bitrd	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (\forall i \in (0 + M ..^N - M + M) \underset{˙}{[} (i - M) / j \underset{˙}{]} (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$
91	47 56 90	3bitrd	$⊢ (((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \land M \leq N) \to (\forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$
92	91	ex	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (M \leq N \to (\forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (M ..^N) W (i) = U (i)))$
93	32 92	syld	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (\neg N \leq M \to (\forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (M ..^N) W (i) = U (i)))$
94	93	impcom	$⊢ (\neg N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to (\forall j \in (0 ..^\|W substr ⟨M, N⟩\|) (W substr ⟨M, N⟩) (j) = (U substr ⟨M, N⟩) (j) \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$
95	22 25 94	3bitr2d	$⊢ (\neg N \leq M \land ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|))) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$
96	16 95	pm2.61ian	$⊢ ((W \in Word V \land U \in Word V) \land (M \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|W\| \land N \leq \|U\|)) \to (W substr ⟨M, N⟩ = U substr ⟨M, N⟩ \leftrightarrow \forall i \in (M ..^N) W (i) = U (i))$

Metamath Proof Explorer

Theorem swrdspsleq

Proof