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 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 biimtrid ⊢ ( ( 𝑦 ∈ ℕ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 biimtrid ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ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 ‘ 𝐺 ) 𝑄 ) )