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

Theorem cshweqrep 13613
 Description: If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.)
Assertion
Ref Expression
cshweqrep ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → ∀𝑗 ∈ ℕ0 (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
Distinct variable groups:   𝑗,𝐼   𝑗,𝐿   𝑗,𝑉   𝑗,𝑊

Proof of Theorem cshweqrep
Dummy variables 𝑦 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6697 . . . . . . . . . 10 (𝑥 = 0 → (𝑥 · 𝐿) = (0 · 𝐿))
21oveq2d 6706 . . . . . . . . 9 (𝑥 = 0 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (0 · 𝐿)))
32oveq1d 6705 . . . . . . . 8 (𝑥 = 0 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
43fveq2d 6233 . . . . . . 7 (𝑥 = 0 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
54eqeq2d 2661 . . . . . 6 (𝑥 = 0 → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))))
65imbi2d 329 . . . . 5 (𝑥 = 0 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))))
7 oveq1 6697 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 · 𝐿) = (𝑦 · 𝐿))
87oveq2d 6706 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑦 · 𝐿)))
98oveq1d 6705 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))
109fveq2d 6233 . . . . . . 7 (𝑥 = 𝑦 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
1110eqeq2d 2661 . . . . . 6 (𝑥 = 𝑦 → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))))
1211imbi2d 329 . . . . 5 (𝑥 = 𝑦 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))))
13 oveq1 6697 . . . . . . . . . 10 (𝑥 = (𝑦 + 1) → (𝑥 · 𝐿) = ((𝑦 + 1) · 𝐿))
1413oveq2d 6706 . . . . . . . . 9 (𝑥 = (𝑦 + 1) → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
1514oveq1d 6705 . . . . . . . 8 (𝑥 = (𝑦 + 1) → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
1615fveq2d 6233 . . . . . . 7 (𝑥 = (𝑦 + 1) → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
1716eqeq2d 2661 . . . . . 6 (𝑥 = (𝑦 + 1) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
1817imbi2d 329 . . . . 5 (𝑥 = (𝑦 + 1) → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
19 oveq1 6697 . . . . . . . . . 10 (𝑥 = 𝑗 → (𝑥 · 𝐿) = (𝑗 · 𝐿))
2019oveq2d 6706 . . . . . . . . 9 (𝑥 = 𝑗 → (𝐼 + (𝑥 · 𝐿)) = (𝐼 + (𝑗 · 𝐿)))
2120oveq1d 6705 . . . . . . . 8 (𝑥 = 𝑗 → ((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)) = ((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))
2221fveq2d 6233 . . . . . . 7 (𝑥 = 𝑗 → (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
2322eqeq2d 2661 . . . . . 6 (𝑥 = 𝑗 → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
2423imbi2d 329 . . . . 5 (𝑥 = 𝑗 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑥 · 𝐿)) mod (#‘𝑊)))) ↔ (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))))
25 zcn 11420 . . . . . . . . . . . . 13 (𝐿 ∈ ℤ → 𝐿 ∈ ℂ)
2625mul02d 10272 . . . . . . . . . . . 12 (𝐿 ∈ ℤ → (0 · 𝐿) = 0)
2726adantl 481 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (0 · 𝐿) = 0)
2827adantr 480 . . . . . . . . . 10 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (0 · 𝐿) = 0)
2928oveq2d 6706 . . . . . . . . 9 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = (𝐼 + 0))
30 elfzoelz 12509 . . . . . . . . . . . 12 (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℤ)
3130zcnd 11521 . . . . . . . . . . 11 (𝐼 ∈ (0..^(#‘𝑊)) → 𝐼 ∈ ℂ)
3231addid1d 10274 . . . . . . . . . 10 (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 + 0) = 𝐼)
3332ad2antll 765 . . . . . . . . 9 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + 0) = 𝐼)
3429, 33eqtrd 2685 . . . . . . . 8 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 + (0 · 𝐿)) = 𝐼)
3534oveq1d 6705 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)) = (𝐼 mod (#‘𝑊)))
36 zmodidfzoimp 12740 . . . . . . . 8 (𝐼 ∈ (0..^(#‘𝑊)) → (𝐼 mod (#‘𝑊)) = 𝐼)
3736ad2antll 765 . . . . . . 7 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝐼 mod (#‘𝑊)) = 𝐼)
3835, 37eqtr2d 2686 . . . . . 6 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → 𝐼 = ((𝐼 + (0 · 𝐿)) mod (#‘𝑊)))
3938fveq2d 6233 . . . . 5 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (0 · 𝐿)) mod (#‘𝑊))))
40 fveq1 6228 . . . . . . . . . . . . 13 (𝑊 = (𝑊 cyclShift 𝐿) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
4140eqcoms 2659 . . . . . . . . . . . 12 ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
4241ad2antrl 764 . . . . . . . . . . 11 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
4342adantl 481 . . . . . . . . . 10 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))))
44 simprll 819 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → 𝑊 ∈ Word 𝑉)
45 simprlr 820 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → 𝐿 ∈ ℤ)
46 elfzo0 12548 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ (0..^(#‘𝑊)) ↔ (𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)))
47 nn0z 11438 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐼 ∈ ℕ0𝐼 ∈ ℤ)
4847adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) → 𝐼 ∈ ℤ)
49 nn0z 11438 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℕ0𝑦 ∈ ℤ)
50 zmulcl 11464 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
5149, 50sylan 487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℕ0𝐿 ∈ ℤ) → (𝑦 · 𝐿) ∈ ℤ)
5251ancoms 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → (𝑦 · 𝐿) ∈ ℤ)
53 zaddcl 11455 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐼 ∈ ℤ ∧ (𝑦 · 𝐿) ∈ ℤ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
5448, 52, 53syl2an 493 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℤ)
55 simplr 807 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)) → (#‘𝑊) ∈ ℕ)
5654, 55jca 553 . . . . . . . . . . . . . . . . . . . . 21 (((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) ∧ (𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0)) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
5756ex 449 . . . . . . . . . . . . . . . . . . . 20 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
58573adant3 1101 . . . . . . . . . . . . . . . . . . 19 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
5946, 58sylbi 207 . . . . . . . . . . . . . . . . . 18 (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
6059adantl 481 . . . . . . . . . . . . . . . . 17 (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
6160expd 451 . . . . . . . . . . . . . . . 16 (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
6261com12 32 . . . . . . . . . . . . . . 15 (𝐿 ∈ ℤ → (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
6362adantl 481 . . . . . . . . . . . . . 14 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))))
6463imp 444 . . . . . . . . . . . . 13 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ0 → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ)))
6564impcom 445 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ))
66 zmodfzo 12733 . . . . . . . . . . . 12 (((𝐼 + (𝑦 · 𝐿)) ∈ ℤ ∧ (#‘𝑊) ∈ ℕ) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
6765, 66syl 17 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊)))
68 cshwidxmod 13595 . . . . . . . . . . 11 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ ∧ ((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
6944, 45, 67, 68syl3anc 1366 . . . . . . . . . 10 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊 cyclShift 𝐿)‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))))
70 nn0re 11339 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ ℕ0𝐼 ∈ ℝ)
71 zre 11419 . . . . . . . . . . . . . . . . . . . . . 22 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
72 nn0re 11339 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
73 nnrp 11880 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑊) ∈ ℕ → (#‘𝑊) ∈ ℝ+)
74 remulcl 10059 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
7574ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℝ)
76 readdcl 10057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐼 ∈ ℝ ∧ (𝑦 · 𝐿) ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
7775, 76sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐼 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
7877ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
7978adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (𝐼 + (𝑦 · 𝐿)) ∈ ℝ)
80 simprll 819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → 𝐿 ∈ ℝ)
81 simpl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (#‘𝑊) ∈ ℝ+)
82 modaddmod 12749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐼 + (𝑦 · 𝐿)) ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ+) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
8379, 80, 81, 82syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)))
84 recn 10064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐼 ∈ ℝ → 𝐼 ∈ ℂ)
8584adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐼 ∈ ℂ)
8674recnd 10106 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
8786ancoms 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
8887adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝑦 · 𝐿) ∈ ℂ)
89 recn 10064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝐿 ∈ ℝ → 𝐿 ∈ ℂ)
9089adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝐿 ∈ ℂ)
9190adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → 𝐿 ∈ ℂ)
9285, 88, 91addassd 10100 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 · 𝐿) + 𝐿)))
93 recn 10064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑦 ∈ ℝ → 𝑦 ∈ ℂ)
9493adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
95 1cnd 10094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 1 ∈ ℂ)
9694, 95, 90adddird 10103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 + 1) · 𝐿) = ((𝑦 · 𝐿) + (1 · 𝐿)))
9789mulid2d 10096 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝐿 ∈ ℝ → (1 · 𝐿) = 𝐿)
9897adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (1 · 𝐿) = 𝐿)
9998oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + (1 · 𝐿)) = ((𝑦 · 𝐿) + 𝐿))
10096, 99eqtr2d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
101100adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝑦 · 𝐿) + 𝐿) = ((𝑦 + 1) · 𝐿))
102101oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → (𝐼 + ((𝑦 · 𝐿) + 𝐿)) = (𝐼 + ((𝑦 + 1) · 𝐿)))
10392, 102eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
104103adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((𝐼 + (𝑦 · 𝐿)) + 𝐿) = (𝐼 + ((𝑦 + 1) · 𝐿)))
105104oveq1d 6705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → (((𝐼 + (𝑦 · 𝐿)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
10683, 105eqtrd 2685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((#‘𝑊) ∈ ℝ+ ∧ ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ)) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
107106ex 449 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝑊) ∈ ℝ+ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
10873, 107syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝑊) ∈ ℕ → (((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ 𝐼 ∈ ℝ) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
109108expd 451 . . . . . . . . . . . . . . . . . . . . . . 23 ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
110109com12 32 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
11171, 72, 110syl2an 493 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((#‘𝑊) ∈ ℕ → (𝐼 ∈ ℝ → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
112111com13 88 . . . . . . . . . . . . . . . . . . . 20 (𝐼 ∈ ℝ → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
11370, 112syl 17 . . . . . . . . . . . . . . . . . . 19 (𝐼 ∈ ℕ0 → ((#‘𝑊) ∈ ℕ → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
114113imp 444 . . . . . . . . . . . . . . . . . 18 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
1151143adant3 1101 . . . . . . . . . . . . . . . . 17 ((𝐼 ∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ ∧ 𝐼 < (#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
11646, 115sylbi 207 . . . . . . . . . . . . . . . 16 (𝐼 ∈ (0..^(#‘𝑊)) → ((𝐿 ∈ ℤ ∧ 𝑦 ∈ ℕ0) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
117116expd 451 . . . . . . . . . . . . . . 15 (𝐼 ∈ (0..^(#‘𝑊)) → (𝐿 ∈ ℤ → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
118117adantld 482 . . . . . . . . . . . . . 14 (𝐼 ∈ (0..^(#‘𝑊)) → ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
119118adantl 481 . . . . . . . . . . . . 13 (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
120119impcom 445 . . . . . . . . . . . 12 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑦 ∈ ℕ0 → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
121120impcom 445 . . . . . . . . . . 11 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊)) = ((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))
122121fveq2d 6233 . . . . . . . . . 10 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)) + 𝐿) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
12343, 69, 1223eqtrd 2689 . . . . . . . . 9 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))
124123eqeq2d 2661 . . . . . . . 8 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) ↔ (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
125124biimpd 219 . . . . . . 7 ((𝑦 ∈ ℕ0 ∧ ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))))) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊)))))
126125ex 449 . . . . . 6 (𝑦 ∈ ℕ0 → (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → ((𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
127126a2d 29 . . . . 5 (𝑦 ∈ ℕ0 → ((((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑦 · 𝐿)) mod (#‘𝑊)))) → (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + ((𝑦 + 1) · 𝐿)) mod (#‘𝑊))))))
1286, 12, 18, 24, 39, 127nn0ind 11510 . . . 4 (𝑗 ∈ ℕ0 → (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
129128com12 32 . . 3 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → (𝑗 ∈ ℕ0 → (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
130129ralrimiv 2994 . 2 (((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) ∧ ((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊)))) → ∀𝑗 ∈ ℕ0 (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))
131130ex 449 1 ((𝑊 ∈ Word 𝑉𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊𝐼 ∈ (0..^(#‘𝑊))) → ∀𝑗 ∈ ℕ0 (𝑊𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941   class class class wbr 4685  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℝ+crp 11870  ..^cfzo 12504   mod cmo 12708  #chash 13157  Word cword 13323   cyclShift ccsh 13580 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-hash 13158  df-word 13331  df-concat 13333  df-substr 13335  df-csh 13581 This theorem is referenced by:  cshw1  13614  cshwsidrepsw  15847
 Copyright terms: Public domain W3C validator