swrdspsleq - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > swrdspsleq		Structured version Visualization version GIF version

Theorem swrdspsleq 14630

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 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))

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

Proof of Theorem swrdspsleq Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		swrdsb0eq 14628	. . . . . 6 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑀) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
2	1	3expa 1118	. . . . 5 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) ∧ 𝑁 ≤ 𝑀) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
3	2	ancoms 458	. . . 4 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀))) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
4	3	3adantr3 1172	. . 3 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
5		ral0 4476	. . . . . . 7 ⊢ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑈‘𝑖)
6		nn0z 12554	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℤ)
7		nn0z 12554	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
8		fzon 13641	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
9	6, 7, 8	syl2an 596	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
10	9	biimpa 476	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑀) → (𝑀..^𝑁) = ∅)
11	10	raleqdv 3299	. . . . . . 7 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑀) → (∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖) ↔ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑈‘𝑖)))
12	5, 11	mpbiri 258	. . . . . 6 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑀) → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))
13	12	ex 412	. . . . 5 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 𝑀 → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
14	13	3ad2ant2 1134	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑁 ≤ 𝑀 → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
15	14	impcom 407	. . 3 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))
16	4, 15	2thd 265	. 2 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
17		swrdcl 14610	. . . . . 6 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
18		swrdcl 14610	. . . . . 6 ⊢ (𝑈 ∈ Word 𝑉 → (𝑈 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
19		eqwrd 14522	. . . . . 6 ⊢ (((𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉 ∧ (𝑈 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
20	17, 18, 19	syl2an 596	. . . . 5 ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
21	20	3ad2ant1 1133	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
22	21	adantl 481	. . 3 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
23		swrdsbslen 14629	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)))
24	23	adantl 481	. . . 4 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)))
25	24	biantrurd 532	. . 3 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)) ∧ ∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗))))
26		nn0re 12451	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℝ)
27		nn0re 12451	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
28		ltnle 11253	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
29		ltle 11262	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
30	28, 29	sylbird 260	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
31	26, 27, 30	syl2an 596	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
32	31	3ad2ant2 1134	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
33		simpl1l 1225	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑊 ∈ Word 𝑉)
34		simpl2l 1227	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℕ₀)
35	6, 7	anim12i 613	. . . . . . . . . . . . . . 15 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
36	35	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
37	36	anim1i 615	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁))
38		df-3an 1088	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁))
39	37, 38	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
40		eluz2 12799	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
41	39, 40	sylibr 234	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ (ℤ_≥‘𝑀))
42	34, 41	jca 511	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)))
43		simpl3l 1229	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑊))
44		swrdlen2 14625	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁 − 𝑀))
45	33, 42, 43, 44	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁 − 𝑀))
46	45	oveq2d 7403	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩))) = (0..^(𝑁 − 𝑀)))
47	46	raleqdv 3299	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
48		0zd 12541	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 0 ∈ ℤ)
49		zsubcl 12575	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 − 𝑀) ∈ ℤ)
50	7, 6, 49	syl2anr 597	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 − 𝑀) ∈ ℤ)
51	50	3ad2ant2 1134	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑁 − 𝑀) ∈ ℤ)
52	6	adantr 480	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → 𝑀 ∈ ℤ)
53	52	3ad2ant2 1134	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 𝑀 ∈ ℤ)
54		fzoshftral 13745	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
55	48, 51, 53, 54	syl3anc 1373	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
56	55	adantr 480	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
57		nn0cn 12452	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
58		nn0cn 12452	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℂ)
59		addlid 11357	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℂ → (0 + 𝑀) = 𝑀)
60	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 + 𝑀) = 𝑀)
61		npcan 11430	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑁 − 𝑀) + 𝑀) = 𝑁)
62	60, 61	oveq12d 7405	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
63	57, 58, 62	syl2anr 597	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
64	63	3ad2ant2 1134	. . . . . . . . . 10 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
65	64	adantr 480	. . . . . . . . 9 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀)) = (𝑀..^𝑁))
66	65	raleqdv 3299	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
67		ovex 7420	. . . . . . . . . . 11 ⊢ (𝑖 − 𝑀) ∈ V
68		sbceqg 4375	. . . . . . . . . . . 12 ⊢ ((𝑖 − 𝑀) ∈ V → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
69		csbfv2g 6907	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗))
70		csbvarg 4397	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌𝑗 = (𝑖 − 𝑀))
71	70	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
72	69, 71	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
73		csbfv2g 6907	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗))
74	70	fveq2d 6862	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
75	73, 74	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
76	72, 75	eqeq12d 2745	. . . . . . . . . . . 12 ⊢ ((𝑖 − 𝑀) ∈ V → (⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀))))
77	68, 76	bitrd 279	. . . . . . . . . . 11 ⊢ ((𝑖 − 𝑀) ∈ V → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀))))
78	67, 77	mp1i 13	. . . . . . . . . 10 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀))))
79	33, 42, 43	3jca 1128	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)))
80		swrdfv2 14626	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑊‘𝑖))
81	79, 80	sylan 580	. . . . . . . . . . 11 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑊‘𝑖))
82		simpl1r 1226	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑈 ∈ Word 𝑉)
83		simpl3r 1230	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑈))
84	82, 42, 83	3jca 1128	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈)))
85		swrdfv2 14626	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑈‘𝑖))
86	84, 85	sylan 580	. . . . . . . . . . 11 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑈‘𝑖))
87	81, 86	eqeq12d 2745	. . . . . . . . . 10 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → (((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) ↔ (𝑊‘𝑖) = (𝑈‘𝑖)))
88	78, 87	bitrd 279	. . . . . . . . 9 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ (𝑊‘𝑖) = (𝑈‘𝑖)))
89	88	ralbidva 3154	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ (𝑀..^𝑁)[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
90	66, 89	bitrd 279	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
91	47, 56, 90	3bitrd 305	. . . . . 6 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
92	91	ex 412	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (𝑀 ≤ 𝑁 → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))))
93	32, 92	syld 47	. . . 4 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖))))
94	93	impcom 407	. . 3 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
95	22, 25, 94	3bitr2d 307	. 2 ⊢ ((¬ 𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
96	16, 95	pm2.61ian 811	1 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 Vcvv 3447 [wsbc 3753 ⦋csb 3862 ∅c0 4296 ⟨cop 4595 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 ℝcr 11067 0cc0 11068 + caddc 11071 < clt 11208 ≤ cle 11209 − cmin 11405 ℕ₀cn0 12442 ℤcz 12529 ℤ_≥cuz 12793 ..^cfzo 13615 ♯chash 14295 Word cword 14478 substr csubstr 14605

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-nn 12187 df-n0 12443 df-z 12530 df-uz 12794 df-fz 13469 df-fzo 13616 df-hash 14296 df-word 14479 df-substr 14606

This theorem is referenced by: pfxsuffeqwrdeq 14663 clwwlkf1 29978

W3C validator