cshwshashlem1 - Metamath Proof Explorer

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

Theorem cshwshashlem1 17161

Description: If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by AV, 19-May-2018.) (Revised by AV, 8-Jun-2018.) (Revised by AV, 10-Nov-2018.)

**Hypothesis**
Ref	Expression
cshwshash.0	⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))

**Assertion**
Ref	Expression
cshwshashlem1	⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊)

Distinct variable groups: 𝑖,𝐿 𝑖,𝑉 𝑖,𝑊 𝜑,𝑖

**Proof of Theorem cshwshashlem1**
Step	Hyp	Ref	Expression
1		df-ne 2958	. . . . . . 7 ⊢ ((𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ (𝑊‘𝑖) = (𝑊‘0))
2	1	rexbii 3111	. . . . . 6 ⊢ (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ∃𝑖 ∈ (0..^(♯‘𝑊)) ¬ (𝑊‘𝑖) = (𝑊‘0))
3		rexnal 3116	. . . . . 6 ⊢ (∃𝑖 ∈ (0..^(♯‘𝑊)) ¬ (𝑊‘𝑖) = (𝑊‘0) ↔ ¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
4	2, 3	bitri 278	. . . . 5 ⊢ (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
5		simpll 778	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝜑)
6		fzo0ss1 13725	. . . . . . . . . . . . . 14 ⊢ (1..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))
7		fzossfz 13714	. . . . . . . . . . . . . 14 ⊢ (0..^(♯‘𝑊)) ⊆ (0...(♯‘𝑊))
8	6, 7	sstri 3945	. . . . . . . . . . . . 13 ⊢ (1..^(♯‘𝑊)) ⊆ (0...(♯‘𝑊))
9	8	sseli 3932	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) → 𝐿 ∈ (0...(♯‘𝑊)))
10	9	ad2antlr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝐿 ∈ (0...(♯‘𝑊)))
11		simpr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 cyclShift 𝐿) = 𝑊)
12		cshwshash.0	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))
13		simpll 778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝑊 ∈ Word 𝑉)
14		simpr 489	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (♯‘𝑊) ∈ ℙ)
15	14	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈ ℙ)
16		elfzelz 13558	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 ∈ ℤ)
17	16	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ ℤ)
18		cshwsidrepswmod0 17160	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
19	13, 15, 17, 18	syl3anc 1397	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
20	19	ex 417	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (𝐿 ∈ (0...(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))))
21	20	3imp 1127	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
22		olc 881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐿 = (♯‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))
23	22	a1d 26	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 = (♯‘𝑊) → (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊))))
24		fzofzim 13745	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ (0..^(♯‘𝑊)))
25		zmodidfzoimp 13941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐿 ∈ (0..^(♯‘𝑊)) → (𝐿 mod (♯‘𝑊)) = 𝐿)
26		eqtr2 2783	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 mod (♯‘𝑊)) = 𝐿 ∧ (𝐿 mod (♯‘𝑊)) = 0) → 𝐿 = 0)
27	26	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐿 mod (♯‘𝑊)) = 𝐿 ∧ (𝐿 mod (♯‘𝑊)) = 0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0))
28	27	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐿 mod (♯‘𝑊)) = 𝐿 → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0)))
29	25, 28	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐿 ∈ (0..^(♯‘𝑊)) → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0)))
30	24, 29	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0)))
31	30	expcom 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → (𝐿 ≠ (♯‘𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0))))
32	31	com24 96	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0))))
33	32	impcom 412	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0)))
34	33	3adant3 1149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0)))
35	34	impcom 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0))
36	35	impcom 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ ((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → 𝐿 = 0)
37	36	orcd 886	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ ((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))
38	37	ex 417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ≠ (♯‘𝑊) → (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊))))
39	23, 38	pm2.61ine 3040	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))
40	39	orcd 886	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
41		df-3or 1103	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) ↔ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
42	40, 41	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
43	42	ex 417	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 mod (♯‘𝑊)) = 0 → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
44		3mix3 1350	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
45	44	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
46	43, 45	jaoi 870	. . . . . . . . . . . . . 14 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
47	21, 46	mpcom 39	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
48	12, 47	syl3an1 1180	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
49		3mix1 1348	. . . . . . . . . . . . . 14 ⊢ (𝐿 = 0 → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
50	49	a1d 26	. . . . . . . . . . . . 13 ⊢ (𝐿 = 0 → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
51		3mix2 1349	. . . . . . . . . . . . . 14 ⊢ (𝐿 = (♯‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
52	51	a1d 26	. . . . . . . . . . . . 13 ⊢ (𝐿 = (♯‘𝑊) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
53		repswsymballbi 14824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
54	53	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
55	12, 54	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
56	55	3ad2ant1 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
57	56	biimpa 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
58	57	3mix3d 1356	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
59	58	expcom 418	. . . . . . . . . . . . 13 ⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
60	50, 52, 59	3jaoi 1453	. . . . . . . . . . . 12 ⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
61	48, 60	mpcom 39	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
62	5, 10, 11, 61	syl3anc 1397	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
63		elfzo1 13748	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) ↔ (𝐿 ∈ ℕ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)))
64		nnne0 12276	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ → 𝐿 ≠ 0)
65		df-ne 2958	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ≠ 0 ↔ ¬ 𝐿 = 0)
66		pm2.21 124	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝐿 = 0 → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
67	65, 66	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ≠ 0 → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
68	64, 67	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ ℕ → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
69	68	3ad2ant1 1150	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ ℕ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
70	63, 69	sylbi 220	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
71	70	ad2antlr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
72	71	com12 33	. . . . . . . . . . 11 ⊢ (𝐿 = 0 → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
73		nnre 12246	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ ℕ → 𝐿 ∈ ℝ)
74		ltne 11313	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℝ ∧ 𝐿 < (♯‘𝑊)) → (♯‘𝑊) ≠ 𝐿)
75	73, 74	sylan 591	. . . . . . . . . . . . . . . 16 ⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (♯‘𝑊) ≠ 𝐿)
76		df-ne 2958	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑊) ≠ 𝐿 ↔ ¬ (♯‘𝑊) = 𝐿)
77		eqcom 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 = (♯‘𝑊) ↔ (♯‘𝑊) = 𝐿)
78		pm2.21 124	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (♯‘𝑊) = 𝐿 → ((♯‘𝑊) = 𝐿 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
79	77, 78	biimtrid 245	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (♯‘𝑊) = 𝐿 → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
80	76, 79	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑊) ≠ 𝐿 → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
81	75, 80	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
82	81	3adant2 1148	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ ℕ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
83	63, 82	sylbi 220	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
84	83	ad2antlr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
85	84	com12 33	. . . . . . . . . . 11 ⊢ (𝐿 = (♯‘𝑊) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
86		ax-1 6	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
87	72, 85, 86	3jaoi 1453	. . . . . . . . . 10 ⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
88	62, 87	mpcom 39	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
89	88	pm2.24d 152	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊))
90	89	exp31 424	. . . . . . 7 ⊢ (𝜑 → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
91	90	com34 92	. . . . . 6 ⊢ (𝜑 → (𝐿 ∈ (1..^(♯‘𝑊)) → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
92	91	com23 87	. . . . 5 ⊢ (𝜑 → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
93	4, 92	biimtrid 245	. . . 4 ⊢ (𝜑 → (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
94	93	3imp 1127	. . 3 ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))
95	94	com12 33	. 2 ⊢ ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊))
96		ax-1 6	. 2 ⊢ ((𝑊 cyclShift 𝐿) ≠ 𝑊 → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊))
97	95, 96	pm2.61ine 3040	1 ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∨ w3o 1101 ∧ w3a 1102 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 class class class wbr 5108 ‘cfv 6536 (class class class)co 7412 ℝcr 11105 0cc0 11106 1c1 11107 < clt 11249 ℕcn 12239 ℤcz 12597 ...cfz 13541 ..^cfzo 13689 mod cmo 13909 ♯chash 14373 Word cword 14557 repeatS creps 14812 cyclShift ccsh 14832 ℙcprime 16735

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-oadd 8455 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9400 df-inf 9401 df-dju 9894 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-n0 12511 df-xnn0 12584 df-z 12598 df-uz 12869 df-rp 13023 df-fz 13542 df-fzo 13690 df-fl 13832 df-mod 13910 df-seq 14045 df-exp 14105 df-hash 14374 df-word 14558 df-concat 14615 df-substr 14686 df-pfx 14716 df-reps 14813 df-csh 14833 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-dvds 16317 df-gcd 16559 df-prm 16736 df-phi 16831

This theorem is used by: cshwshashlem2 17162

W3C validator