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

Theorem 2cshwcshw 13422
 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
StepHypRef Expression
1 difelfznle 12322 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ ¬ 𝐾𝑚) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
213exp 1256 . . . . . . . . . . . . . . . . . 18 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
32ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))))
43imp 444 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
54adantr 480 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (¬ 𝐾𝑚 → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
65com12 32 . . . . . . . . . . . . . 14 𝐾𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
76adantl 481 . . . . . . . . . . . . 13 ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁)))
87imp 444 . . . . . . . . . . . 12 (((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁))
9 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → 𝑌 ∈ Word 𝑉)
109ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
11 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → 𝐾 ∈ ℤ)
1211adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → 𝐾 ∈ ℤ)
1312ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
14 elfz2 12204 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐾 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾𝐾𝑁)))
15 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℤ)
16 zaddcl 11294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑚 + 𝑁) ∈ ℤ)
1716adantrr 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝑚 + 𝑁) ∈ ℤ)
18 simprr 792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → 𝐾 ∈ ℤ)
1917, 18zsubcld 11363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
2019ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2115, 20syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2221com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
23223adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2423adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾𝐾𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2514, 24sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2625ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ))
2726imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑚 + 𝑁) − 𝐾) ∈ ℤ)
28 2cshw 13410 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑌 ∈ Word 𝑉𝐾 ∈ ℤ ∧ ((𝑚 + 𝑁) − 𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
2910, 13, 27, 28syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))))
3018, 19zaddcld 11362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
3130ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3215, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3332com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
34333adant1 1072 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3534adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (0 ≤ 𝐾𝐾𝑁)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3614, 35sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3736ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑚 ∈ (0...𝑁) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ))
3837imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ)
39 cshwsublen 13393 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑌 ∈ Word 𝑉 ∧ (𝐾 + ((𝑚 + 𝑁) − 𝐾)) ∈ ℤ) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
4010, 38, 39syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + ((𝑚 + 𝑁) − 𝐾))) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
4129, 40eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)) = (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))))
42 elfz2nn0 12300 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁))
43 elfznn0 12302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℕ0)
44 nn0cn 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑚 ∈ ℕ0𝑚 ∈ ℂ)
45 nn0cn 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐾 ∈ ℕ0𝐾 ∈ ℂ)
46 nn0cn 11179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑁 ∈ ℕ0𝑁 ∈ ℂ)
4745, 46anim12i 588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ))
48 simprl 790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → 𝐾 ∈ ℂ)
49 addcl 9897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑚 + 𝑁) ∈ ℂ)
5049adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝑚 + 𝑁) ∈ ℂ)
5148, 50pncan3d 10274 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → (𝐾 + ((𝑚 + 𝑁) − 𝐾)) = (𝑚 + 𝑁))
5251oveq1d 6564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = ((𝑚 + 𝑁) − 𝑁))
53 pncan 10166 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑚 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
5453adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝑚 + 𝑁) − 𝑁) = 𝑚)
5552, 54eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑚 ∈ ℂ ∧ (𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
5644, 47, 55syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑚 ∈ ℕ0 ∧ (𝐾 ∈ ℕ0𝑁 ∈ ℕ0)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)
5756ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑚 ∈ ℕ0 → ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
5843, 57syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑚 ∈ (0...𝑁) → ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
5958com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
60593adant3 1074 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ ℕ0𝑁 ∈ ℕ0𝐾𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
6142, 60sylbi 206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
6261adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
63 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝑌) = 𝑁 → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁))
6463eqeq1d 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑌) = 𝑁 → (((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚 ↔ ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚))
6564imbi2d 329 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝑌) = 𝑁 → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
6665adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
6766adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ((𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚) ↔ (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − 𝑁) = 𝑚)))
6862, 67mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚))
6968adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑚 ∈ (0...𝑁) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚))
7069imp 444 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌)) = 𝑚)
7170oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift ((𝐾 + ((𝑚 + 𝑁) − 𝐾)) − (#‘𝑌))) = (𝑌 cyclShift 𝑚))
7241, 71eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
7372adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
74 oveq1 6556 . . . . . . . . . . . . . . . . . . . . 21 (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
7574adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((𝑚 + 𝑁) − 𝐾)))
7673, 75eqtr4d 2647 . . . . . . . . . . . . . . . . . . 19 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
7776exp41 636 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
7877com24 93 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))))
7978imp41 617 . . . . . . . . . . . . . . . 16 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
8079eqeq2d 2620 . . . . . . . . . . . . . . 15 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
8180biimpd 218 . . . . . . . . . . . . . 14 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ (¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
8281impancom 455 . . . . . . . . . . . . 13 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
8382impcom 445 . . . . . . . . . . . 12 (((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
84 oveq2 6557 . . . . . . . . . . . . . 14 (𝑛 = ((𝑚 + 𝑁) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾)))
8584eqeq2d 2620 . . . . . . . . . . . . 13 (𝑛 = ((𝑚 + 𝑁) − 𝐾) → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))))
8685rspcev 3282 . . . . . . . . . . . 12 ((((𝑚 + 𝑁) − 𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift ((𝑚 + 𝑁) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
878, 83, 86syl2anc 691 . . . . . . . . . . 11 (((¬ 𝑚 = 0 ∧ ¬ 𝐾𝑚) ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
8887exp31 628 . . . . . . . . . 10 𝑚 = 0 → (¬ 𝐾𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
89 oveq2 6557 . . . . . . . . . . . . . . . 16 (𝑚 = 0 → (𝑌 cyclShift 𝑚) = (𝑌 cyclShift 0))
9089eqeq2d 2620 . . . . . . . . . . . . . . 15 (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑌 cyclShift 0)))
91 cshw0 13391 . . . . . . . . . . . . . . . . . . . . . 22 (𝑌 ∈ Word 𝑉 → (𝑌 cyclShift 0) = 𝑌)
9291adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑌 cyclShift 0) = 𝑌)
9392eqeq2d 2620 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) ↔ 𝑍 = 𝑌))
94 fznn0sub2 12315 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐾 ∈ (0...𝑁) → (𝑁𝐾) ∈ (0...𝑁))
9594adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (𝑁𝐾) ∈ (0...𝑁))
96 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝑌) = 𝑁 → ((#‘𝑌) − 𝐾) = (𝑁𝐾))
9796eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝑌) = 𝑁 → (((#‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁𝐾) ∈ (0...𝑁)))
9897ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → (((#‘𝑌) − 𝐾) ∈ (0...𝑁) ↔ (𝑁𝐾) ∈ (0...𝑁)))
9995, 98mpbird 246 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((#‘𝑌) − 𝐾) ∈ (0...𝑁))
10099adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((#‘𝑌) − 𝐾) ∈ (0...𝑁))
101 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift ((#‘𝑌) − 𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)))
102 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → 𝑌 ∈ Word 𝑉)
103 2cshwid 13411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑌 ∈ Word 𝑉𝐾 ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
104102, 11, 103syl2an 493 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
105101, 104sylan9eqr 2666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑋 cyclShift ((#‘𝑌) − 𝐾)) = 𝑌)
106105eqcomd 2616 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾)))
107 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑛 = ((#‘𝑌) − 𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift ((#‘𝑌) − 𝐾)))
108107eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛 = ((#‘𝑌) − 𝐾) → (𝑌 = (𝑋 cyclShift 𝑛) ↔ 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾))))
109108rspcev 3282 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((#‘𝑌) − 𝐾) ∈ (0...𝑁) ∧ 𝑌 = (𝑋 cyclShift ((#‘𝑌) − 𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
110100, 106, 109syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
111110adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))
112 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑍 = 𝑌 → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑌 = (𝑋 cyclShift 𝑛)))
113112rexbidv 3034 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑍 = 𝑌 → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
114113adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → (∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))
115111, 114mpbird 246 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) ∧ 𝐾 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑍 = 𝑌) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
116115exp41 636 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = 𝑌 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
117116com24 93 . . . . . . . . . . . . . . . . . . . 20 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = 𝑌 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
11893, 117sylbid 229 . . . . . . . . . . . . . . . . . . 19 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝐾 ∈ (0...𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
119118com24 93 . . . . . . . . . . . . . . . . . 18 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
120119impcom 445 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 0) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
121120com13 86 . . . . . . . . . . . . . . . 16 (𝑍 = (𝑌 cyclShift 0) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
122121a1d 25 . . . . . . . . . . . . . . 15 (𝑍 = (𝑌 cyclShift 0) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
12390, 122syl6bi 242 . . . . . . . . . . . . . 14 (𝑚 = 0 → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
124123com24 93 . . . . . . . . . . . . 13 (𝑚 = 0 → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
125124com15 99 . . . . . . . . . . . 12 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))))
126125imp41 617 . . . . . . . . . . 11 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝑚 = 0 → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
127126com12 32 . . . . . . . . . 10 (𝑚 = 0 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
128 difelfzle 12321 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ 𝑚 ∈ (0...𝑁) ∧ 𝐾𝑚) → (𝑚𝐾) ∈ (0...𝑁))
1291283exp 1256 . . . . . . . . . . . . . . . 16 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁))))
130129ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑚 ∈ (0...𝑁) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁))))
131130imp 444 . . . . . . . . . . . . . 14 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁)))
132131adantr 480 . . . . . . . . . . . . 13 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾𝑚 → (𝑚𝐾) ∈ (0...𝑁)))
133132impcom 445 . . . . . . . . . . . 12 ((𝐾𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → (𝑚𝐾) ∈ (0...𝑁))
1349ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝑌 ∈ Word 𝑉)
13512ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → 𝐾 ∈ ℤ)
136 zsubcl 11296 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚𝐾) ∈ ℤ)
137136ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ ℤ → (𝐾 ∈ ℤ → (𝑚𝐾) ∈ ℤ))
13815, 11, 137syl2imc 40 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝑚𝐾) ∈ ℤ))
139138ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) → (𝑚 ∈ (0...𝑁) → (𝑚𝐾) ∈ ℤ))
140139imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑚𝐾) ∈ ℤ)
141 2cshw 13410 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑌 ∈ Word 𝑉𝐾 ∈ ℤ ∧ (𝑚𝐾) ∈ ℤ) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚𝐾))))
142134, 135, 140, 141syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)) = (𝑌 cyclShift (𝐾 + (𝑚𝐾))))
143 zcn 11259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
14415zcnd 11359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑚 ∈ (0...𝑁) → 𝑚 ∈ ℂ)
145 pncan3 10168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐾 ∈ ℂ ∧ 𝑚 ∈ ℂ) → (𝐾 + (𝑚𝐾)) = 𝑚)
146143, 144, 145syl2anr 494 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑚 ∈ (0...𝑁) ∧ 𝐾 ∈ ℤ) → (𝐾 + (𝑚𝐾)) = 𝑚)
147146ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑚 ∈ (0...𝑁) → (𝐾 ∈ ℤ → (𝐾 + (𝑚𝐾)) = 𝑚))
14811, 147syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐾 ∈ (0...𝑁) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚𝐾)) = 𝑚))
149148ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) → (𝑚 ∈ (0...𝑁) → (𝐾 + (𝑚𝐾)) = 𝑚))
150149imp 444 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾 + (𝑚𝐾)) = 𝑚)
151150oveq2d 6565 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift (𝐾 + (𝑚𝐾))) = (𝑌 cyclShift 𝑚))
152142, 151eqtr2d 2645 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)))
153152adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)))
154 oveq1 6556 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 = (𝑌 cyclShift 𝐾) → (𝑋 cyclShift (𝑚𝐾)) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾)))
155154eqeq2d 2620 . . . . . . . . . . . . . . . . . . . . . 22 (𝑋 = (𝑌 cyclShift 𝐾) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾))))
156155adantl 481 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → ((𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚𝐾)) ↔ (𝑌 cyclShift 𝑚) = ((𝑌 cyclShift 𝐾) cyclShift (𝑚𝐾))))
157153, 156mpbird 246 . . . . . . . . . . . . . . . . . . . 20 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑌 cyclShift 𝑚) = (𝑋 cyclShift (𝑚𝐾)))
158157eqeq2d 2620 . . . . . . . . . . . . . . . . . . 19 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) ↔ 𝑍 = (𝑋 cyclShift (𝑚𝐾))))
159158biimpd 218 . . . . . . . . . . . . . . . . . 18 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝐾𝑚) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾))))
160159exp41 636 . . . . . . . . . . . . . . . . 17 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝐾𝑚 → (𝑚 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))))))
161160com24 93 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (𝑚 ∈ (0...𝑁) → (𝐾𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))))))
162161imp31 447 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝐾𝑚 → (𝑍 = (𝑌 cyclShift 𝑚) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))))
163162com23 84 . . . . . . . . . . . . . 14 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑍 = (𝑌 cyclShift 𝑚) → (𝐾𝑚𝑍 = (𝑋 cyclShift (𝑚𝐾)))))
164163imp 444 . . . . . . . . . . . . 13 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → (𝐾𝑚𝑍 = (𝑋 cyclShift (𝑚𝐾))))
165164impcom 445 . . . . . . . . . . . 12 ((𝐾𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → 𝑍 = (𝑋 cyclShift (𝑚𝐾)))
166 oveq2 6557 . . . . . . . . . . . . . 14 (𝑛 = (𝑚𝐾) → (𝑋 cyclShift 𝑛) = (𝑋 cyclShift (𝑚𝐾)))
167166eqeq2d 2620 . . . . . . . . . . . . 13 (𝑛 = (𝑚𝐾) → (𝑍 = (𝑋 cyclShift 𝑛) ↔ 𝑍 = (𝑋 cyclShift (𝑚𝐾))))
168167rspcev 3282 . . . . . . . . . . . 12 (((𝑚𝐾) ∈ (0...𝑁) ∧ 𝑍 = (𝑋 cyclShift (𝑚𝐾))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
169133, 165, 168syl2anc 691 . . . . . . . . . . 11 ((𝐾𝑚 ∧ ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚))) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
170169ex 449 . . . . . . . . . 10 (𝐾𝑚 → (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
17188, 127, 170pm2.61ii 176 . . . . . . . . 9 (((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) ∧ 𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))
172171ex 449 . . . . . . . 8 ((((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) ∧ 𝑚 ∈ (0...𝑁)) → (𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
173172rexlimdva 3013 . . . . . . 7 (((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) ∧ 𝑋 = (𝑌 cyclShift 𝐾)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
174173ex 449 . . . . . 6 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
175174com23 84 . . . . 5 ((𝐾 ∈ (0...𝑁) ∧ (𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁)) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))))
176175ex 449 . . . 4 (𝐾 ∈ (0...𝑁) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → (𝑋 = (𝑌 cyclShift 𝐾) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
177176com24 93 . . 3 (𝐾 ∈ (0...𝑁) → (𝑋 = (𝑌 cyclShift 𝐾) → (∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))))
1781773imp 1249 . 2 ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
179178com12 32 1 ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∃wrex 2897   class class class wbr 4583  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  0cc0 9815   + caddc 9818   ≤ cle 9954   − cmin 10145  ℕ0cn0 11169  ℤcz 11254  ...cfz 12197  #chash 12979  Word cword 13146   cyclShift ccsh 13385 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-inf 8232  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fz 12198  df-fzo 12335  df-fl 12455  df-mod 12531  df-hash 12980  df-word 13154  df-concat 13156  df-substr 13158  df-csh 13386 This theorem is referenced by:  eleclclwwlknlem1  26345  eleclclwwlksnlem1  41245
 Copyright terms: Public domain W3C validator