Theorem swrdspsleq 11120

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.)

Assertion

Ref	Expression
swrdspsleq	⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))

Distinct variable groups:   𝑖,𝑀   𝑖,𝑁   𝑈,𝑖   𝑖,𝑉   𝑖,𝑊

Proof of Theorem swrdspsleq

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		swrdsb0eq 11118	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝑀) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
2	1	3expa 1206	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) ∧ 𝑁 ≤ 𝑀) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
3	2	ancoms 268	. . . . 5 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
4	3	3adantr3 1161	. . . 4 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
5		ral0 3562	. . . . . . . 8 ⊢ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑈‘𝑖)
6		nn0z 9392	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ)
7		nn0z 9392	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
8		fzon 10289	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
9	6, 7, 8	syl2an 289	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
10	9	biimpa 296	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝑀) → (𝑀..^𝑁) = ∅)
11	10	raleqdv 2708	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝑀) → (∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑈‘𝑖)))
12	5, 11	mpbiri 168	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝑀) → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))
13	12	ex 115	. . . . . 6 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 ≤ 𝑀 → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
14	13	3ad2ant2 1022	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑁 ≤ 𝑀 → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
15	14	impcom 125	. . . 4 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))
16	4, 15	2thd 175	. . 3 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
17	16	ancoms 268	. 2 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑁 ≤ 𝑀) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
18		simp1l 1024	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑊 ∈ Word 𝑉)
19		simp2l 1026	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ ℕ0)
20	19	nn0zd 9493	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ ℤ)
21		simp2r 1027	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑁 ∈ ℕ0)
22	21	nn0zd 9493	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑁 ∈ ℤ)
23		swrdclg 11103	. . . . . . 7 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
24	18, 20, 22, 23	syl3anc 1250	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
25		simp1r 1025	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑈 ∈ Word 𝑉)
26		swrdclg 11103	. . . . . . 7 ⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑈 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
27	25, 20, 22, 26	syl3anc 1250	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑈 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
28		eqwrd 11034	. . . . . 6 ⊢ (((𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉 ∧ (𝑈 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
29	24, 27, 28	syl2anc 411	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
30	29	adantl 277	. . . 4 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
31		swrdsbslen 11119	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)))
32	31	adantl 277	. . . . 5 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)))
33	32	biantrurd 305	. . . 4 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
34		zltnle 9418	. . . . . . . 8 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
35	20, 22, 34	syl2anc 411	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
36	19	nn0red 9349	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ ℝ)
37	21	nn0red 9349	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑁 ∈ ℝ)
38		ltle 8160	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
39	36, 37, 38	syl2anc 411	. . . . . . 7 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
40	35, 39	sylbird 170	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
41		simpl1l 1051	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑊 ∈ Word 𝑉)
42		simpl2l 1053	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℕ0)
43	6, 7	anim12i 338	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
44	43	3ad2ant2 1022	. . . . . . . . . . . . . . 15 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
45	44	anim1i 340	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁))
46		df-3an 983	. . . . . . . . . . . . . 14 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁))
47	45, 46	sylibr 134	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
48		eluz2 9654	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
49	47, 48	sylibr 134	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ (ℤ≥‘𝑀))
50	42, 49	jca 306	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)))
51		simpl3l 1055	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑊))
52		swrdlen2 11115	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁 − 𝑀))
53	41, 50, 51, 52	syl3anc 1250	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁 − 𝑀))
54	53	oveq2d 5960	. . . . . . . . 9 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩))) = (0..^(𝑁 − 𝑀)))
55	54	raleqdv 2708	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
56		0zd 9384	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 0 ∈ ℤ)
57		zsubcl 9413	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ)
58	7, 6, 57	syl2anr 290	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑁 − 𝑀) ∈ ℤ)
59	58	3ad2ant2 1022	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑁 − 𝑀) ∈ ℤ)
60	6	adantr 276	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → 𝑀 ∈ ℤ)
61	60	3ad2ant2 1022	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ ℤ)
62		fzoshftral 10367	. . . . . . . . . 10 ⊢ ((0 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
63	56, 59, 61, 62	syl3anc 1250	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
64	63	adantr 276	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
65		nn0cn 9305	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ)
66		nn0cn 9305	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ)
67		addlid 8211	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ ℂ → (0 + 𝑀) = 𝑀)
68	67	adantl 277	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 + 𝑀) = 𝑀)
69		npcan 8281	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑁 − 𝑀) + 𝑀) = 𝑁)
70	68, 69	oveq12d 5962	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
71	65, 66, 70	syl2anr 290	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
72	71	3ad2ant2 1022	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
73	72	adantr 276	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
74	73	raleqdv 2708	. . . . . . . . 9 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
75		elfzoelz 10269	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ (𝑀..^𝑁) → 𝑖 ∈ ℤ)
76	75	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑖 ∈ ℤ)
77	20	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → 𝑀 ∈ ℤ)
78	76, 77	zsubcld 9500	. . . . . . . . . . . . 13 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 − 𝑀) ∈ ℤ)
79	78	elexd 2785	. . . . . . . . . . . 12 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → (𝑖 − 𝑀) ∈ V)
80		sbceqg 3109	. . . . . . . . . . . . 13 ⊢ ((𝑖 − 𝑀) ∈ V → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
81		csbfvg 5616	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
82		csbfvg 5616	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
83	81, 82	eqeq12d 2220	. . . . . . . . . . . . 13 ⊢ ((𝑖 − 𝑀) ∈ V → (⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀))))
84	80, 83	bitrd 188	. . . . . . . . . . . 12 ⊢ ((𝑖 − 𝑀) ∈ V → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀))))
85	79, 84	syl 14	. . . . . . . . . . 11 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀))))
86	41, 50, 51	3jca 1180	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)))
87		swrdfv2 11116	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑊‘𝑖))
88	86, 87	sylan 283	. . . . . . . . . . . 12 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑊‘𝑖))
89		simpl1r 1052	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑈 ∈ Word 𝑉)
90		simpl3r 1056	. . . . . . . . . . . . . 14 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑈))
91	89, 50, 90	3jca 1180	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈)))
92		swrdfv2 11116	. . . . . . . . . . . . 13 ⊢ (((𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑈‘𝑖))
93	91, 92	sylan 283	. . . . . . . . . . . 12 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑈‘𝑖))
94	88, 93	eqeq12d 2220	. . . . . . . . . . 11 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → (((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) ↔ (𝑊‘𝑖) = (𝑈‘𝑖)))
95	85, 94	bitrd 188	. . . . . . . . . 10 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ (𝑊‘𝑖) = (𝑈‘𝑖)))
96	95	ralbidva 2502	. . . . . . . . 9 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ (𝑀..^𝑁)[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
97	74, 96	bitrd 188	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
98	55, 64, 97	3bitrd 214	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
99	98	ex 115	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑀 ≤ 𝑁 → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))))
100	40, 99	syld 45	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))))
101	100	impcom 125	. . . 4 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
102	30, 33, 101	3bitr2d 216	. . 3 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
103	102	ancoms 268	. 2 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ ¬ 𝑁 ≤ 𝑀) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
104	44	simprd 114	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑁 ∈ ℤ)
105		zdcle 9449	. . . 4 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑁 ≤ 𝑀)
106	104, 61, 105	syl2anc 411	. . 3 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → DECID 𝑁 ≤ 𝑀)
107		exmiddc 838	. . 3 ⊢ (DECID 𝑁 ≤ 𝑀 → (𝑁 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝑀))
108	106, 107	syl 14	. 2 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑁 ≤ 𝑀 ∨ ¬ 𝑁 ≤ 𝑀))
109	17, 103, 108	mpjaodan 800	1 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 710  DECID wdc 836   ∧ w3a 981   = wceq 1373   ∈ wcel 2176  ∀wral 2484  Vcvv 2772  [wsbc 2998  ⦋csb 3093  ∅c0 3460  ⟨cop 3636   class class class wbr 4044  ‘cfv 5271  (class class class)co 5944  ℂcc 7923  ℝcr 7924  0cc0 7925   + caddc 7928   < clt 8107   ≤ cle 8108   − cmin 8243  ℕ₀cn0 9295  ℤcz 9372  ℤ_≥cuz 9648  ..^cfzo 10264  ♯chash 10920  Word cword 10994   substr csubstr 11098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-coll 4159  ax-sep 4162  ax-nul 4170  ax-pow 4218  ax-pr 4253  ax-un 4480  ax-setind 4585  ax-iinf 4636  ax-cnex 8016  ax-resscn 8017  ax-1cn 8018  ax-1re 8019  ax-icn 8020  ax-addcl 8021  ax-addrcl 8022  ax-mulcl 8023  ax-addcom 8025  ax-addass 8027  ax-distr 8029  ax-i2m1 8030  ax-0lt1 8031  ax-0id 8033  ax-rnegex 8034  ax-cnre 8036  ax-pre-ltirr 8037  ax-pre-ltwlin 8038  ax-pre-lttrn 8039  ax-pre-apti 8040  ax-pre-ltadd 8041

This theorem depends on definitions:  df-bi 117  df-dc 837  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-nel 2472  df-ral 2489  df-rex 2490  df-reu 2491  df-rab 2493  df-v 2774  df-sbc 2999  df-csb 3094  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3461  df-if 3572  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-iun 3929  df-br 4045  df-opab 4106  df-mpt 4107  df-tr 4143  df-id 4340  df-iord 4413  df-on 4415  df-ilim 4416  df-suc 4418  df-iom 4639  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-rn 4686  df-res 4687  df-ima 4688  df-iota 5232  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-riota 5899  df-ov 5947  df-oprab 5948  df-mpo 5949  df-1st 6226  df-2nd 6227  df-recs 6391  df-frec 6477  df-1o 6502  df-er 6620  df-en 6828  df-dom 6829  df-fin 6830  df-pnf 8109  df-mnf 8110  df-xr 8111  df-ltxr 8112  df-le 8113  df-sub 8245  df-neg 8246  df-inn 9037  df-n0 9296  df-z 9373  df-uz 9649  df-fz 10131  df-fzo 10265  df-ihash 10921  df-word 10995  df-substr 11099

This theorem is referenced by: (None)