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 14686

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 14684	. . . . . 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 1171	. . 3 ⊢ ((𝑁 ≤ 𝑀 ∧ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈)))) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
5		ral0 4495	. . . . . . 7 ⊢ ∀𝑖 ∈ ∅ (𝑊‘𝑖) = (𝑈‘𝑖)
6		nn0z 12622	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℤ)
7		nn0z 12622	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
8		fzon 13703	. . . . . . . . . 10 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
9	6, 7, 8	syl2an 596	. . . . . . . . 9 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑁 ≤ 𝑀 ↔ (𝑀..^𝑁) = ∅))
10	9	biimpa 476	. . . . . . . 8 ⊢ (((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ 𝑁 ≤ 𝑀) → (𝑀..^𝑁) = ∅)
11	10	raleqdv 3310	. . . . . . 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 14666	. . . . . 6 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
18		swrdcl 14666	. . . . . 6 ⊢ (𝑈 ∈ Word 𝑉 → (𝑈 substr ⟨𝑀, 𝑁⟩) ∈ Word 𝑉)
19		eqwrd 14578	. . . . . 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 14685	. . . . 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 12519	. . . . . . 7 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℝ)
27		nn0re 12519	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
28		ltnle 11323	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 ↔ ¬ 𝑁 ≤ 𝑀))
29		ltle 11332	. . . . . . . 8 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑀 < 𝑁 → 𝑀 ≤ 𝑁))
30	28, 29	sylbird 260	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
31	26, 27, 30	syl2an 596	. . . . . 6 ⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
32	31	3ad2ant2 1134	. . . . 5 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (¬ 𝑁 ≤ 𝑀 → 𝑀 ≤ 𝑁))
33		simpl1l 1224	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑊 ∈ Word 𝑉)
34		simpl2l 1226	. . . . . . . . . . 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 12867	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))
41	39, 40	sylibr 234	. . . . . . . . . . 11 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ (ℤ_≥‘𝑀))
42	34, 41	jca 511	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)))
43		simpl3l 1228	. . . . . . . . . 10 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑊))
44		swrdlen2 14681	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁 − 𝑀))
45	33, 42, 43, 44	syl3anc 1372	. . . . . . . . 9 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (𝑁 − 𝑀))
46	45	oveq2d 7430	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩))) = (0..^(𝑁 − 𝑀)))
47	46	raleqdv 3310	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
48		0zd 12609	. . . . . . . . 9 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → 0 ∈ ℤ)
49		zsubcl 12643	. . . . . . . . . . 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 13806	. . . . . . . . 9 ⊢ ((0 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
55	48, 51, 53, 54	syl3anc 1372	. . . . . . . 8 ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
56	55	adantr 480	. . . . . . 7 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑗 ∈ (0..^(𝑁 − 𝑀))((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
57		nn0cn 12520	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
58		nn0cn 12520	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ ℕ₀ → 𝑀 ∈ ℂ)
59		addlid 11427	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℂ → (0 + 𝑀) = 𝑀)
60	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (0 + 𝑀) = 𝑀)
61		npcan 11500	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑁 − 𝑀) + 𝑀) = 𝑁)
62	60, 61	oveq12d 7432	. . . . . . . . . . . 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 3310	. . . . . . . 8 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (∀𝑖 ∈ ((0 + 𝑀)..^((𝑁 − 𝑀) + 𝑀))[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ∀𝑖 ∈ (𝑀..^𝑁)[(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
67		ovex 7447	. . . . . . . . . . 11 ⊢ (𝑖 − 𝑀) ∈ V
68		sbceqg 4394	. . . . . . . . . . . 12 ⊢ ((𝑖 − 𝑀) ∈ V → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗)))
69		csbfv2g 6936	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗))
70		csbvarg 4416	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌𝑗 = (𝑖 − 𝑀))
71	70	fveq2d 6891	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
72	69, 71	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
73		csbfv2g 6936	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗))
74	70	fveq2d 6891	. . . . . . . . . . . . . 14 ⊢ ((𝑖 − 𝑀) ∈ V → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘⦋(𝑖 − 𝑀) / 𝑗⦌𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
75	73, 74	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((𝑖 − 𝑀) ∈ V → ⦋(𝑖 − 𝑀) / 𝑗⦌((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)))
76	72, 75	eqeq12d 2750	. . . . . . . . . . . 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 14682	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑊)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑊‘𝑖))
81	79, 80	sylan 580	. . . . . . . . . . 11 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑊‘𝑖))
82		simpl1r 1225	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑈 ∈ Word 𝑉)
83		simpl3r 1229	. . . . . . . . . . . . 13 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → 𝑁 ≤ (♯‘𝑈))
84	82, 42, 83	3jca 1128	. . . . . . . . . . . 12 ⊢ ((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) → (𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈)))
85		swrdfv2 14682	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ Word 𝑉 ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ (ℤ_≥‘𝑀)) ∧ 𝑁 ≤ (♯‘𝑈)) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑈‘𝑖))
86	84, 85	sylan 580	. . . . . . . . . . 11 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = (𝑈‘𝑖))
87	81, 86	eqeq12d 2750	. . . . . . . . . 10 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → (((𝑊 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘(𝑖 − 𝑀)) ↔ (𝑊‘𝑖) = (𝑈‘𝑖)))
88	78, 87	bitrd 279	. . . . . . . . 9 ⊢ (((((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) ∧ 𝑀 ≤ 𝑁) ∧ 𝑖 ∈ (𝑀..^𝑁)) → ([(𝑖 − 𝑀) / 𝑗]((𝑊 substr ⟨𝑀, 𝑁⟩)‘𝑗) = ((𝑈 substr ⟨𝑀, 𝑁⟩)‘𝑗) ↔ (𝑊‘𝑖) = (𝑈‘𝑖)))
89	88	ralbidva 3163	. . . . . . . 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 1539 ∈ wcel 2107 ∀wral 3050 Vcvv 3464 [wsbc 3772 ⦋csb 3881 ∅c0 4315 ⟨cop 4614 class class class wbr 5125 ‘cfv 6542 (class class class)co 7414 ℂcc 11136 ℝcr 11137 0cc0 11138 + caddc 11141 < clt 11278 ≤ cle 11279 − cmin 11475 ℕ₀cn0 12510 ℤcz 12597 ℤ_≥cuz 12861 ..^cfzo 13677 ♯chash 14352 Word cword 14535 substr csubstr 14661

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5261 ax-sep 5278 ax-nul 5288 ax-pow 5347 ax-pr 5414 ax-un 7738 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3773 df-csb 3882 df-dif 3936 df-un 3938 df-in 3940 df-ss 3950 df-pss 3953 df-nul 4316 df-if 4508 df-pw 4584 df-sn 4609 df-pr 4611 df-op 4615 df-uni 4890 df-int 4929 df-iun 4975 df-br 5126 df-opab 5188 df-mpt 5208 df-tr 5242 df-id 5560 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-pred 6303 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6495 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7871 df-1st 7997 df-2nd 7998 df-frecs 8289 df-wrecs 8320 df-recs 8394 df-rdg 8433 df-1o 8489 df-er 8728 df-en 8969 df-dom 8970 df-sdom 8971 df-fin 8972 df-card 9962 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11477 df-neg 11478 df-nn 12250 df-n0 12511 df-z 12598 df-uz 12862 df-fz 13531 df-fzo 13678 df-hash 14353 df-word 14536 df-substr 14662

This theorem is referenced by: pfxsuffeqwrdeq 14719 clwwlkf1 30015

W3C validator