Metamath Proof Explorer

Theorem 1cshid

Description: Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023)

Ref Expression
Assertion 1cshid ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → W cyclShift N = W

Proof

Step Hyp Ref Expression
1 cshwmodn ⊢ W ∈ Word V ∧ N ∈ ℤ → W cyclShift N = W cyclShift N mod W
2 1 3adant3 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → W cyclShift N = W cyclShift N mod W
3 simp3 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → W = 1
4 3 oveq2d ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → N mod W = N mod 1
5 zmod10 ⊢ N ∈ ℤ → N mod 1 = 0
6 5 3ad2ant2 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → N mod 1 = 0
7 4 6 eqtrd ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → N mod W = 0
8 7 oveq2d ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → W cyclShift N mod W = W cyclShift 0
9 cshw0 ⊢ W ∈ Word V → W cyclShift 0 = W
10 9 3ad2ant1 ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → W cyclShift 0 = W
11 2 8 10 3eqtrd ⊢ W ∈ Word V ∧ N ∈ ℤ ∧ W = 1 → W cyclShift N = W