eucrctshift

Description: Cyclically shifting the indices of an Eulerian circuit <. F , P >. results in an Eulerian circuit <. H , Q >. . (Contributed by AV, 15-Mar-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypotheses	eucrctshift.v	$⊢ V = Vtx (G)$
	eucrctshift.i	$⊢ I = iEdg (G)$
	eucrctshift.c	$⊢ φ \to F Circuits (G) P$
	eucrctshift.n	$⊢ N = \|F\|$
	eucrctshift.s	$⊢ φ \to S \in (0 ..^N)$
	eucrctshift.h	$⊢ H = F cyclShift S$
	eucrctshift.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
	eucrctshift.e	$⊢ φ \to F EulerPaths (G) P$
Assertion	eucrctshift	$⊢ φ \to (H EulerPaths (G) Q \land H Circuits (G) Q)$

Proof

Step	Hyp	Ref	Expression
1		eucrctshift.v	$⊢ V = Vtx (G)$
2		eucrctshift.i	$⊢ I = iEdg (G)$
3		eucrctshift.c	$⊢ φ \to F Circuits (G) P$
4		eucrctshift.n	$⊢ N = \|F\|$
5		eucrctshift.s	$⊢ φ \to S \in (0 ..^N)$
6		eucrctshift.h	$⊢ H = F cyclShift S$
7		eucrctshift.q	$⊢ Q = (x \in (0 \dots N) ⟼ if (x \leq N - S, P (x + S), P (x + S - N)))$
8		eucrctshift.e	$⊢ φ \to F EulerPaths (G) P$
9	1 2 3 4 5 6 7	crctcshtrl	$⊢ φ \to H Trails (G) Q$
10		simpr	$⊢ (φ \land H Trails (G) Q) \to H Trails (G) Q$
11	2	eupthf1o	$⊢ F EulerPaths (G) P \to F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I$
12	8 11	syl	$⊢ φ \to F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I$
13	12	adantr	$⊢ (φ \land H Trails (G) Q) \to F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I$
14		trliswlk	$⊢ H Trails (G) Q \to H Walks (G) Q$
15	2	wlkf	$⊢ H Walks (G) Q \to H \in Word dom I$
16		wrdf	$⊢ H \in Word dom I \to H : (0 ..^\|H\|) ⟶ dom I$
17	14 15 16	3syl	$⊢ H Trails (G) Q \to H : (0 ..^\|H\|) ⟶ dom I$
18		df-f1o	$⊢ F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land F : (0 ..^\|F\|) \underset{onto}{⟶} dom I)$
19		dffo3	$⊢ F : (0 ..^\|F\|) \underset{onto}{⟶} dom I \leftrightarrow (F : (0 ..^\|F\|) ⟶ dom I \land \forall i \in dom I \exists y \in (0 ..^\|F\|) i = F (y))$
20		crctiswlk	$⊢ F Circuits (G) P \to F Walks (G) P$
21	2	wlkf	$⊢ F Walks (G) P \to F \in Word dom I$
22		lencl	$⊢ F \in Word dom I \to \|F\| \in ℕ_{0}$
23	4	oveq2i	$⊢ (0 ..^N) = (0 ..^\|F\|)$
24	23	eleq2i	$⊢ S \in (0 ..^N) \leftrightarrow S \in (0 ..^\|F\|)$
25		elfzonn0	$⊢ S \in (0 ..^\|F\|) \to S \in ℕ_{0}$
26	25	adantl	$⊢ (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \to S \in ℕ_{0}$
27		elfzonn0	$⊢ y \in (0 ..^\|F\|) \to y \in ℕ_{0}$
28		nn0sub	$⊢ (S \in ℕ_{0} \land y \in ℕ_{0}) \to (S \leq y \leftrightarrow y - S \in ℕ_{0})$
29	26 27 28	syl2an	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to (S \leq y \leftrightarrow y - S \in ℕ_{0})$
30	29	biimpac	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to y - S \in ℕ_{0}$
31		elfzo0	$⊢ y \in (0 ..^\|F\|) \leftrightarrow (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|)$
32		simp2	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to \|F\| \in ℕ$
33	31 32	sylbi	$⊢ y \in (0 ..^\|F\|) \to \|F\| \in ℕ$
34	33	ad2antll	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to \|F\| \in ℕ$
35		nn0re	$⊢ y \in ℕ_{0} \to y \in ℝ$
36	35	ad2antrr	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to y \in ℝ$
37		nnre	$⊢ \|F\| \in ℕ \to \|F\| \in ℝ$
38	37	adantl	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ) \to \|F\| \in ℝ$
39	38	adantr	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to \|F\| \in ℝ$
40		elfzoelz	$⊢ S \in (0 ..^\|F\|) \to S \in ℤ$
41	40	zred	$⊢ S \in (0 ..^\|F\|) \to S \in ℝ$
42		readdcl	$⊢ (\|F\| \in ℝ \land S \in ℝ) \to \|F\| + S \in ℝ$
43	38 41 42	syl2an	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to \|F\| + S \in ℝ$
44	36 39 43	3jca	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to (y \in ℝ \land \|F\| \in ℝ \land \|F\| + S \in ℝ)$
45		elfzole1	$⊢ S \in (0 ..^\|F\|) \to 0 \leq S$
46	45	adantl	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to 0 \leq S$
47		addge01	$⊢ (\|F\| \in ℝ \land S \in ℝ) \to (0 \leq S \leftrightarrow \|F\| \leq \|F\| + S)$
48	38 41 47	syl2an	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to (0 \leq S \leftrightarrow \|F\| \leq \|F\| + S)$
49	46 48	mpbid	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to \|F\| \leq \|F\| + S$
50	44 49	lelttrdi	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ) \land S \in (0 ..^\|F\|)) \to (y < \|F\| \to y < \|F\| + S)$
51	50	ex	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ) \to (S \in (0 ..^\|F\|) \to (y < \|F\| \to y < \|F\| + S))$
52	51	com23	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ) \to (y < \|F\| \to (S \in (0 ..^\|F\|) \to y < \|F\| + S))$
53	52	3impia	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to (S \in (0 ..^\|F\|) \to y < \|F\| + S)$
54	53	adantld	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \to y < \|F\| + S)$
55	54	imp	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \land (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|))) \to y < \|F\| + S$
56	35	3ad2ant1	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to y \in ℝ$
57	56	adantr	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \land (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|))) \to y \in ℝ$
58	41	ad2antll	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \land (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|))) \to S \in ℝ$
59		elfzoel2	$⊢ S \in (0 ..^\|F\|) \to \|F\| \in ℤ$
60	59	zred	$⊢ S \in (0 ..^\|F\|) \to \|F\| \in ℝ$
61	60	ad2antll	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \land (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|))) \to \|F\| \in ℝ$
62	57 58 61	ltsubaddd	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \land (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|))) \to (y - S < \|F\| \leftrightarrow y < \|F\| + S)$
63	55 62	mpbird	$⊢ ((y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \land (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|))) \to y - S < \|F\|$
64	63	ex	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \to y - S < \|F\|)$
65	31 64	sylbi	$⊢ y \in (0 ..^\|F\|) \to ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \to y - S < \|F\|)$
66	65	impcom	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to y - S < \|F\|$
67	66	adantl	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to y - S < \|F\|$
68		elfzo0	$⊢ y - S \in (0 ..^\|F\|) \leftrightarrow (y - S \in ℕ_{0} \land \|F\| \in ℕ \land y - S < \|F\|)$
69	30 34 67 68	syl3anbrc	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to y - S \in (0 ..^\|F\|)$
70		oveq1	$⊢ z = y - S \to z + S = y - S + S$
71	70	oveq1d	$⊢ z = y - S \to (z + S) \mod \|F\| = (y - S + S) \mod \|F\|$
72	40	zcnd	$⊢ S \in (0 ..^\|F\|) \to S \in ℂ$
73	72	adantl	$⊢ (\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \to S \in ℂ$
74		elfzoelz	$⊢ y \in (0 ..^\|F\|) \to y \in ℤ$
75	74	zcnd	$⊢ y \in (0 ..^\|F\|) \to y \in ℂ$
76	73 75	anim12ci	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to (y \in ℂ \land S \in ℂ)$
77	76	adantl	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (y \in ℂ \land S \in ℂ)$
78		npcan	$⊢ (y \in ℂ \land S \in ℂ) \to y - S + S = y$
79	77 78	syl	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to y - S + S = y$
80	79	oveq1d	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (y - S + S) \mod \|F\| = y \mod \|F\|$
81		zmodidfzoimp	$⊢ y \in (0 ..^\|F\|) \to y \mod \|F\| = y$
82	81	ad2antll	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to y \mod \|F\| = y$
83	80 82	eqtrd	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (y - S + S) \mod \|F\| = y$
84	71 83	sylan9eqr	$⊢ ((S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \land z = y - S) \to (z + S) \mod \|F\| = y$
85	84	eqcomd	$⊢ ((S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \land z = y - S) \to y = (z + S) \mod \|F\|$
86	69 85	rspcedeq2vd	$⊢ (S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to \exists z \in (0 ..^\|F\|) y = (z + S) \mod \|F\|$
87		elfzo0	$⊢ S \in (0 ..^\|F\|) \leftrightarrow (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)$
88		nn0cn	$⊢ y \in ℕ_{0} \to y \in ℂ$
89	88	ad2antrr	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to y \in ℂ$
90		nn0cn	$⊢ S \in ℕ_{0} \to S \in ℂ$
91	90	3ad2ant1	$⊢ (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|) \to S \in ℂ$
92	91	adantl	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to S \in ℂ$
93		nncn	$⊢ \|F\| \in ℕ \to \|F\| \in ℂ$
94	93	3ad2ant2	$⊢ (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|) \to \|F\| \in ℂ$
95	94	adantl	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to \|F\| \in ℂ$
96	89 92 95	subadd23d	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to y - S + \|F\| = y + \|F\| - S$
97		simpll	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to y \in ℕ_{0}$
98		nn0z	$⊢ S \in ℕ_{0} \to S \in ℤ$
99		nnz	$⊢ \|F\| \in ℕ \to \|F\| \in ℤ$
100		znnsub	$⊢ (S \in ℤ \land \|F\| \in ℤ) \to (S < \|F\| \leftrightarrow \|F\| - S \in ℕ)$
101	98 99 100	syl2an	$⊢ (S \in ℕ_{0} \land \|F\| \in ℕ) \to (S < \|F\| \leftrightarrow \|F\| - S \in ℕ)$
102	101	biimp3a	$⊢ (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|) \to \|F\| - S \in ℕ$
103	102	adantl	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to \|F\| - S \in ℕ$
104	103	nnnn0d	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to \|F\| - S \in ℕ_{0}$
105	97 104	nn0addcld	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to y + \|F\| - S \in ℕ_{0}$
106	96 105	eqeltrd	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to y - S + \|F\| \in ℕ_{0}$
107	106	adantr	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to y - S + \|F\| \in ℕ_{0}$
108		simplr2	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to \|F\| \in ℕ$
109	88	adantr	$⊢ (y \in ℕ_{0} \land y < \|F\|) \to y \in ℂ$
110		subcl	$⊢ (y \in ℂ \land S \in ℂ) \to y - S \in ℂ$
111	109 91 110	syl2an	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to y - S \in ℂ$
112	95 111	jca	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to (\|F\| \in ℂ \land y - S \in ℂ)$
113	112	adantr	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to (\|F\| \in ℂ \land y - S \in ℂ)$
114		addcom	$⊢ (\|F\| \in ℂ \land y - S \in ℂ) \to \|F\| + y - S = y - S + \|F\|$
115	113 114	syl	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to \|F\| + y - S = y - S + \|F\|$
116	35	adantr	$⊢ (y \in ℕ_{0} \land y < \|F\|) \to y \in ℝ$
117		nn0re	$⊢ S \in ℕ_{0} \to S \in ℝ$
118	117	3ad2ant1	$⊢ (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|) \to S \in ℝ$
119		ltnle	$⊢ (y \in ℝ \land S \in ℝ) \to (y < S \leftrightarrow \neg S \leq y)$
120		simpl	$⊢ (y \in ℝ \land S \in ℝ) \to y \in ℝ$
121		simpr	$⊢ (y \in ℝ \land S \in ℝ) \to S \in ℝ$
122	120 121	sublt0d	$⊢ (y \in ℝ \land S \in ℝ) \to (y - S < 0 \leftrightarrow y < S)$
123	122	biimprd	$⊢ (y \in ℝ \land S \in ℝ) \to (y < S \to y - S < 0)$
124	119 123	sylbird	$⊢ (y \in ℝ \land S \in ℝ) \to (\neg S \leq y \to y - S < 0)$
125	116 118 124	syl2an	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to (\neg S \leq y \to y - S < 0)$
126	125	imp	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to y - S < 0$
127		resubcl	$⊢ (y \in ℝ \land S \in ℝ) \to y - S \in ℝ$
128	116 118 127	syl2an	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to y - S \in ℝ$
129	37	3ad2ant2	$⊢ (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|) \to \|F\| \in ℝ$
130	129	adantl	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to \|F\| \in ℝ$
131	128 130	jca	$⊢ ((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \to (y - S \in ℝ \land \|F\| \in ℝ)$
132	131	adantr	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to (y - S \in ℝ \land \|F\| \in ℝ)$
133		ltaddneg	$⊢ (y - S \in ℝ \land \|F\| \in ℝ) \to (y - S < 0 \leftrightarrow \|F\| + y - S < \|F\|)$
134	132 133	syl	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to (y - S < 0 \leftrightarrow \|F\| + y - S < \|F\|)$
135	126 134	mpbid	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to \|F\| + y - S < \|F\|$
136	115 135	eqbrtrrd	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to y - S + \|F\| < \|F\|$
137	107 108 136	3jca	$⊢ (((y \in ℕ_{0} \land y < \|F\|) \land (S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|)) \land \neg S \leq y) \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)$
138	137	exp31	$⊢ (y \in ℕ_{0} \land y < \|F\|) \to ((S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|) \to (\neg S \leq y \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)))$
139	138	3adant2	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to ((S \in ℕ_{0} \land \|F\| \in ℕ \land S < \|F\|) \to (\neg S \leq y \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)))$
140	87 139	syl5bi	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to (S \in (0 ..^\|F\|) \to (\neg S \leq y \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)))$
141	140	adantld	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \to (\neg S \leq y \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)))$
142	31 141	sylbi	$⊢ y \in (0 ..^\|F\|) \to ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \to (\neg S \leq y \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)))$
143	142	impcom	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to (\neg S \leq y \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|))$
144	143	impcom	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)$
145		elfzo0	$⊢ y - S + \|F\| \in (0 ..^\|F\|) \leftrightarrow (y - S + \|F\| \in ℕ_{0} \land \|F\| \in ℕ \land y - S + \|F\| < \|F\|)$
146	144 145	sylibr	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to y - S + \|F\| \in (0 ..^\|F\|)$
147		oveq1	$⊢ z = y - S + \|F\| \to z + S = (y - S) + \|F\| + S$
148	147	oveq1d	$⊢ z = y - S + \|F\| \to (z + S) \mod \|F\| = ((y - S) + \|F\| + S) \mod \|F\|$
149	73	adantr	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to S \in ℂ$
150	75	adantl	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to y \in ℂ$
151		nn0cn	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℂ$
152	151	ad2antrr	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to \|F\| \in ℂ$
153	149 150 152	3jca	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to (S \in ℂ \land y \in ℂ \land \|F\| \in ℂ)$
154	153	adantl	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (S \in ℂ \land y \in ℂ \land \|F\| \in ℂ)$
155		simp2	$⊢ (S \in ℂ \land y \in ℂ \land \|F\| \in ℂ) \to y \in ℂ$
156		simp3	$⊢ (S \in ℂ \land y \in ℂ \land \|F\| \in ℂ) \to \|F\| \in ℂ$
157		simp1	$⊢ (S \in ℂ \land y \in ℂ \land \|F\| \in ℂ) \to S \in ℂ$
158	155 157 156	nppcand	$⊢ (S \in ℂ \land y \in ℂ \land \|F\| \in ℂ) \to (y - S) + \|F\| + S = y + \|F\|$
159	155 156 158	comraddd	$⊢ (S \in ℂ \land y \in ℂ \land \|F\| \in ℂ) \to (y - S) + \|F\| + S = \|F\| + y$
160	154 159	syl	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (y - S) + \|F\| + S = \|F\| + y$
161	160	oveq1d	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to ((y - S) + \|F\| + S) \mod \|F\| = (\|F\| + y) \mod \|F\|$
162	31	biimpi	$⊢ y \in (0 ..^\|F\|) \to (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|)$
163	162	ad2antll	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|)$
164		addmodid	$⊢ (y \in ℕ_{0} \land \|F\| \in ℕ \land y < \|F\|) \to (\|F\| + y) \mod \|F\| = y$
165	163 164	syl	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to (\|F\| + y) \mod \|F\| = y$
166	161 165	eqtrd	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to ((y - S) + \|F\| + S) \mod \|F\| = y$
167	148 166	sylan9eqr	$⊢ ((\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \land z = y - S + \|F\|) \to (z + S) \mod \|F\| = y$
168	167	eqcomd	$⊢ ((\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \land z = y - S + \|F\|) \to y = (z + S) \mod \|F\|$
169	146 168	rspcedeq2vd	$⊢ (\neg S \leq y \land ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|))) \to \exists z \in (0 ..^\|F\|) y = (z + S) \mod \|F\|$
170	86 169	pm2.61ian	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to \exists z \in (0 ..^\|F\|) y = (z + S) \mod \|F\|$
171	23	rexeqi	$⊢ \exists z \in (0 ..^N) y = (z + S) \mod \|F\| \leftrightarrow \exists z \in (0 ..^\|F\|) y = (z + S) \mod \|F\|$
172	170 171	sylibr	$⊢ ((\|F\| \in ℕ_{0} \land S \in (0 ..^\|F\|)) \land y \in (0 ..^\|F\|)) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|$
173	172	exp31	$⊢ \|F\| \in ℕ_{0} \to (S \in (0 ..^\|F\|) \to (y \in (0 ..^\|F\|) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|))$
174	24 173	syl5bi	$⊢ \|F\| \in ℕ_{0} \to (S \in (0 ..^N) \to (y \in (0 ..^\|F\|) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|))$
175	22 174	syl	$⊢ F \in Word dom I \to (S \in (0 ..^N) \to (y \in (0 ..^\|F\|) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|))$
176	20 21 175	3syl	$⊢ F Circuits (G) P \to (S \in (0 ..^N) \to (y \in (0 ..^\|F\|) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|))$
177	3 5 176	sylc	$⊢ φ \to (y \in (0 ..^\|F\|) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|)$
178	177	adantr	$⊢ (φ \land i \in dom I) \to (y \in (0 ..^\|F\|) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|)$
179	178	imp	$⊢ ((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|$
180	179	adantr	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to \exists z \in (0 ..^N) y = (z + S) \mod \|F\|$
181		fveq2	$⊢ y = (z + S) \mod \|F\| \to F (y) = F ((z + S) \mod \|F\|)$
182	181	reximi	$⊢ \exists z \in (0 ..^N) y = (z + S) \mod \|F\| \to \exists z \in (0 ..^N) F (y) = F ((z + S) \mod \|F\|)$
183	180 182	syl	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to \exists z \in (0 ..^N) F (y) = F ((z + S) \mod \|F\|)$
184	3 20 21	3syl	$⊢ φ \to F \in Word dom I$
185	184	ad3antrrr	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to F \in Word dom I$
186		elfzoelz	$⊢ S \in (0 ..^N) \to S \in ℤ$
187	5 186	syl	$⊢ φ \to S \in ℤ$
188	187	ad3antrrr	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to S \in ℤ$
189	23	eleq2i	$⊢ z \in (0 ..^N) \leftrightarrow z \in (0 ..^\|F\|)$
190	189	biimpi	$⊢ z \in (0 ..^N) \to z \in (0 ..^\|F\|)$
191		cshwidxmod	$⊢ (F \in Word dom I \land S \in ℤ \land z \in (0 ..^\|F\|)) \to (F cyclShift S) (z) = F ((z + S) \mod \|F\|)$
192	185 188 190 191	syl2an3an	$⊢ ((((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \land z \in (0 ..^N)) \to (F cyclShift S) (z) = F ((z + S) \mod \|F\|)$
193	192	eqeq2d	$⊢ ((((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \land z \in (0 ..^N)) \to (F (y) = (F cyclShift S) (z) \leftrightarrow F (y) = F ((z + S) \mod \|F\|))$
194	193	rexbidva	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to (\exists z \in (0 ..^N) F (y) = (F cyclShift S) (z) \leftrightarrow \exists z \in (0 ..^N) F (y) = F ((z + S) \mod \|F\|))$
195	183 194	mpbird	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to \exists z \in (0 ..^N) F (y) = (F cyclShift S) (z)$
196	1 2 3 4 5 6	crctcshlem2	$⊢ φ \to \|H\| = N$
197	196	oveq2d	$⊢ φ \to (0 ..^\|H\|) = (0 ..^N)$
198	197	ad3antrrr	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to (0 ..^\|H\|) = (0 ..^N)$
199		simpr	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to i = F (y)$
200	6	fveq1i	$⊢ H (z) = (F cyclShift S) (z)$
201	200	a1i	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to H (z) = (F cyclShift S) (z)$
202	199 201	eqeq12d	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to (i = H (z) \leftrightarrow F (y) = (F cyclShift S) (z))$
203	198 202	rexeqbidv	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to (\exists z \in (0 ..^\|H\|) i = H (z) \leftrightarrow \exists z \in (0 ..^N) F (y) = (F cyclShift S) (z))$
204	195 203	mpbird	$⊢ (((φ \land i \in dom I) \land y \in (0 ..^\|F\|)) \land i = F (y)) \to \exists z \in (0 ..^\|H\|) i = H (z)$
205	204	rexlimdva2	$⊢ (φ \land i \in dom I) \to (\exists y \in (0 ..^\|F\|) i = F (y) \to \exists z \in (0 ..^\|H\|) i = H (z))$
206	205	ralimdva	$⊢ φ \to (\forall i \in dom I \exists y \in (0 ..^\|F\|) i = F (y) \to \forall i \in dom I \exists z \in (0 ..^\|H\|) i = H (z))$
207	206	impcom	$⊢ (\forall i \in dom I \exists y \in (0 ..^\|F\|) i = F (y) \land φ) \to \forall i \in dom I \exists z \in (0 ..^\|H\|) i = H (z)$
208	207	anim1ci	$⊢ ((\forall i \in dom I \exists y \in (0 ..^\|F\|) i = F (y) \land φ) \land H : (0 ..^\|H\|) ⟶ dom I) \to (H : (0 ..^\|H\|) ⟶ dom I \land \forall i \in dom I \exists z \in (0 ..^\|H\|) i = H (z))$
209		dffo3	$⊢ H : (0 ..^\|H\|) \underset{onto}{⟶} dom I \leftrightarrow (H : (0 ..^\|H\|) ⟶ dom I \land \forall i \in dom I \exists z \in (0 ..^\|H\|) i = H (z))$
210	208 209	sylibr	$⊢ ((\forall i \in dom I \exists y \in (0 ..^\|F\|) i = F (y) \land φ) \land H : (0 ..^\|H\|) ⟶ dom I) \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I$
211	210	exp31	$⊢ \forall i \in dom I \exists y \in (0 ..^\|F\|) i = F (y) \to (φ \to (H : (0 ..^\|H\|) ⟶ dom I \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I))$
212	19 211	simplbiim	$⊢ F : (0 ..^\|F\|) \underset{onto}{⟶} dom I \to (φ \to (H : (0 ..^\|H\|) ⟶ dom I \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I))$
213	18 212	simplbiim	$⊢ F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \to (φ \to (H : (0 ..^\|H\|) ⟶ dom I \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I))$
214	213	com13	$⊢ H : (0 ..^\|H\|) ⟶ dom I \to (φ \to (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I))$
215	17 214	syl	$⊢ H Trails (G) Q \to (φ \to (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I))$
216	215	impcom	$⊢ (φ \land H Trails (G) Q) \to (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I)$
217	13 216	mpd	$⊢ (φ \land H Trails (G) Q) \to H : (0 ..^\|H\|) \underset{onto}{⟶} dom I$
218	10 217	jca	$⊢ (φ \land H Trails (G) Q) \to (H Trails (G) Q \land H : (0 ..^\|H\|) \underset{onto}{⟶} dom I)$
219	9 218	mpdan	$⊢ φ \to (H Trails (G) Q \land H : (0 ..^\|H\|) \underset{onto}{⟶} dom I)$
220	2	iseupth	$⊢ H EulerPaths (G) Q \leftrightarrow (H Trails (G) Q \land H : (0 ..^\|H\|) \underset{onto}{⟶} dom I)$
221	219 220	sylibr	$⊢ φ \to H EulerPaths (G) Q$
222	1 2 3 4 5 6 7	crctcsh	$⊢ φ \to H Circuits (G) Q$
223	221 222	jca	$⊢ φ \to (H EulerPaths (G) Q \land H Circuits (G) Q)$

Metamath Proof Explorer

Theorem eucrctshift

Proof