| Step | Hyp | Ref
| Expression |
| 1 | | eucrctshift.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
| 2 | | eucrctshift.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
| 3 | | eucrctshift.c |
. . . . 5
⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) |
| 4 | | eucrctshift.n |
. . . . 5
⊢ 𝑁 = (♯‘𝐹) |
| 5 | | eucrctshift.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) |
| 6 | | eucrctshift.h |
. . . . 5
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
| 7 | | eucrctshift.q |
. . . . 5
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | crctcshtrl 29843 |
. . . 4
⊢ (𝜑 → 𝐻(Trails‘𝐺)𝑄) |
| 9 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝐻(Trails‘𝐺)𝑄) → 𝐻(Trails‘𝐺)𝑄) |
| 10 | | eucrctshift.e |
. . . . . . . 8
⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) |
| 11 | 2 | eupthf1o 30223 |
. . . . . . . 8
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼) |
| 12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼) |
| 13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐻(Trails‘𝐺)𝑄) → 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼) |
| 14 | | trliswlk 29715 |
. . . . . . . 8
⊢ (𝐻(Trails‘𝐺)𝑄 → 𝐻(Walks‘𝐺)𝑄) |
| 15 | 2 | wlkf 29632 |
. . . . . . . 8
⊢ (𝐻(Walks‘𝐺)𝑄 → 𝐻 ∈ Word dom 𝐼) |
| 16 | | wrdf 14557 |
. . . . . . . 8
⊢ (𝐻 ∈ Word dom 𝐼 → 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) |
| 17 | | df-f1o 6568 |
. . . . . . . . . 10
⊢ (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼 ↔ (𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼)) |
| 18 | | dffo3 7122 |
. . . . . . . . . . 11
⊢ (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 ↔ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼∃𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹‘𝑦))) |
| 19 | | crctiswlk 29816 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
| 20 | 2 | wlkf 29632 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
| 21 | | lencl 14571 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹 ∈ Word dom 𝐼 → (♯‘𝐹) ∈
ℕ0) |
| 22 | 4 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(0..^𝑁) =
(0..^(♯‘𝐹)) |
| 23 | 22 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 ∈ (0..^𝑁) ↔ 𝑆 ∈ (0..^(♯‘𝐹))) |
| 24 | | elfzonn0 13747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
→ 𝑆 ∈
ℕ0) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈
ℕ0) |
| 26 | | elfzonn0 13747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ 𝑦 ∈
ℕ0) |
| 27 | | nn0sub 12576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑆 ∈ ℕ0
∧ 𝑦 ∈
ℕ0) → (𝑆 ≤ 𝑦 ↔ (𝑦 − 𝑆) ∈
ℕ0)) |
| 28 | 25, 26, 27 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆 ≤ 𝑦 ↔ (𝑦 − 𝑆) ∈
ℕ0)) |
| 29 | 28 | biimpac 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (𝑦 − 𝑆) ∈
ℕ0) |
| 30 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
↔ (𝑦 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹))) |
| 31 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
(♯‘𝐹) ∈
ℕ) |
| 32 | 30, 31 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ (♯‘𝐹)
∈ ℕ) |
| 33 | 32 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (♯‘𝐹)
∈ ℕ) |
| 34 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℝ) |
| 35 | 34 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℝ) |
| 36 | | nnre 12273 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
((♯‘𝐹)
∈ ℕ → (♯‘𝐹) ∈ ℝ) |
| 37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (♯‘𝐹) ∈ ℝ) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℝ) |
| 39 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
→ 𝑆 ∈
ℤ) |
| 40 | 39 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
→ 𝑆 ∈
ℝ) |
| 41 | | readdcl 11238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((♯‘𝐹)
∈ ℝ ∧ 𝑆
∈ ℝ) → ((♯‘𝐹) + 𝑆) ∈ ℝ) |
| 42 | 37, 40, 41 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → ((♯‘𝐹) + 𝑆) ∈ ℝ) |
| 43 | 35, 38, 42 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ ∧
((♯‘𝐹) + 𝑆) ∈
ℝ)) |
| 44 | | elfzole1 13707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
→ 0 ≤ 𝑆) |
| 45 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → 0 ≤ 𝑆) |
| 46 | | addge01 11773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
(((♯‘𝐹)
∈ ℝ ∧ 𝑆
∈ ℝ) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆))) |
| 47 | 37, 40, 46 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → (0 ≤ 𝑆 ↔ (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆))) |
| 48 | 45, 47 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ≤ ((♯‘𝐹) + 𝑆)) |
| 49 | 43, 48 | lelttrdi 11423 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) ∧ 𝑆
∈ (0..^(♯‘𝐹))) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆))) |
| 50 | 49 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (𝑆
∈ (0..^(♯‘𝐹)) → (𝑦 < (♯‘𝐹) → 𝑦 < ((♯‘𝐹) + 𝑆)))) |
| 51 | 50 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (𝑦
< (♯‘𝐹)
→ (𝑆 ∈
(0..^(♯‘𝐹))
→ 𝑦 <
((♯‘𝐹) + 𝑆)))) |
| 52 | 51 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
(𝑆 ∈
(0..^(♯‘𝐹))
→ 𝑦 <
((♯‘𝐹) + 𝑆))) |
| 53 | 52 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
(((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹))) → 𝑦 < ((♯‘𝐹) + 𝑆))) |
| 54 | 53 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) ∧
((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹)))) → 𝑦 < ((♯‘𝐹) + 𝑆)) |
| 55 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
𝑦 ∈
ℝ) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) ∧
((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹)))) → 𝑦 ∈ ℝ) |
| 57 | 40 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) ∧
((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹)))) → 𝑆 ∈ ℝ) |
| 58 | | elfzoel2 13698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
→ (♯‘𝐹)
∈ ℤ) |
| 59 | 58 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
→ (♯‘𝐹)
∈ ℝ) |
| 60 | 59 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) ∧
((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹)))) → (♯‘𝐹) ∈ ℝ) |
| 61 | 56, 57, 60 | ltsubaddd 11859 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) ∧
((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹)))) → ((𝑦 − 𝑆) < (♯‘𝐹) ↔ 𝑦 < ((♯‘𝐹) + 𝑆))) |
| 62 | 54, 61 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) ∧
((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹)))) → (𝑦 − 𝑆) < (♯‘𝐹)) |
| 63 | 62 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
(((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹))) → (𝑦 − 𝑆) < (♯‘𝐹))) |
| 64 | 30, 63 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ (((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (𝑦 − 𝑆) < (♯‘𝐹))) |
| 65 | 64 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦 − 𝑆) < (♯‘𝐹)) |
| 66 | 65 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (𝑦 − 𝑆) < (♯‘𝐹)) |
| 67 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑦 − 𝑆) ∈ (0..^(♯‘𝐹)) ↔ ((𝑦 − 𝑆) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ (𝑦 −
𝑆) <
(♯‘𝐹))) |
| 68 | 29, 33, 66, 67 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (𝑦 − 𝑆) ∈
(0..^(♯‘𝐹))) |
| 69 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 = (𝑦 − 𝑆) → (𝑧 + 𝑆) = ((𝑦 − 𝑆) + 𝑆)) |
| 70 | 69 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 = (𝑦 − 𝑆) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = (((𝑦 − 𝑆) + 𝑆) mod (♯‘𝐹))) |
| 71 | 39 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
→ 𝑆 ∈
ℂ) |
| 72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ) |
| 73 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ 𝑦 ∈
ℤ) |
| 74 | 73 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ 𝑦 ∈
ℂ) |
| 75 | 72, 74 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ)) |
| 76 | 75 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (𝑦 ∈ ℂ
∧ 𝑆 ∈
ℂ)) |
| 77 | | npcan 11517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → ((𝑦 − 𝑆) + 𝑆) = 𝑦) |
| 78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ ((𝑦 − 𝑆) + 𝑆) = 𝑦) |
| 79 | 78 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (((𝑦 − 𝑆) + 𝑆) mod (♯‘𝐹)) = (𝑦 mod (♯‘𝐹))) |
| 80 | | zmodidfzoimp 13941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ (𝑦 mod
(♯‘𝐹)) = 𝑦) |
| 81 | 80 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (𝑦 mod
(♯‘𝐹)) = 𝑦) |
| 82 | 79, 81 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (((𝑦 − 𝑆) + 𝑆) mod (♯‘𝐹)) = 𝑦) |
| 83 | 70, 82 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
∧ 𝑧 = (𝑦 − 𝑆)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦) |
| 84 | 83 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
∧ 𝑧 = (𝑦 − 𝑆)) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 85 | 68, 84 | rspcedeq2vd 3630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ ∃𝑧 ∈
(0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 86 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑆 ∈
(0..^(♯‘𝐹))
↔ (𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) |
| 87 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℂ) |
| 88 | 87 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℂ) |
| 89 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℂ) |
| 90 | 89 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑆 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑆 <
(♯‘𝐹)) →
𝑆 ∈
ℂ) |
| 91 | 90 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑆 ∈ ℂ) |
| 92 | | nncn 12274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
((♯‘𝐹)
∈ ℕ → (♯‘𝐹) ∈ ℂ) |
| 93 | 92 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑆 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑆 <
(♯‘𝐹)) →
(♯‘𝐹) ∈
ℂ) |
| 94 | 93 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℂ) |
| 95 | 88, 91, 94 | subadd23d 11642 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦 − 𝑆) + (♯‘𝐹)) = (𝑦 + ((♯‘𝐹) − 𝑆))) |
| 96 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → 𝑦 ∈ ℕ0) |
| 97 | | nn0z 12638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℤ) |
| 98 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢
((♯‘𝐹)
∈ ℕ → (♯‘𝐹) ∈ ℤ) |
| 99 | | znnsub 12663 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑆 ∈ ℤ ∧
(♯‘𝐹) ∈
ℤ) → (𝑆 <
(♯‘𝐹) ↔
((♯‘𝐹) −
𝑆) ∈
ℕ)) |
| 100 | 97, 98, 99 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑆 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ) → (𝑆
< (♯‘𝐹)
↔ ((♯‘𝐹)
− 𝑆) ∈
ℕ)) |
| 101 | 100 | biimp3a 1471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑆 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑆 <
(♯‘𝐹)) →
((♯‘𝐹) −
𝑆) ∈
ℕ) |
| 102 | 101 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈ ℕ) |
| 103 | 102 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) − 𝑆) ∈
ℕ0) |
| 104 | 96, 103 | nn0addcld 12591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦 + ((♯‘𝐹) − 𝑆)) ∈
ℕ0) |
| 105 | 95, 104 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦 − 𝑆) + (♯‘𝐹)) ∈
ℕ0) |
| 106 | 105 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) + (♯‘𝐹)) ∈
ℕ0) |
| 107 | | simplr2 1217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → (♯‘𝐹) ∈ ℕ) |
| 108 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) →
𝑦 ∈
ℂ) |
| 109 | | subcl 11507 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑦 ∈ ℂ ∧ 𝑆 ∈ ℂ) → (𝑦 − 𝑆) ∈ ℂ) |
| 110 | 108, 90, 109 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦 − 𝑆) ∈ ℂ) |
| 111 | 94, 110 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦 − 𝑆) ∈ ℂ)) |
| 112 | 111 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((♯‘𝐹) ∈ ℂ ∧ (𝑦 − 𝑆) ∈ ℂ)) |
| 113 | | addcom 11447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((♯‘𝐹)
∈ ℂ ∧ (𝑦
− 𝑆) ∈ ℂ)
→ ((♯‘𝐹) +
(𝑦 − 𝑆)) = ((𝑦 − 𝑆) + (♯‘𝐹))) |
| 114 | 112, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((♯‘𝐹) + (𝑦 − 𝑆)) = ((𝑦 − 𝑆) + (♯‘𝐹))) |
| 115 | 34 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) →
𝑦 ∈
ℝ) |
| 116 | | nn0re 12535 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℝ) |
| 117 | 116 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑆 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑆 <
(♯‘𝐹)) →
𝑆 ∈
ℝ) |
| 118 | | ltnle 11340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 ↔ ¬ 𝑆 ≤ 𝑦)) |
| 119 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑦 ∈
ℝ) |
| 120 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → 𝑆 ∈
ℝ) |
| 121 | 119, 120 | sublt0d 11889 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → ((𝑦 − 𝑆) < 0 ↔ 𝑦 < 𝑆)) |
| 122 | 121 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 < 𝑆 → (𝑦 − 𝑆) < 0)) |
| 123 | 118, 122 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (¬
𝑆 ≤ 𝑦 → (𝑦 − 𝑆) < 0)) |
| 124 | 115, 117,
123 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (¬ 𝑆 ≤ 𝑦 → (𝑦 − 𝑆) < 0)) |
| 125 | 124 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → (𝑦 − 𝑆) < 0) |
| 126 | | resubcl 11573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑦 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑦 − 𝑆) ∈ ℝ) |
| 127 | 115, 117,
126 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (𝑦 − 𝑆) ∈ ℝ) |
| 128 | 36 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑆 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑆 <
(♯‘𝐹)) →
(♯‘𝐹) ∈
ℝ) |
| 129 | 128 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → (♯‘𝐹) ∈ ℝ) |
| 130 | 127, 129 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) → ((𝑦 − 𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈
ℝ)) |
| 131 | 130 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈
ℝ)) |
| 132 | | ltaddneg 11477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑦 − 𝑆) ∈ ℝ ∧ (♯‘𝐹) ∈ ℝ) → ((𝑦 − 𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦 − 𝑆)) < (♯‘𝐹))) |
| 133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) < 0 ↔ ((♯‘𝐹) + (𝑦 − 𝑆)) < (♯‘𝐹))) |
| 134 | 125, 133 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((♯‘𝐹) + (𝑦 − 𝑆)) < (♯‘𝐹)) |
| 135 | 114, 134 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → ((𝑦 − 𝑆) + (♯‘𝐹)) < (♯‘𝐹)) |
| 136 | 106, 107,
135 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) ∧
(𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹))) ∧ ¬ 𝑆 ≤ 𝑦) → (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹))) |
| 137 | 136 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑦 ∈ ℕ0
∧ 𝑦 <
(♯‘𝐹)) →
((𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹))))) |
| 138 | 137 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
((𝑆 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑆 < (♯‘𝐹)) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹))))) |
| 139 | 86, 138 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
(𝑆 ∈
(0..^(♯‘𝐹))
→ (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹))))) |
| 140 | 139 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
(((♯‘𝐹) ∈
ℕ0 ∧ 𝑆
∈ (0..^(♯‘𝐹))) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹))))) |
| 141 | 30, 140 | sylbi 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ (((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹))))) |
| 142 | 141 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (¬ 𝑆 ≤ 𝑦 → (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹)))) |
| 143 | 142 | impcom 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ ((𝑦
− 𝑆) +
(♯‘𝐹)) <
(♯‘𝐹))) |
| 144 | | elfzo0 13740 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ (0..^(♯‘𝐹)) ↔ (((𝑦 − 𝑆) + (♯‘𝐹)) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ ∧ ((𝑦 −
𝑆) + (♯‘𝐹)) < (♯‘𝐹))) |
| 145 | 143, 144 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ ((𝑦 − 𝑆) + (♯‘𝐹)) ∈
(0..^(♯‘𝐹))) |
| 146 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 = ((𝑦 − 𝑆) + (♯‘𝐹)) → (𝑧 + 𝑆) = (((𝑦 − 𝑆) + (♯‘𝐹)) + 𝑆)) |
| 147 | 146 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 = ((𝑦 − 𝑆) + (♯‘𝐹)) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = ((((𝑦 − 𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹))) |
| 148 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑆 ∈ ℂ) |
| 149 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → 𝑦 ∈ ℂ) |
| 150 | | nn0cn 12536 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((♯‘𝐹)
∈ ℕ0 → (♯‘𝐹) ∈ ℂ) |
| 151 | 150 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (♯‘𝐹) ∈ ℂ) |
| 152 | 148, 149,
151 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → (𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (♯‘𝐹) ∈
ℂ)) |
| 153 | 152 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (𝑆 ∈ ℂ
∧ 𝑦 ∈ ℂ
∧ (♯‘𝐹)
∈ ℂ)) |
| 154 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(♯‘𝐹) ∈
ℂ) → 𝑦 ∈
ℂ) |
| 155 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(♯‘𝐹) ∈
ℂ) → (♯‘𝐹) ∈ ℂ) |
| 156 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(♯‘𝐹) ∈
ℂ) → 𝑆 ∈
ℂ) |
| 157 | 154, 156,
155 | nppcand 11645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(♯‘𝐹) ∈
ℂ) → (((𝑦
− 𝑆) +
(♯‘𝐹)) + 𝑆) = (𝑦 + (♯‘𝐹))) |
| 158 | 154, 155,
157 | comraddd 11475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑆 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧
(♯‘𝐹) ∈
ℂ) → (((𝑦
− 𝑆) +
(♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦)) |
| 159 | 153, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (((𝑦 − 𝑆) + (♯‘𝐹)) + 𝑆) = ((♯‘𝐹) + 𝑦)) |
| 160 | 159 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ ((((𝑦 − 𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = (((♯‘𝐹) + 𝑦) mod (♯‘𝐹))) |
| 161 | 30 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈
(0..^(♯‘𝐹))
→ (𝑦 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹))) |
| 162 | 161 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (𝑦 ∈
ℕ0 ∧ (♯‘𝐹) ∈ ℕ ∧ 𝑦 < (♯‘𝐹))) |
| 163 | | addmodid 13960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑦 ∈ ℕ0
∧ (♯‘𝐹)
∈ ℕ ∧ 𝑦 <
(♯‘𝐹)) →
(((♯‘𝐹) + 𝑦) mod (♯‘𝐹)) = 𝑦) |
| 164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ (((♯‘𝐹)
+ 𝑦) mod
(♯‘𝐹)) = 𝑦) |
| 165 | 160, 164 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ ((((𝑦 − 𝑆) + (♯‘𝐹)) + 𝑆) mod (♯‘𝐹)) = 𝑦) |
| 166 | 147, 165 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
∧ 𝑧 = ((𝑦 − 𝑆) + (♯‘𝐹))) → ((𝑧 + 𝑆) mod (♯‘𝐹)) = 𝑦) |
| 167 | 166 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
∧ 𝑧 = ((𝑦 − 𝑆) + (♯‘𝐹))) → 𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 168 | 145, 167 | rspcedeq2vd 3630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((¬
𝑆 ≤ 𝑦 ∧ (((♯‘𝐹) ∈ ℕ0 ∧ 𝑆 ∈
(0..^(♯‘𝐹)))
∧ 𝑦 ∈
(0..^(♯‘𝐹))))
→ ∃𝑧 ∈
(0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 169 | 85, 168 | pm2.61ian 812 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 170 | 22 | rexeqi 3325 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∃𝑧 ∈
(0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) ↔ ∃𝑧 ∈ (0..^(♯‘𝐹))𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 171 | 169, 170 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((♯‘𝐹)
∈ ℕ0 ∧ 𝑆 ∈ (0..^(♯‘𝐹))) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 172 | 171 | exp31 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((♯‘𝐹)
∈ ℕ0 → (𝑆 ∈ (0..^(♯‘𝐹)) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))) |
| 173 | 23, 172 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((♯‘𝐹)
∈ ℕ0 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))) |
| 174 | 19, 20, 21, 173 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝑆 ∈ (0..^𝑁) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))))) |
| 175 | 3, 5, 174 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))) |
| 176 | 175 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (𝑦 ∈ (0..^(♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)))) |
| 177 | 176 | imp 406 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 178 | 177 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹))) |
| 179 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → (𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))) |
| 180 | 179 | reximi 3084 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑧 ∈
(0..^𝑁)𝑦 = ((𝑧 + 𝑆) mod (♯‘𝐹)) → ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))) |
| 181 | 178, 180 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))) |
| 182 | 3, 19, 20 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
| 183 | 182 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → 𝐹 ∈ Word dom 𝐼) |
| 184 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ) |
| 185 | 5, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑆 ∈ ℤ) |
| 186 | 185 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → 𝑆 ∈ ℤ) |
| 187 | 22 | eleq2i 2833 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (0..^𝑁) ↔ 𝑧 ∈ (0..^(♯‘𝐹))) |
| 188 | 187 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ (0..^(♯‘𝐹))) |
| 189 | | cshwidxmod 14841 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑆 ∈ ℤ ∧ 𝑧 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))) |
| 190 | 183, 186,
188, 189 | syl2an3an 1424 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹 cyclShift 𝑆)‘𝑧) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹)))) |
| 191 | 190 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) ∧ 𝑧 ∈ (0..^𝑁)) → ((𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ (𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))) |
| 192 | 191 | rexbidva 3177 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = (𝐹‘((𝑧 + 𝑆) mod (♯‘𝐹))))) |
| 193 | 181, 192 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧)) |
| 194 | 1, 2, 3, 4, 5, 6 | crctcshlem2 29838 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘𝐻) = 𝑁) |
| 195 | 194 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁)) |
| 196 | 195 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (0..^(♯‘𝐻)) = (0..^𝑁)) |
| 197 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → 𝑖 = (𝐹‘𝑦)) |
| 198 | 6 | fveq1i 6907 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐻‘𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧) |
| 199 | 198 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (𝐻‘𝑧) = ((𝐹 cyclShift 𝑆)‘𝑧)) |
| 200 | 197, 199 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (𝑖 = (𝐻‘𝑧) ↔ (𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧))) |
| 201 | 196, 200 | rexeqbidv 3347 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → (∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻‘𝑧) ↔ ∃𝑧 ∈ (0..^𝑁)(𝐹‘𝑦) = ((𝐹 cyclShift 𝑆)‘𝑧))) |
| 202 | 193, 201 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ dom 𝐼) ∧ 𝑦 ∈ (0..^(♯‘𝐹))) ∧ 𝑖 = (𝐹‘𝑦)) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻‘𝑧)) |
| 203 | 202 | rexlimdva2 3157 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ dom 𝐼) → (∃𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹‘𝑦) → ∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻‘𝑧))) |
| 204 | 203 | ralimdva 3167 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∀𝑖 ∈ dom 𝐼∃𝑦 ∈ (0..^(♯‘𝐹))𝑖 = (𝐹‘𝑦) → ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻‘𝑧))) |
| 205 | 204 | impcom 407 |
. . . . . . . . . . . . . 14
⊢
((∀𝑖 ∈
dom 𝐼∃𝑦 ∈
(0..^(♯‘𝐹))𝑖 = (𝐹‘𝑦) ∧ 𝜑) → ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻‘𝑧)) |
| 206 | 205 | anim1ci 616 |
. . . . . . . . . . . . 13
⊢
(((∀𝑖 ∈
dom 𝐼∃𝑦 ∈
(0..^(♯‘𝐹))𝑖 = (𝐹‘𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻‘𝑧))) |
| 207 | | dffo3 7122 |
. . . . . . . . . . . . 13
⊢ (𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼 ↔ (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 ∧ ∀𝑖 ∈ dom 𝐼∃𝑧 ∈ (0..^(♯‘𝐻))𝑖 = (𝐻‘𝑧))) |
| 208 | 206, 207 | sylibr 234 |
. . . . . . . . . . . 12
⊢
(((∀𝑖 ∈
dom 𝐼∃𝑦 ∈
(0..^(♯‘𝐹))𝑖 = (𝐹‘𝑦) ∧ 𝜑) ∧ 𝐻:(0..^(♯‘𝐻))⟶dom 𝐼) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼) |
| 209 | 208 | exp31 419 |
. . . . . . . . . . 11
⊢
(∀𝑖 ∈
dom 𝐼∃𝑦 ∈
(0..^(♯‘𝐹))𝑖 = (𝐹‘𝑦) → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))) |
| 210 | 18, 209 | simplbiim 504 |
. . . . . . . . . 10
⊢ (𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))) |
| 211 | 17, 210 | simplbiim 504 |
. . . . . . . . 9
⊢ (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼 → (𝜑 → (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))) |
| 212 | 211 | com13 88 |
. . . . . . . 8
⊢ (𝐻:(0..^(♯‘𝐻))⟶dom 𝐼 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼 → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))) |
| 213 | 14, 15, 16, 212 | 4syl 19 |
. . . . . . 7
⊢ (𝐻(Trails‘𝐺)𝑄 → (𝜑 → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼 → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼))) |
| 214 | 213 | impcom 407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐻(Trails‘𝐺)𝑄) → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom
𝐼 → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)) |
| 215 | 13, 214 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝐻(Trails‘𝐺)𝑄) → 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼) |
| 216 | 9, 215 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝐻(Trails‘𝐺)𝑄) → (𝐻(Trails‘𝐺)𝑄 ∧ 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)) |
| 217 | 8, 216 | mpdan 687 |
. . 3
⊢ (𝜑 → (𝐻(Trails‘𝐺)𝑄 ∧ 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)) |
| 218 | 2 | iseupth 30220 |
. . 3
⊢ (𝐻(EulerPaths‘𝐺)𝑄 ↔ (𝐻(Trails‘𝐺)𝑄 ∧ 𝐻:(0..^(♯‘𝐻))–onto→dom 𝐼)) |
| 219 | 217, 218 | sylibr 234 |
. 2
⊢ (𝜑 → 𝐻(EulerPaths‘𝐺)𝑄) |
| 220 | 1, 2, 3, 4, 5, 6, 7 | crctcsh 29844 |
. 2
⊢ (𝜑 → 𝐻(Circuits‘𝐺)𝑄) |
| 221 | 219, 220 | jca 511 |
1
⊢ (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄 ∧ 𝐻(Circuits‘𝐺)𝑄)) |