Metamath Proof Explorer

Theorem 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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
eucrctshift.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
eucrctshift.c ⊢ ( 𝜑 → 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
eucrctshift.n ⊢ 𝑁 = ( ♯ ‘ 𝐹 )
eucrctshift.s ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ 𝑁 ) )
eucrctshift.h ⊢ 𝐻 = ( 𝐹 cyclShift 𝑆 )
eucrctshift.q ⊢ 𝑄 = ( 𝑥 ∈ ( 0 ... 𝑁 ) ↦ if ( 𝑥 ≤ ( 𝑁 − 𝑆 ) , ( 𝑃 ‘ ( 𝑥 + 𝑆 ) ) , ( 𝑃 ‘ ( ( 𝑥 + 𝑆 ) − 𝑁 ) ) ) )
eucrctshift.e ⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
Assertion eucrctshift ( 𝜑 → ( 𝐻 ( EulerPaths ‘ 𝐺 ) 𝑄 ∧ 𝐻 ( Circuits ‘ 𝐺 ) 𝑄 ) )

Proof

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