Proof of Theorem crctcsh
Step | Hyp | Ref
| Expression |
1 | | crctcsh.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | crctcsh.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝐺) |
3 | | crctcsh.d |
. . . 4
⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) |
4 | | crctcsh.n |
. . . 4
⊢ 𝑁 = (#‘𝐹) |
5 | | crctcsh.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) |
6 | | crctcsh.h |
. . . 4
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
7 | | crctcsh.q |
. . . 4
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
8 | 1, 2, 3, 4, 5, 6, 7 | crctcshlem4 41023 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → (𝐻 = 𝐹 ∧ 𝑄 = 𝑃)) |
9 | | breq12 4588 |
. . . . 5
⊢ ((𝐻 = 𝐹 ∧ 𝑄 = 𝑃) → (𝐻(CircuitS‘𝐺)𝑄 ↔ 𝐹(CircuitS‘𝐺)𝑃)) |
10 | 3, 9 | syl5ibrcom 236 |
. . . 4
⊢ (𝜑 → ((𝐻 = 𝐹 ∧ 𝑄 = 𝑃) → 𝐻(CircuitS‘𝐺)𝑄)) |
11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑆 = 0) → ((𝐻 = 𝐹 ∧ 𝑄 = 𝑃) → 𝐻(CircuitS‘𝐺)𝑄)) |
12 | 8, 11 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑆 = 0) → 𝐻(CircuitS‘𝐺)𝑄) |
13 | 1, 2, 3, 4, 5, 6, 7 | crctcshtrl 41026 |
. . . . 5
⊢ (𝜑 → 𝐻(TrailS‘𝐺)𝑄) |
14 | 13 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(TrailS‘𝐺)𝑄) |
15 | 7 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))) |
16 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑥 ≤ (𝑁 − 𝑆) ↔ 0 ≤ (𝑁 − 𝑆))) |
17 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝑥 + 𝑆) = (0 + 𝑆)) |
18 | 17 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑃‘(𝑥 + 𝑆)) = (𝑃‘(0 + 𝑆))) |
19 | 17 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((𝑥 + 𝑆) − 𝑁) = ((0 + 𝑆) − 𝑁)) |
20 | 19 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝑃‘((𝑥 + 𝑆) − 𝑁)) = (𝑃‘((0 + 𝑆) − 𝑁))) |
21 | 16, 18, 20 | ifbieq12d 4063 |
. . . . . . 7
⊢ (𝑥 = 0 → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) = if(0 ≤ (𝑁 − 𝑆), (𝑃‘(0 + 𝑆)), (𝑃‘((0 + 𝑆) − 𝑁)))) |
22 | | elfzo0le 12379 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ≤ 𝑁) |
23 | 5, 22 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ≤ 𝑁) |
24 | 1, 2, 3, 4 | crctcshlem1 41020 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
25 | 24 | nn0red 11229 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℝ) |
26 | | elfzoelz 12339 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ) |
27 | 5, 26 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℤ) |
28 | 27 | zred 11358 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ℝ) |
29 | 25, 28 | subge0d 10496 |
. . . . . . . . . 10
⊢ (𝜑 → (0 ≤ (𝑁 − 𝑆) ↔ 𝑆 ≤ 𝑁)) |
30 | 23, 29 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑁 − 𝑆)) |
31 | 30 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 0 ≤ (𝑁 − 𝑆)) |
32 | 31 | iftrued 4044 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → if(0 ≤ (𝑁 − 𝑆), (𝑃‘(0 + 𝑆)), (𝑃‘((0 + 𝑆) − 𝑁))) = (𝑃‘(0 + 𝑆))) |
33 | 21, 32 | sylan9eqr 2666 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ≠ 0) ∧ 𝑥 = 0) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) = (𝑃‘(0 + 𝑆))) |
34 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐹(CircuitS‘𝐺)𝑃) |
35 | 1, 2, 34, 4 | crctcshlem1 41020 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑁 ∈
ℕ0) |
36 | | 0elfz 12305 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ (0...𝑁)) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 0 ∈ (0...𝑁)) |
38 | | fvex 6113 |
. . . . . . 7
⊢ (𝑃‘(0 + 𝑆)) ∈ V |
39 | 38 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝑃‘(0 + 𝑆)) ∈ V) |
40 | 15, 33, 37, 39 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝑄‘0) = (𝑃‘(0 + 𝑆))) |
41 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑥 = (#‘𝐻) → (𝑥 ≤ (𝑁 − 𝑆) ↔ (#‘𝐻) ≤ (𝑁 − 𝑆))) |
42 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = (#‘𝐻) → (𝑥 + 𝑆) = ((#‘𝐻) + 𝑆)) |
43 | 42 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑥 = (#‘𝐻) → (𝑃‘(𝑥 + 𝑆)) = (𝑃‘((#‘𝐻) + 𝑆))) |
44 | 42 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑥 = (#‘𝐻) → ((𝑥 + 𝑆) − 𝑁) = (((#‘𝐻) + 𝑆) − 𝑁)) |
45 | 44 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑥 = (#‘𝐻) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) = (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁))) |
46 | 41, 43, 45 | ifbieq12d 4063 |
. . . . . . . 8
⊢ (𝑥 = (#‘𝐻) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) = if((#‘𝐻) ≤ (𝑁 − 𝑆), (𝑃‘((#‘𝐻) + 𝑆)), (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁)))) |
47 | | elfzoel2 12338 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ) |
48 | | elfzonn0 12380 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈
ℕ0) |
49 | | simpr 476 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
→ 𝑆 ∈
ℕ0) |
50 | 49 | anim1i 590 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
∧ 𝑆 ≠ 0) →
(𝑆 ∈
ℕ0 ∧ 𝑆
≠ 0)) |
51 | | elnnne0 11183 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ ℕ ↔ (𝑆 ∈ ℕ0
∧ 𝑆 ≠
0)) |
52 | 50, 51 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
∧ 𝑆 ≠ 0) →
𝑆 ∈
ℕ) |
53 | 52 | nngt0d 10941 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
∧ 𝑆 ≠ 0) → 0
< 𝑆) |
54 | | zre 11258 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
55 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℝ) |
56 | 54, 55 | anim12ci 589 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
→ (𝑆 ∈ ℝ
∧ 𝑁 ∈
ℝ)) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
∧ 𝑆 ≠ 0) →
(𝑆 ∈ ℝ ∧
𝑁 ∈
ℝ)) |
58 | | ltsubpos 10399 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (0 <
𝑆 ↔ (𝑁 − 𝑆) < 𝑁)) |
59 | 58 | bicomd 212 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑁 ↔ 0 < 𝑆)) |
60 | 57, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
∧ 𝑆 ≠ 0) →
((𝑁 − 𝑆) < 𝑁 ↔ 0 < 𝑆)) |
61 | 53, 60 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
∧ 𝑆 ≠ 0) →
(𝑁 − 𝑆) < 𝑁) |
62 | 61 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℕ0)
→ (𝑆 ≠ 0 →
(𝑁 − 𝑆) < 𝑁)) |
63 | 47, 48, 62 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (0..^𝑁) → (𝑆 ≠ 0 → (𝑁 − 𝑆) < 𝑁)) |
64 | 5, 63 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑆 ≠ 0 → (𝑁 − 𝑆) < 𝑁)) |
65 | 64 | imp 444 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝑁 − 𝑆) < 𝑁) |
66 | 5 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ (0..^𝑁)) |
67 | 1, 2, 34, 4, 66, 6 | crctcshlem2 41021 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (#‘𝐻) = 𝑁) |
68 | 67 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ((#‘𝐻) ≤ (𝑁 − 𝑆) ↔ 𝑁 ≤ (𝑁 − 𝑆))) |
69 | 68 | notbid 307 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (¬ (#‘𝐻) ≤ (𝑁 − 𝑆) ↔ ¬ 𝑁 ≤ (𝑁 − 𝑆))) |
70 | 25, 28 | resubcld 10337 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑁 − 𝑆) ∈ ℝ) |
71 | 70, 25 | jca 553 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑁 − 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
72 | 71 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ((𝑁 − 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
73 | | ltnle 9996 |
. . . . . . . . . . . 12
⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 𝑆))) |
74 | 72, 73 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ((𝑁 − 𝑆) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 𝑆))) |
75 | 69, 74 | bitr4d 270 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (¬ (#‘𝐻) ≤ (𝑁 − 𝑆) ↔ (𝑁 − 𝑆) < 𝑁)) |
76 | 65, 75 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ¬ (#‘𝐻) ≤ (𝑁 − 𝑆)) |
77 | 76 | iffalsed 4047 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → if((#‘𝐻) ≤ (𝑁 − 𝑆), (𝑃‘((#‘𝐻) + 𝑆)), (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁))) = (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁))) |
78 | 46, 77 | sylan9eqr 2666 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ≠ 0) ∧ 𝑥 = (#‘𝐻)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) = (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁))) |
79 | 1, 2, 3, 4, 5, 6 | crctcshlem2 41021 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (#‘𝐻) = 𝑁) |
80 | 79, 24 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (#‘𝐻) ∈
ℕ0) |
81 | 80 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (𝜑 → (#‘𝐻) ∈ ℂ) |
82 | 27 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ ℂ) |
83 | 24 | nn0cnd 11230 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
84 | 81, 82, 83 | addsubd 10292 |
. . . . . . . . . . 11
⊢ (𝜑 → (((#‘𝐻) + 𝑆) − 𝑁) = (((#‘𝐻) − 𝑁) + 𝑆)) |
85 | 79 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((#‘𝐻) − 𝑁) = (𝑁 − 𝑁)) |
86 | 83 | subidd 10259 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 𝑁) = 0) |
87 | 85, 86 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝐻) − 𝑁) = 0) |
88 | 87 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → (((#‘𝐻) − 𝑁) + 𝑆) = (0 + 𝑆)) |
89 | 84, 88 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (((#‘𝐻) + 𝑆) − 𝑁) = (0 + 𝑆)) |
90 | 89 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁)) = (𝑃‘(0 + 𝑆))) |
91 | 90 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁)) = (𝑃‘(0 + 𝑆))) |
92 | 91 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑆 ≠ 0) ∧ 𝑥 = (#‘𝐻)) → (𝑃‘(((#‘𝐻) + 𝑆) − 𝑁)) = (𝑃‘(0 + 𝑆))) |
93 | 78, 92 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑆 ≠ 0) ∧ 𝑥 = (#‘𝐻)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) = (𝑃‘(0 + 𝑆))) |
94 | 79 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (#‘𝐻) = 𝑁) |
95 | | nn0fz0 12306 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
↔ 𝑁 ∈ (0...𝑁)) |
96 | 24, 95 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
97 | 96 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑁 ∈ (0...𝑁)) |
98 | 94, 97 | eqeltrd 2688 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (#‘𝐻) ∈ (0...𝑁)) |
99 | 15, 93, 98, 39 | fvmptd 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝑄‘(#‘𝐻)) = (𝑃‘(0 + 𝑆))) |
100 | 40, 99 | eqtr4d 2647 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝑄‘0) = (𝑄‘(#‘𝐻))) |
101 | 14, 100 | jca 553 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻(TrailS‘𝐺)𝑄 ∧ (𝑄‘0) = (𝑄‘(#‘𝐻)))) |
102 | 1, 2, 3, 4, 5, 6, 7 | crctcshlem3 41022 |
. . . . 5
⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
103 | 102 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
104 | | isCrct 40996 |
. . . 4
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(CircuitS‘𝐺)𝑄 ↔ (𝐻(TrailS‘𝐺)𝑄 ∧ (𝑄‘0) = (𝑄‘(#‘𝐻))))) |
105 | 103, 104 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻(CircuitS‘𝐺)𝑄 ↔ (𝐻(TrailS‘𝐺)𝑄 ∧ (𝑄‘0) = (𝑄‘(#‘𝐻))))) |
106 | 101, 105 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(CircuitS‘𝐺)𝑄) |
107 | 12, 106 | pm2.61dane 2869 |
1
⊢ (𝜑 → 𝐻(CircuitS‘𝐺)𝑄) |