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 17121

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 2957	. . . . . . 7 ⊢ ((𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ (𝑊‘𝑖) = (𝑊‘0))
2	1	rexbii 3108	. . . . . 6 ⊢ (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ∃𝑖 ∈ (0..^(♯‘𝑊)) ¬ (𝑊‘𝑖) = (𝑊‘0))
3		rexnal 3113	. . . . . 6 ⊢ (∃𝑖 ∈ (0..^(♯‘𝑊)) ¬ (𝑊‘𝑖) = (𝑊‘0) ↔ ¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
4	2, 3	bitri 277	. . . . 5 ⊢ (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ↔ ¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
5		simpll 776	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝜑)
6		fzo0ss1 13688	. . . . . . . . . . . . . 14 ⊢ (1..^(♯‘𝑊)) ⊆ (0..^(♯‘𝑊))
7		fzossfz 13677	. . . . . . . . . . . . . 14 ⊢ (0..^(♯‘𝑊)) ⊆ (0...(♯‘𝑊))
8	6, 7	sstri 3943	. . . . . . . . . . . . 13 ⊢ (1..^(♯‘𝑊)) ⊆ (0...(♯‘𝑊))
9	8	sseli 3930	. . . . . . . . . . . 12 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) → 𝐿 ∈ (0...(♯‘𝑊)))
10	9	ad2antlr 737	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → 𝐿 ∈ (0...(♯‘𝑊)))
11		simpr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 cyclShift 𝐿) = 𝑊)
12		cshwshash.0	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ))
13		simpll 776	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝑊 ∈ Word 𝑉)
14		simpr 488	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (♯‘𝑊) ∈ ℙ)
15	14	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘𝑊) ∈ ℙ)
16		elfzelz 13522	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → 𝐿 ∈ ℤ)
17	16	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ ℤ)
18		cshwsidrepswmod0 17120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ ∧ 𝐿 ∈ ℤ) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
19	13, 15, 17, 18	syl3anc 1389	. . . . . . . . . . . . . . . 16 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
20	19	ex 416	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (𝐿 ∈ (0...(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))))
21	20	3imp 1122	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
22		olc 879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐿 = (♯‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))
23	22	a1d 25	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 = (♯‘𝑊) → (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊))))
24		fzofzim 13708	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → 𝐿 ∈ (0..^(♯‘𝑊)))
25		zmodidfzoimp 13904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐿 ∈ (0..^(♯‘𝑊)) → (𝐿 mod (♯‘𝑊)) = 𝐿)
26		eqtr2 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐿 mod (♯‘𝑊)) = 𝐿 ∧ (𝐿 mod (♯‘𝑊)) = 0) → 𝐿 = 0)
27	26	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐿 mod (♯‘𝑊)) = 𝐿 ∧ (𝐿 mod (♯‘𝑊)) = 0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0))
28	27	ex 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐿 mod (♯‘𝑊)) = 𝐿 → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0)))
29	25, 28	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐿 ∈ (0..^(♯‘𝑊)) → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0)))
30	24, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0)))
31	30	expcom 417	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → (𝐿 ≠ (♯‘𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → 𝐿 = 0))))
32	31	com24 95	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐿 ∈ (0...(♯‘𝑊)) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0))))
33	32	impcom 411	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0)))
34	33	3adant3 1144	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ((𝐿 mod (♯‘𝑊)) = 0 → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0)))
35	34	impcom 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 ≠ (♯‘𝑊) → 𝐿 = 0))
36	35	impcom 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ ((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → 𝐿 = 0)
37	36	orcd 884	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐿 ≠ (♯‘𝑊) ∧ ((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊))) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))
38	37	ex 416	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐿 ≠ (♯‘𝑊) → (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊))))
39	23, 38	pm2.61ine 3039	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)))
40	39	orcd 884	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
41		df-3or 1098	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) ↔ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊)) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
42	40, 41	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∧ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
43	42	ex 416	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 mod (♯‘𝑊)) = 0 → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
44		3mix3 1345	. . . . . . . . . . . . . . . 16 ⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
45	44	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
46	43, 45	jaoi 868	. . . . . . . . . . . . . 14 ⊢ (((𝐿 mod (♯‘𝑊)) = 0 ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))))
47	21, 46	mpcom 38	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
48	12, 47	syl3an1 1175	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))))
49		3mix1 1343	. . . . . . . . . . . . . 14 ⊢ (𝐿 = 0 → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
50	49	a1d 25	. . . . . . . . . . . . 13 ⊢ (𝐿 = 0 → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
51		3mix2 1344	. . . . . . . . . . . . . 14 ⊢ (𝐿 = (♯‘𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
52	51	a1d 25	. . . . . . . . . . . . 13 ⊢ (𝐿 = (♯‘𝑊) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
53		repswsymballbi 14786	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
54	53	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) ∈ ℙ) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
55	12, 54	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
56	55	3ad2ant1 1145	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
57	56	biimpa 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
58	57	3mix3d 1351	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) ∧ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
59	58	expcom 417	. . . . . . . . . . . . 13 ⊢ (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
60	50, 52, 59	3jaoi 1446	. . . . . . . . . . . 12 ⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊))) → ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))))
61	48, 60	mpcom 38	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
62	5, 10, 11, 61	syl3anc 1389	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
63		elfzo1 13711	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) ↔ (𝐿 ∈ ℕ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)))
64		nnne0 12240	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ℕ → 𝐿 ≠ 0)
65		df-ne 2957	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ≠ 0 ↔ ¬ 𝐿 = 0)
66		pm2.21 123	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝐿 = 0 → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
67	65, 66	sylbi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ≠ 0 → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
68	64, 67	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝐿 ∈ ℕ → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
69	68	3ad2ant1 1145	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ ℕ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
70	63, 69	sylbi 219	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
71	70	ad2antlr 737	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = 0 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
72	71	com12 32	. . . . . . . . . . 11 ⊢ (𝐿 = 0 → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
73		nnre 12210	. . . . . . . . . . . . . . . . 17 ⊢ (𝐿 ∈ ℕ → 𝐿 ∈ ℝ)
74		ltne 11273	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐿 ∈ ℝ ∧ 𝐿 < (♯‘𝑊)) → (♯‘𝑊) ≠ 𝐿)
75	73, 74	sylan 589	. . . . . . . . . . . . . . . 16 ⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (♯‘𝑊) ≠ 𝐿)
76		df-ne 2957	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘𝑊) ≠ 𝐿 ↔ ¬ (♯‘𝑊) = 𝐿)
77		eqcom 2768	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐿 = (♯‘𝑊) ↔ (♯‘𝑊) = 𝐿)
78		pm2.21 123	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (♯‘𝑊) = 𝐿 → ((♯‘𝑊) = 𝐿 → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
79	77, 78	biimtrid 244	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (♯‘𝑊) = 𝐿 → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
80	76, 79	sylbi 219	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘𝑊) ≠ 𝐿 → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
81	75, 80	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
82	81	3adant2 1143	. . . . . . . . . . . . . 14 ⊢ ((𝐿 ∈ ℕ ∧ (♯‘𝑊) ∈ ℕ ∧ 𝐿 < (♯‘𝑊)) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
83	63, 82	sylbi 219	. . . . . . . . . . . . 13 ⊢ (𝐿 ∈ (1..^(♯‘𝑊)) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
84	83	ad2antlr 737	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (𝐿 = (♯‘𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
85	84	com12 32	. . . . . . . . . . 11 ⊢ (𝐿 = (♯‘𝑊) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
86		ax-1 6	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
87	72, 85, 86	3jaoi 1446	. . . . . . . . . 10 ⊢ ((𝐿 = 0 ∨ 𝐿 = (♯‘𝑊) ∨ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) → (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
88	62, 87	mpcom 38	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
89	88	pm2.24d 151	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐿 ∈ (1..^(♯‘𝑊))) ∧ (𝑊 cyclShift 𝐿) = 𝑊) → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊))
90	89	exp31 423	. . . . . . 7 ⊢ (𝜑 → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
91	90	com34 91	. . . . . 6 ⊢ (𝜑 → (𝐿 ∈ (1..^(♯‘𝑊)) → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
92	91	com23 86	. . . . 5 ⊢ (𝜑 → (¬ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0) → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
93	4, 92	biimtrid 244	. . . 4 ⊢ (𝜑 → (∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) → (𝐿 ∈ (1..^(♯‘𝑊)) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))))
94	93	3imp 1122	. . 3 ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → ((𝑊 cyclShift 𝐿) = 𝑊 → (𝑊 cyclShift 𝐿) ≠ 𝑊))
95	94	com12 32	. 2 ⊢ ((𝑊 cyclShift 𝐿) = 𝑊 → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊))
96		ax-1 6	. 2 ⊢ ((𝑊 cyclShift 𝐿) ≠ 𝑊 → ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊))
97	95, 96	pm2.61ine 3039	1 ⊢ ((𝜑 ∧ ∃𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ≠ (𝑊‘0) ∧ 𝐿 ∈ (1..^(♯‘𝑊))) → (𝑊 cyclShift 𝐿) ≠ 𝑊)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∨ w3o 1096 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 ∃wrex 3085 class class class wbr 5097 ‘cfv 6515 (class class class)co 7390 ℝcr 11065 0cc0 11066 1c1 11067 < clt 11209 ℕcn 12203 ℤcz 12561 ...cfz 13505 ..^cfzo 13652 mod cmo 13872 ♯chash 14336 Word cword 14519 repeatS creps 14774 cyclShift ccsh 14794 ℙcprime 16695

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143 ax-pre-sup 11144

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-1o 8430 df-2o 8431 df-oadd 8434 df-er 8671 df-en 8921 df-dom 8922 df-sdom 8923 df-fin 8924 df-sup 9381 df-inf 9382 df-dju 9852 df-card 9890 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-div 11838 df-nn 12204 df-2 12273 df-3 12274 df-n0 12475 df-xnn0 12548 df-z 12562 df-uz 12833 df-rp 12987 df-fz 13506 df-fzo 13653 df-fl 13795 df-mod 13873 df-seq 14008 df-exp 14068 df-hash 14337 df-word 14520 df-concat 14577 df-substr 14648 df-pfx 14678 df-reps 14775 df-csh 14795 df-cj 15116 df-re 15117 df-im 15118 df-sqrt 15252 df-abs 15253 df-dvds 16277 df-gcd 16519 df-prm 16696 df-phi 16791

This theorem is referenced by: cshwshashlem2 17122

W3C validator