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

Metamath Proof Explorer

Theorem eucrctshift

Proof