2cshwcshw

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)

		Ref	Expression
	Assertion	2cshwcshw	$⊢ (Y \in Word V \land \|Y\| = N) \to ((K \in (0 \dots N) \land X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n)$

Proof

Step	Hyp	Ref	Expression
1		difelfznle	$⊢ (K \in (0 \dots N) \land m \in (0 \dots N) \land \neg K \leq m) \to m + N - K \in (0 \dots N)$
2	1	3exp	$⊢ K \in (0 \dots N) \to (m \in (0 \dots N) \to (\neg K \leq m \to m + N - K \in (0 \dots N)))$
3	2	ad2antrr	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \to (m \in (0 \dots N) \to (\neg K \leq m \to m + N - K \in (0 \dots N)))$
4	3	imp	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \to (\neg K \leq m \to m + N - K \in (0 \dots N))$
5	4	adantr	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to (\neg K \leq m \to m + N - K \in (0 \dots N))$
6	5	com12	$⊢ \neg K \leq m \to (((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to m + N - K \in (0 \dots N))$
7	6	adantl	$⊢ (\neg m = 0 \land \neg K \leq m) \to (((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to m + N - K \in (0 \dots N))$
8	7	imp	$⊢ ((\neg m = 0 \land \neg K \leq m) \land ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m)) \to m + N - K \in (0 \dots N)$
9		simprl	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to Y \in Word V$
10	9	ad2antrr	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to Y \in Word V$
11		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
12	11	adantr	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to K \in ℤ$
13	12	ad2antrr	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to K \in ℤ$
14		elfz2	$⊢ K \in (0 \dots N) \leftrightarrow ((0 \in ℤ \land N \in ℤ \land K \in ℤ) \land (0 \leq K \land K \leq N))$
15		zaddcl	$⊢ (m \in ℤ \land N \in ℤ) \to m + N \in ℤ$
16	15	adantrr	$⊢ (m \in ℤ \land (N \in ℤ \land K \in ℤ)) \to m + N \in ℤ$
17		simprr	$⊢ (m \in ℤ \land (N \in ℤ \land K \in ℤ)) \to K \in ℤ$
18	16 17	zsubcld	$⊢ (m \in ℤ \land (N \in ℤ \land K \in ℤ)) \to m + N - K \in ℤ$
19	18	ex	$⊢ m \in ℤ \to ((N \in ℤ \land K \in ℤ) \to m + N - K \in ℤ)$
20		elfzelz	$⊢ m \in (0 \dots N) \to m \in ℤ$
21	19 20	syl11	$⊢ (N \in ℤ \land K \in ℤ) \to (m \in (0 \dots N) \to m + N - K \in ℤ)$
22	21	3adant1	$⊢ (0 \in ℤ \land N \in ℤ \land K \in ℤ) \to (m \in (0 \dots N) \to m + N - K \in ℤ)$
23	22	adantr	$⊢ ((0 \in ℤ \land N \in ℤ \land K \in ℤ) \land (0 \leq K \land K \leq N)) \to (m \in (0 \dots N) \to m + N - K \in ℤ)$
24	14 23	sylbi	$⊢ K \in (0 \dots N) \to (m \in (0 \dots N) \to m + N - K \in ℤ)$
25	24	ad2antrr	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \to (m \in (0 \dots N) \to m + N - K \in ℤ)$
26	25	imp	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to m + N - K \in ℤ$
27		2cshw	$⊢ (Y \in Word V \land K \in ℤ \land m + N - K \in ℤ) \to (Y cyclShift K) cyclShift (m + N - K) = Y cyclShift (K + (m + N) - K)$
28	10 13 26 27	syl3anc	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to (Y cyclShift K) cyclShift (m + N - K) = Y cyclShift (K + (m + N) - K)$
29	17 18	zaddcld	$⊢ (m \in ℤ \land (N \in ℤ \land K \in ℤ)) \to K + (m + N) - K \in ℤ$
30	29	ex	$⊢ m \in ℤ \to ((N \in ℤ \land K \in ℤ) \to K + (m + N) - K \in ℤ)$
31	30 20	syl11	$⊢ (N \in ℤ \land K \in ℤ) \to (m \in (0 \dots N) \to K + (m + N) - K \in ℤ)$
32	31	3adant1	$⊢ (0 \in ℤ \land N \in ℤ \land K \in ℤ) \to (m \in (0 \dots N) \to K + (m + N) - K \in ℤ)$
33	32	adantr	$⊢ ((0 \in ℤ \land N \in ℤ \land K \in ℤ) \land (0 \leq K \land K \leq N)) \to (m \in (0 \dots N) \to K + (m + N) - K \in ℤ)$
34	14 33	sylbi	$⊢ K \in (0 \dots N) \to (m \in (0 \dots N) \to K + (m + N) - K \in ℤ)$
35	34	ad2antrr	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \to (m \in (0 \dots N) \to K + (m + N) - K \in ℤ)$
36	35	imp	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to K + (m + N) - K \in ℤ$
37		cshwsublen	$⊢ (Y \in Word V \land K + (m + N) - K \in ℤ) \to Y cyclShift (K + (m + N) - K) = Y cyclShift (K + (m + N - K) - \|Y\|)$
38	10 36 37	syl2anc	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to Y cyclShift (K + (m + N) - K) = Y cyclShift (K + (m + N - K) - \|Y\|)$
39	28 38	eqtrd	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to (Y cyclShift K) cyclShift (m + N - K) = Y cyclShift (K + (m + N - K) - \|Y\|)$
40		elfz2nn0	$⊢ K \in (0 \dots N) \leftrightarrow (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N)$
41		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
42		nn0cn	$⊢ K \in ℕ_{0} \to K \in ℂ$
43		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
44	42 43	anim12i	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to (K \in ℂ \land N \in ℂ)$
45		simprl	$⊢ (m \in ℂ \land (K \in ℂ \land N \in ℂ)) \to K \in ℂ$
46		addcl	$⊢ (m \in ℂ \land N \in ℂ) \to m + N \in ℂ$
47	46	adantrl	$⊢ (m \in ℂ \land (K \in ℂ \land N \in ℂ)) \to m + N \in ℂ$
48	45 47	pncan3d	$⊢ (m \in ℂ \land (K \in ℂ \land N \in ℂ)) \to K + (m + N) - K = m + N$
49	48	oveq1d	$⊢ (m \in ℂ \land (K \in ℂ \land N \in ℂ)) \to K + (m + N - K) - N = m + N - N$
50		pncan	$⊢ (m \in ℂ \land N \in ℂ) \to m + N - N = m$
51	50	adantrl	$⊢ (m \in ℂ \land (K \in ℂ \land N \in ℂ)) \to m + N - N = m$
52	49 51	eqtrd	$⊢ (m \in ℂ \land (K \in ℂ \land N \in ℂ)) \to K + (m + N - K) - N = m$
53	41 44 52	syl2an	$⊢ (m \in ℕ_{0} \land (K \in ℕ_{0} \land N \in ℕ_{0})) \to K + (m + N - K) - N = m$
54	53	ex	$⊢ m \in ℕ_{0} \to ((K \in ℕ_{0} \land N \in ℕ_{0}) \to K + (m + N - K) - N = m)$
55		elfznn0	$⊢ m \in (0 \dots N) \to m \in ℕ_{0}$
56	54 55	syl11	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0}) \to (m \in (0 \dots N) \to K + (m + N - K) - N = m)$
57	56	3adant3	$⊢ (K \in ℕ_{0} \land N \in ℕ_{0} \land K \leq N) \to (m \in (0 \dots N) \to K + (m + N - K) - N = m)$
58	40 57	sylbi	$⊢ K \in (0 \dots N) \to (m \in (0 \dots N) \to K + (m + N - K) - N = m)$
59	58	adantr	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (m \in (0 \dots N) \to K + (m + N - K) - N = m)$
60		oveq2	$⊢ \|Y\| = N \to K + (m + N - K) - \|Y\| = K + (m + N - K) - N$
61	60	eqeq1d	$⊢ \|Y\| = N \to (K + (m + N - K) - \|Y\| = m \leftrightarrow K + (m + N - K) - N = m)$
62	61	imbi2d	$⊢ \|Y\| = N \to ((m \in (0 \dots N) \to K + (m + N - K) - \|Y\| = m) \leftrightarrow (m \in (0 \dots N) \to K + (m + N - K) - N = m))$
63	62	adantl	$⊢ (Y \in Word V \land \|Y\| = N) \to ((m \in (0 \dots N) \to K + (m + N - K) - \|Y\| = m) \leftrightarrow (m \in (0 \dots N) \to K + (m + N - K) - N = m))$
64	63	adantl	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to ((m \in (0 \dots N) \to K + (m + N - K) - \|Y\| = m) \leftrightarrow (m \in (0 \dots N) \to K + (m + N - K) - N = m))$
65	59 64	mpbird	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (m \in (0 \dots N) \to K + (m + N - K) - \|Y\| = m)$
66	65	adantr	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \to (m \in (0 \dots N) \to K + (m + N - K) - \|Y\| = m)$
67	66	imp	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to K + (m + N - K) - \|Y\| = m$
68	67	oveq2d	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to Y cyclShift (K + (m + N - K) - \|Y\|) = Y cyclShift m$
69	39 68	eqtr2d	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \to Y cyclShift m = (Y cyclShift K) cyclShift (m + N - K)$
70	69	adantr	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to Y cyclShift m = (Y cyclShift K) cyclShift (m + N - K)$
71		oveq1	$⊢ X = Y cyclShift K \to X cyclShift (m + N - K) = (Y cyclShift K) cyclShift (m + N - K)$
72	71	adantl	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to X cyclShift (m + N - K) = (Y cyclShift K) cyclShift (m + N - K)$
73	70 72	eqtr4d	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land (\neg m = 0 \land \neg K \leq m)) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to Y cyclShift m = X cyclShift (m + N - K)$
74	73	exp41	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to ((\neg m = 0 \land \neg K \leq m) \to (m \in (0 \dots N) \to (X = Y cyclShift K \to Y cyclShift m = X cyclShift (m + N - K))))$
75	74	com24	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (X = Y cyclShift K \to (m \in (0 \dots N) \to ((\neg m = 0 \land \neg K \leq m) \to Y cyclShift m = X cyclShift (m + N - K))))$
76	75	imp41	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land (\neg m = 0 \land \neg K \leq m)) \to Y cyclShift m = X cyclShift (m + N - K)$
77	76	eqeq2d	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land (\neg m = 0 \land \neg K \leq m)) \to (Z = Y cyclShift m \leftrightarrow Z = X cyclShift (m + N - K))$
78	77	biimpd	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land (\neg m = 0 \land \neg K \leq m)) \to (Z = Y cyclShift m \to Z = X cyclShift (m + N - K))$
79	78	impancom	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to ((\neg m = 0 \land \neg K \leq m) \to Z = X cyclShift (m + N - K))$
80	79	impcom	$⊢ ((\neg m = 0 \land \neg K \leq m) \land ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m)) \to Z = X cyclShift (m + N - K)$
81		oveq2	$⊢ n = m + N - K \to X cyclShift n = X cyclShift (m + N - K)$
82	81	rspceeqv	$⊢ (m + N - K \in (0 \dots N) \land Z = X cyclShift (m + N - K)) \to \exists n \in (0 \dots N) Z = X cyclShift n$
83	8 80 82	syl2anc	$⊢ ((\neg m = 0 \land \neg K \leq m) \land ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m)) \to \exists n \in (0 \dots N) Z = X cyclShift n$
84	83	exp31	$⊢ \neg m = 0 \to (\neg K \leq m \to (((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n))$
85		oveq2	$⊢ m = 0 \to Y cyclShift m = Y cyclShift 0$
86	85	eqeq2d	$⊢ m = 0 \to (Z = Y cyclShift m \leftrightarrow Z = Y cyclShift 0)$
87		cshw0	$⊢ Y \in Word V \to Y cyclShift 0 = Y$
88	87	adantr	$⊢ (Y \in Word V \land \|Y\| = N) \to Y cyclShift 0 = Y$
89	88	eqeq2d	$⊢ (Y \in Word V \land \|Y\| = N) \to (Z = Y cyclShift 0 \leftrightarrow Z = Y)$
90		fznn0sub2	$⊢ K \in (0 \dots N) \to N - K \in (0 \dots N)$
91	90	adantl	$⊢ ((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \to N - K \in (0 \dots N)$
92		oveq1	$⊢ \|Y\| = N \to \|Y\| - K = N - K$
93	92	eleq1d	$⊢ \|Y\| = N \to (\|Y\| - K \in (0 \dots N) \leftrightarrow N - K \in (0 \dots N))$
94	93	ad2antlr	$⊢ ((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \to (\|Y\| - K \in (0 \dots N) \leftrightarrow N - K \in (0 \dots N))$
95	91 94	mpbird	$⊢ ((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \to \|Y\| - K \in (0 \dots N)$
96	95	adantr	$⊢ (((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \land X = Y cyclShift K) \to \|Y\| - K \in (0 \dots N)$
97		oveq1	$⊢ X = Y cyclShift K \to X cyclShift (\|Y\| - K) = (Y cyclShift K) cyclShift (\|Y\| - K)$
98		simpl	$⊢ (Y \in Word V \land \|Y\| = N) \to Y \in Word V$
99		2cshwid	$⊢ (Y \in Word V \land K \in ℤ) \to (Y cyclShift K) cyclShift (\|Y\| - K) = Y$
100	98 11 99	syl2an	$⊢ ((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \to (Y cyclShift K) cyclShift (\|Y\| - K) = Y$
101	97 100	sylan9eqr	$⊢ (((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \land X = Y cyclShift K) \to X cyclShift (\|Y\| - K) = Y$
102	101	eqcomd	$⊢ (((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \land X = Y cyclShift K) \to Y = X cyclShift (\|Y\| - K)$
103		oveq2	$⊢ n = \|Y\| - K \to X cyclShift n = X cyclShift (\|Y\| - K)$
104	103	rspceeqv	$⊢ (\|Y\| - K \in (0 \dots N) \land Y = X cyclShift (\|Y\| - K)) \to \exists n \in (0 \dots N) Y = X cyclShift n$
105	96 102 104	syl2anc	$⊢ (((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \land X = Y cyclShift K) \to \exists n \in (0 \dots N) Y = X cyclShift n$
106	105	adantr	$⊢ ((((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \land X = Y cyclShift K) \land Z = Y) \to \exists n \in (0 \dots N) Y = X cyclShift n$
107		eqeq1	$⊢ Z = Y \to (Z = X cyclShift n \leftrightarrow Y = X cyclShift n)$
108	107	rexbidv	$⊢ Z = Y \to (\exists n \in (0 \dots N) Z = X cyclShift n \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)$
109	108	adantl	$⊢ ((((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \land X = Y cyclShift K) \land Z = Y) \to (\exists n \in (0 \dots N) Z = X cyclShift n \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)$
110	106 109	mpbird	$⊢ ((((Y \in Word V \land \|Y\| = N) \land K \in (0 \dots N)) \land X = Y cyclShift K) \land Z = Y) \to \exists n \in (0 \dots N) Z = X cyclShift n$
111	110	exp41	$⊢ (Y \in Word V \land \|Y\| = N) \to (K \in (0 \dots N) \to (X = Y cyclShift K \to (Z = Y \to \exists n \in (0 \dots N) Z = X cyclShift n)))$
112	111	com24	$⊢ (Y \in Word V \land \|Y\| = N) \to (Z = Y \to (X = Y cyclShift K \to (K \in (0 \dots N) \to \exists n \in (0 \dots N) Z = X cyclShift n)))$
113	89 112	sylbid	$⊢ (Y \in Word V \land \|Y\| = N) \to (Z = Y cyclShift 0 \to (X = Y cyclShift K \to (K \in (0 \dots N) \to \exists n \in (0 \dots N) Z = X cyclShift n)))$
114	113	com24	$⊢ (Y \in Word V \land \|Y\| = N) \to (K \in (0 \dots N) \to (X = Y cyclShift K \to (Z = Y cyclShift 0 \to \exists n \in (0 \dots N) Z = X cyclShift n)))$
115	114	impcom	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (X = Y cyclShift K \to (Z = Y cyclShift 0 \to \exists n \in (0 \dots N) Z = X cyclShift n))$
116	115	com13	$⊢ Z = Y cyclShift 0 \to (X = Y cyclShift K \to ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to \exists n \in (0 \dots N) Z = X cyclShift n))$
117	116	a1d	$⊢ Z = Y cyclShift 0 \to (m \in (0 \dots N) \to (X = Y cyclShift K \to ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to \exists n \in (0 \dots N) Z = X cyclShift n)))$
118	86 117	biimtrdi	$⊢ m = 0 \to (Z = Y cyclShift m \to (m \in (0 \dots N) \to (X = Y cyclShift K \to ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to \exists n \in (0 \dots N) Z = X cyclShift n))))$
119	118	com24	$⊢ m = 0 \to (X = Y cyclShift K \to (m \in (0 \dots N) \to (Z = Y cyclShift m \to ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to \exists n \in (0 \dots N) Z = X cyclShift n))))$
120	119	com15	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (X = Y cyclShift K \to (m \in (0 \dots N) \to (Z = Y cyclShift m \to (m = 0 \to \exists n \in (0 \dots N) Z = X cyclShift n))))$
121	120	imp41	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to (m = 0 \to \exists n \in (0 \dots N) Z = X cyclShift n)$
122	121	com12	$⊢ m = 0 \to (((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n)$
123		difelfzle	$⊢ (K \in (0 \dots N) \land m \in (0 \dots N) \land K \leq m) \to m - K \in (0 \dots N)$
124	123	3exp	$⊢ K \in (0 \dots N) \to (m \in (0 \dots N) \to (K \leq m \to m - K \in (0 \dots N)))$
125	124	ad2antrr	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \to (m \in (0 \dots N) \to (K \leq m \to m - K \in (0 \dots N)))$
126	125	imp	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \to (K \leq m \to m - K \in (0 \dots N))$
127	126	adantr	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to (K \leq m \to m - K \in (0 \dots N))$
128	127	impcom	$⊢ (K \leq m \land ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m)) \to m - K \in (0 \dots N)$
129	9	ad2antrr	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \to Y \in Word V$
130	12	ad2antrr	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \to K \in ℤ$
131		zsubcl	$⊢ (m \in ℤ \land K \in ℤ) \to m - K \in ℤ$
132	131	ex	$⊢ m \in ℤ \to (K \in ℤ \to m - K \in ℤ)$
133	20 11 132	syl2imc	$⊢ K \in (0 \dots N) \to (m \in (0 \dots N) \to m - K \in ℤ)$
134	133	ad2antrr	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \to (m \in (0 \dots N) \to m - K \in ℤ)$
135	134	imp	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \to m - K \in ℤ$
136		2cshw	$⊢ (Y \in Word V \land K \in ℤ \land m - K \in ℤ) \to (Y cyclShift K) cyclShift (m - K) = Y cyclShift (K + m - K)$
137	129 130 135 136	syl3anc	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \to (Y cyclShift K) cyclShift (m - K) = Y cyclShift (K + m - K)$
138		zcn	$⊢ K \in ℤ \to K \in ℂ$
139	20	zcnd	$⊢ m \in (0 \dots N) \to m \in ℂ$
140		pncan3	$⊢ (K \in ℂ \land m \in ℂ) \to K + m - K = m$
141	138 139 140	syl2anr	$⊢ (m \in (0 \dots N) \land K \in ℤ) \to K + m - K = m$
142	141	ex	$⊢ m \in (0 \dots N) \to (K \in ℤ \to K + m - K = m)$
143	11 142	syl5com	$⊢ K \in (0 \dots N) \to (m \in (0 \dots N) \to K + m - K = m)$
144	143	ad2antrr	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \to (m \in (0 \dots N) \to K + m - K = m)$
145	144	imp	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \to K + m - K = m$
146	145	oveq2d	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \to Y cyclShift (K + m - K) = Y cyclShift m$
147	137 146	eqtr2d	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \to Y cyclShift m = (Y cyclShift K) cyclShift (m - K)$
148	147	adantr	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to Y cyclShift m = (Y cyclShift K) cyclShift (m - K)$
149		oveq1	$⊢ X = Y cyclShift K \to X cyclShift (m - K) = (Y cyclShift K) cyclShift (m - K)$
150	149	eqeq2d	$⊢ X = Y cyclShift K \to (Y cyclShift m = X cyclShift (m - K) \leftrightarrow Y cyclShift m = (Y cyclShift K) cyclShift (m - K))$
151	150	adantl	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to (Y cyclShift m = X cyclShift (m - K) \leftrightarrow Y cyclShift m = (Y cyclShift K) cyclShift (m - K))$
152	148 151	mpbird	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to Y cyclShift m = X cyclShift (m - K)$
153	152	eqeq2d	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to (Z = Y cyclShift m \leftrightarrow Z = X cyclShift (m - K))$
154	153	biimpd	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land K \leq m) \land m \in (0 \dots N)) \land X = Y cyclShift K) \to (Z = Y cyclShift m \to Z = X cyclShift (m - K))$
155	154	exp41	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (K \leq m \to (m \in (0 \dots N) \to (X = Y cyclShift K \to (Z = Y cyclShift m \to Z = X cyclShift (m - K)))))$
156	155	com24	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (X = Y cyclShift K \to (m \in (0 \dots N) \to (K \leq m \to (Z = Y cyclShift m \to Z = X cyclShift (m - K)))))$
157	156	imp31	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \to (K \leq m \to (Z = Y cyclShift m \to Z = X cyclShift (m - K)))$
158	157	com23	$⊢ (((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \to (Z = Y cyclShift m \to (K \leq m \to Z = X cyclShift (m - K)))$
159	158	imp	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to (K \leq m \to Z = X cyclShift (m - K))$
160	159	impcom	$⊢ (K \leq m \land ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m)) \to Z = X cyclShift (m - K)$
161		oveq2	$⊢ n = m - K \to X cyclShift n = X cyclShift (m - K)$
162	161	rspceeqv	$⊢ (m - K \in (0 \dots N) \land Z = X cyclShift (m - K)) \to \exists n \in (0 \dots N) Z = X cyclShift n$
163	128 160 162	syl2anc	$⊢ (K \leq m \land ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m)) \to \exists n \in (0 \dots N) Z = X cyclShift n$
164	163	ex	$⊢ K \leq m \to (((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n)$
165	84 122 164	pm2.61ii	$⊢ ((((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \land m \in (0 \dots N)) \land Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n$
166	165	rexlimdva2	$⊢ ((K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \land X = Y cyclShift K) \to (\exists m \in (0 \dots N) Z = Y cyclShift m \to \exists n \in (0 \dots N) Z = X cyclShift n)$
167	166	ex	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (X = Y cyclShift K \to (\exists m \in (0 \dots N) Z = Y cyclShift m \to \exists n \in (0 \dots N) Z = X cyclShift n))$
168	167	com23	$⊢ (K \in (0 \dots N) \land (Y \in Word V \land \|Y\| = N)) \to (\exists m \in (0 \dots N) Z = Y cyclShift m \to (X = Y cyclShift K \to \exists n \in (0 \dots N) Z = X cyclShift n))$
169	168	ex	$⊢ K \in (0 \dots N) \to ((Y \in Word V \land \|Y\| = N) \to (\exists m \in (0 \dots N) Z = Y cyclShift m \to (X = Y cyclShift K \to \exists n \in (0 \dots N) Z = X cyclShift n)))$
170	169	com24	$⊢ K \in (0 \dots N) \to (X = Y cyclShift K \to (\exists m \in (0 \dots N) Z = Y cyclShift m \to ((Y \in Word V \land \|Y\| = N) \to \exists n \in (0 \dots N) Z = X cyclShift n)))$
171	170	3imp	$⊢ (K \in (0 \dots N) \land X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m) \to ((Y \in Word V \land \|Y\| = N) \to \exists n \in (0 \dots N) Z = X cyclShift n)$
172	171	com12	$⊢ (Y \in Word V \land \|Y\| = N) \to ((K \in (0 \dots N) \land X = Y cyclShift K \land \exists m \in (0 \dots N) Z = Y cyclShift m) \to \exists n \in (0 \dots N) Z = X cyclShift n)$

Metamath Proof Explorer

Theorem 2cshwcshw

Proof