2cshwcshw - Metamath Proof Explorer

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

Theorem 2cshwcshw 14888

Description: If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018.) (Revised by AV, 12-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)

**Assertion**
Ref	Expression
2cshwcshw	⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))

Distinct variable groups: 𝑚,𝑛,𝐾 𝑚,𝑁,𝑛 𝑚,𝑉,𝑛 𝑚,𝑋,𝑛 𝑚,𝑌,𝑛 𝑚,𝑍,𝑛

**Proof of Theorem 2cshwcshw**
Step	Hyp	Ref	Expression
1		difelfznle 13689	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ ¬ 𝐾 ≤ 𝑚) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
2	1	3exp 1137	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
3	2	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
4	3	imp 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
5	4	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (¬ 𝐾 ≤ 𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
6	5	com12 33	. . . . . . . . . . . . 13 ⊢ (¬ 𝐾 ≤ 𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
7	6	adantl 487	. . . . . . . . . . . 12 ⊢ ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
8	7	imp 412	. . . . . . . . . . 11 ⊢ (((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
9		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → 𝑌 ∈ Word 𝑉)
10	9	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
11		elfzelz 13570	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ)
12	11	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → 𝐾 ∈ ℤ)
13	12	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
14		elfz2 13560	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
15		zaddcl 12652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 + 𝑁) ∈ ℤ)
16	15	adantrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑚 + 𝑁) ∈ ℤ)
17		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈ ℤ)
18	16, 17	zsubcld 12723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
19	18	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
20		elfzelz 13570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
21	19, 20	syl11 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
22	21	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
23	22	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
24	14, 23	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
25	24	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
26	25	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
27		2cshw 14876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑌 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ ∧ ((𝑚 + 𝑁) − 𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
28	10, 13, 26, 27	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
29	17, 18	zaddcld 12722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
30	29	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
31	30, 20	syl11 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
32	31	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
33	32	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
34	14, 33	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
35	34	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
36	35	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
37		cshwsublen 14859	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌))))
38	10, 36, 37	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌))))
39	28, 38	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌))))
40		elfz2nn0 13665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑁))
41		nn0cn 12532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ ℕ₀ → 𝑚 ∈ ℂ)
42		nn0cn 12532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐾 ∈ ℕ₀ → 𝐾 ∈ ℂ)
43		nn0cn 12532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
44	42, 43	anim12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ))
45		simprl 783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → 𝐾 ∈ ℂ)
46		addcl 11200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑚 + 𝑁) ∈ ℂ)
47	46	adantrl 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝑚 + 𝑁) ∈ ℂ)
48	45, 47	pncan3d 11590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) = (𝑚 + 𝑁))
49	48	oveq1d 7438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = ((𝑚 + 𝑁) − 𝑁))
50		pncan 11481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
51	50	adantrl 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
52	49, 51	eqtrd 2801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
53	41, 44, 52	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑚 ∈ ℕ₀ ∧ (𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
54	53	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 ∈ ℕ₀ → ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
55		elfznn0 13667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ₀)
56	54, 55	syl11 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
57	56	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐾 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀ ∧ 𝐾 ≤ 𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
58	40, 57	sylbi 220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
59	58	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
60		oveq2 7431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((♯‘𝑌) = 𝑁 → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁))
61	60	eqeq1d 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑌) = 𝑁 → (((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = 𝑚 ↔ ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
62	61	imbi2d 343	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑌) = 𝑁 → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
63	62	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
64	63	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
65	59, 64	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = 𝑚))
66	65	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = 𝑚))
67	66	imp 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌)) = 𝑚)
68	67	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (♯‘𝑌))) = (𝑌 cyclShift 𝑚))
69	39, 68	eqtr2d 2802	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
70	69	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
71		oveq1 7430	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
72	71	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
73	70, 72	eqtr4d 2804	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
74	73	exp41 440	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
75	74	com24 96	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
76	75	imp41 431	. . . . . . . . . . . . . . 15 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
77	76	eqeq2d 2777	. . . . . . . . . . . . . 14 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
78	77	biimpd 232	. . . . . . . . . . . . 13 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
79	78	impancom 457	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
80	79	impcom 413	. . . . . . . . . . 11 ⊢ (((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
81		oveq2 7431	. . . . . . . . . . . 12 ⊢ (𝑛 = ((𝑚 + 𝑁) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
82	81	rspceeqv 3607	. . . . . . . . . . 11 ⊢ ((((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
83	8, 80, 82	syl2anc 596	. . . . . . . . . 10 ⊢ (((¬ 𝑚 = 0 ∧ ¬ 𝐾 ≤ 𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
84	83	exp31 425	. . . . . . . . 9 ⊢ (¬ 𝑚 = 0 → (¬ 𝐾 ≤ 𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
85		oveq2 7431	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 0 → (𝑌 cyclShift 𝑚) = (𝑌 cyclShift 0))
86	85	eqeq2d 2777	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑌 cyclShift 0)))
87		cshw0 14857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑌 ∈ Word 𝑉 → (𝑌 cyclShift 0) = 𝑌)
88	87	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → (𝑌 cyclShift 0) = 𝑌)
89	88	eqeq2d 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) ↔ 𝑍 = 𝑌))
90		fznn0sub2 13682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁 − 𝐾) ∈ (0...𝑁))
91	90	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (𝑁 − 𝐾) ∈ (0...𝑁))
92		oveq1 7430	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((♯‘𝑌) = 𝑁 → ((♯‘𝑌) − 𝐾) = (𝑁 − 𝐾))
93	92	eleq1d 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((♯‘𝑌) = 𝑁 → (((♯‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁 − 𝐾) ∈ (0...𝑁)))
94	93	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (((♯‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁 − 𝐾) ∈ (0...𝑁)))
95	91, 94	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((♯‘𝑌) − 𝐾) ∈ (0...𝑁))
96	95	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((♯‘𝑌) − 𝐾) ∈ (0...𝑁))
97		oveq1 7430	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((♯‘𝑌) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((♯‘𝑌) − 𝐾)))
98		simpl 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → 𝑌 ∈ Word 𝑉)
99		2cshwid 14877	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑌 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((♯‘𝑌) − 𝐾)) = 𝑌)
100	98, 11, 99	syl2an 608	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((♯‘𝑌) − 𝐾)) = 𝑌)
101	97, 100	sylan9eqr 2823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((♯‘𝑌) − 𝐾)) = 𝑌)
102	101	eqcomd 2772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → 𝑌 = (𝑋 cyclShift ((♯‘𝑌) − 𝐾)))
103		oveq2 7431	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = ((♯‘𝑌) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((♯‘𝑌) − 𝐾)))
104	103	rspceeqv 3607	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((♯‘𝑌) − 𝐾) ∈ (0...𝑁) ∧ 𝑌 = (𝑋 cyclShift ((♯‘𝑌) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
105	96, 102, 104	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
106	105	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
107		eqeq1 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑍 = 𝑌 → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑌 = (𝑋 cyclShift 𝑛)))
108	107	rexbidv 3192	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑍 = 𝑌 → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
109	108	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
110	106, 109	mpbird 260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
111	110	exp41 440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = 𝑌 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
112	111	com24 96	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → (𝑍 = 𝑌 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
113	89, 112	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
114	113	com24 96	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
115	114	impcom 413	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
116	115	com13 89	. . . . . . . . . . . . . . 15 ⊢ (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
117	116	a1d 26	. . . . . . . . . . . . . 14 ⊢ (𝑍 = (𝑌 cyclShift 0) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
118	86, 117	biimtrdi 256	. . . . . . . . . . . . 13 ⊢ (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
119	118	com24 96	. . . . . . . . . . . 12 ⊢ (𝑚 = 0 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
120	119	com15 102	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
121	120	imp41 431	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
122	121	com12 33	. . . . . . . . 9 ⊢ (𝑚 = 0 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
123		difelfzle 13688	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ 𝐾 ≤ 𝑚) → (𝑚 − 𝐾) ∈ (0...𝑁))
124	123	3exp 1137	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁))))
125	124	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁))))
126	125	imp 412	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁)))
127	126	adantr 486	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾 ≤ 𝑚 → (𝑚 − 𝐾) ∈ (0...𝑁)))
128	127	impcom 413	. . . . . . . . . . 11 ⊢ ((𝐾 ≤ 𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → (𝑚 − 𝐾) ∈ (0...𝑁))
129	9	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
130	12	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
131		zsubcl 12654	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 − 𝐾) ∈ ℤ)
132	131	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ ℤ → (𝐾 ∈ ℤ → (𝑚 − 𝐾) ∈ ℤ))
133	20, 11, 132	syl2imc 42	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝑚 − 𝐾) ∈ ℤ))
134	133	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑚 − 𝐾) ∈ ℤ))
135	134	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚 − 𝐾) ∈ ℤ)
136		2cshw 14876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑌 ∈ Word 𝑉 ∧ 𝐾 ∈ ℤ ∧ (𝑚 − 𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚 − 𝐾))))
137	129, 130, 135, 136	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚 − 𝐾))))
138		zcn 12614	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
139	20	zcnd 12719	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℂ)
140		pncan3 11483	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝐾 + (𝑚 − 𝐾)) = 𝑚)
141	138, 139, 140	syl2anr 609	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑚 ∈ (0...𝑁) ∧ 𝐾 ∈ ℤ) → (𝐾 + (𝑚 − 𝐾)) = 𝑚)
142	141	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑚 ∈ (0...𝑁) → (𝐾 ∈ ℤ → (𝐾 + (𝑚 − 𝐾)) = 𝑚))
143	11, 142	syl5com 32	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚 − 𝐾)) = 𝑚))
144	143	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚 − 𝐾)) = 𝑚))
145	144	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + (𝑚 − 𝐾)) = 𝑚)
146	145	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + (𝑚 − 𝐾))) = (𝑌 cyclShift 𝑚))
147	137, 146	eqtr2d 2802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)))
148	147	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)))
149		oveq1 7430	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift (𝑚 − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾)))
150	149	eqeq2d 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑋 = (𝑌 cyclShift 𝐾) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚 − 𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾))))
151	150	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚 − 𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚 − 𝐾))))
152	148, 151	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚 − 𝐾)))
153	152	eqeq2d 2777	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))))
154	153	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝐾 ≤ 𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))))
155	154	exp41 440	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝐾 ≤ 𝑚 → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))))
156	155	com24 96	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝐾 ≤ 𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))))
157	156	imp31 423	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 ≤ 𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))
158	157	com23 87	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝐾 ≤ 𝑚 → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))))
159	158	imp 412	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾 ≤ 𝑚 → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))))
160	159	impcom 413	. . . . . . . . . . 11 ⊢ ((𝐾 ≤ 𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾)))
161		oveq2 7431	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑚 − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift (𝑚 − 𝐾)))
162	161	rspceeqv 3607	. . . . . . . . . . 11 ⊢ (((𝑚 − 𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift (𝑚 − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
163	128, 160, 162	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝐾 ≤ 𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
164	163	ex 418	. . . . . . . . 9 ⊢ (𝐾 ≤ 𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
165	84, 122, 164	pm2.61ii 185	. . . . . . . 8 ⊢ (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
166	165	rexlimdva2 3171	. . . . . . 7 ⊢ (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
167	166	ex 418	. . . . . 6 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
168	167	com23 87	. . . . 5 ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
169	168	ex 418	. . . 4 ⊢ (𝐾 ∈ (0...𝑁) → ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
170	169	com24 96	. . 3 ⊢ (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
171	170	3imp 1128	. 2 ⊢ ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
172	171	com12 33	1 ⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ∃wrex 3092 class class class wbr 5114 ‘cfv 6543 (class class class)co 7423 ℂcc 11116 0cc0 11118 + caddc 11121 ≤ cle 11262 − cmin 11459 ℕ₀cn0 12522 ℤcz 12609 ...cfz 13553 ♯chash 14386 Word cword 14570 cyclShift ccsh 14851

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-inf 9413 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-n0 12523 df-z 12610 df-uz 12881 df-rp 13035 df-fz 13554 df-fzo 13702 df-fl 13845 df-mod 13923 df-hash 14387 df-word 14571 df-concat 14628 df-substr 14701 df-pfx 14733 df-csh 14852

This theorem is used by: eleclclwwlknlem1 30448

W3C validator