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