Step | Hyp | Ref
| Expression |
1 | | crctcsh.h |
. . . . 5
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
2 | | crctcsh.d |
. . . . . . 7
⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃) |
3 | | crctiswlk 27737 |
. . . . . . 7
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
4 | | crctcsh.i |
. . . . . . . 8
⊢ 𝐼 = (iEdg‘𝐺) |
5 | 4 | wlkf 27556 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) |
6 | 2, 3, 5 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) |
7 | | cshwcl 14249 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐼 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹 cyclShift 𝑆) ∈ Word dom 𝐼) |
9 | 1, 8 | eqeltrid 2837 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ Word dom 𝐼) |
10 | 9 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻 ∈ Word dom 𝐼) |
11 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) |
12 | | crctcsh.v |
. . . . . . . . . 10
⊢ 𝑉 = (Vtx‘𝐺) |
13 | 12 | wlkp 27558 |
. . . . . . . . 9
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
14 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
15 | | crctcsh.s |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) |
16 | | elfznn0 13091 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℕ0) |
17 | 16 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℕ0) |
18 | | elfzonn0 13173 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈
ℕ0) |
19 | 18 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈
ℕ0) |
20 | 17, 19 | nn0addcld 12040 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ∈
ℕ0) |
21 | 20 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈
ℕ0) |
22 | | crctcsh.n |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 = (♯‘𝐹) |
23 | | elfz3nn0 13092 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈
ℕ0) |
24 | 22, 23 | eqeltrrid 2838 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0...𝑁) → (♯‘𝐹) ∈
ℕ0) |
25 | 24 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈
ℕ0) |
26 | | elfzelz 12998 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℤ) |
27 | 26 | zred 12168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0...𝑁) → 𝑥 ∈ ℝ) |
28 | 27 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑥 ∈ ℝ) |
29 | | elfzoelz 13129 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℤ) |
30 | 29 | zred 12168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑆 ∈ (0..^𝑁) → 𝑆 ∈ ℝ) |
31 | 30 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑆 ∈ ℝ) |
32 | | elfzel2 12996 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℤ) |
33 | 32 | zred 12168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (0...𝑁) → 𝑁 ∈ ℝ) |
34 | 33 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → 𝑁 ∈ ℝ) |
35 | | leaddsub 11194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆))) |
36 | 28, 31, 34, 35 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ≤ 𝑁 ↔ 𝑥 ≤ (𝑁 − 𝑆))) |
37 | 36 | biimpar 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ 𝑁) |
38 | 37, 22 | breqtrdi 5071 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ≤ (♯‘𝐹)) |
39 | 21, 25, 38 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ0 ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹))) |
40 | 15, 39 | sylanl1 680 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ0 ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹))) |
41 | | elfz2nn0 13089 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 + 𝑆) ∈ (0...(♯‘𝐹)) ↔ ((𝑥 + 𝑆) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ0 ∧ (𝑥 + 𝑆) ≤ (♯‘𝐹))) |
42 | 40, 41 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹))) |
43 | 42 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑥 + 𝑆) ∈ (0...(♯‘𝐹))) |
44 | 14, 43 | ffvelrnd 6862 |
. . . . . . . . . . 11
⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘(𝑥 + 𝑆)) ∈ 𝑉) |
45 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → 𝑃:(0...(♯‘𝐹))⟶𝑉) |
46 | | elfzoel2 13128 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℤ) |
47 | | zaddcl 12103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑥 + 𝑆) ∈ ℤ) |
48 | 47 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℤ) |
49 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℤ) |
50 | 48, 49 | zsubcld 12173 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ) |
51 | 50 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬
𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℤ) |
52 | | zsubcl 12105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑁 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ) |
53 | 52 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℤ) |
54 | 53 | zred 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 − 𝑆) ∈ ℝ) |
55 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) |
56 | | ltnle 10798 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆))) |
57 | 54, 55, 56 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ ¬ 𝑥 ≤ (𝑁 − 𝑆))) |
58 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
59 | 58 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
60 | | zre 12066 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑆 ∈ ℤ → 𝑆 ∈
ℝ) |
61 | 60 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑆 ∈
ℝ) |
62 | 55 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑥 ∈
ℝ) |
63 | | ltsubadd 11188 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑥 ∈ ℝ) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆))) |
64 | 59, 61, 62, 63 | syl2an23an 1424 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 ↔ 𝑁 < (𝑥 + 𝑆))) |
65 | 59 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈
ℝ) |
66 | 48 | zred 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑥 + 𝑆) ∈ ℝ) |
67 | 65, 66 | posdifd 11305 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) ↔ 0 < ((𝑥 + 𝑆) − 𝑁))) |
68 | | 0red 10722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 0
∈ ℝ) |
69 | 50 | zred 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) − 𝑁) ∈ ℝ) |
70 | | ltle 10807 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℝ ∧ ((𝑥 +
𝑆) − 𝑁) ∈ ℝ) → (0 <
((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
71 | 68, 69, 70 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (0 <
((𝑥 + 𝑆) − 𝑁) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
72 | 67, 71 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 < (𝑥 + 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
73 | 64, 72 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑁 − 𝑆) < 𝑥 → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
74 | 57, 73 | sylbird 263 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (¬
𝑥 ≤ (𝑁 − 𝑆) → 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
75 | 74 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬
𝑥 ≤ (𝑁 − 𝑆)) → 0 ≤ ((𝑥 + 𝑆) − 𝑁)) |
76 | 51, 75 | jca 515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) ∧ ¬
𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
77 | 76 | exp31 423 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬
𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))))) |
78 | 77, 26 | syl11 33 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))))) |
79 | 29, 46, 78 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → (¬ 𝑥 ≤ (𝑁 − 𝑆) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))))) |
80 | 79 | imp31 421 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
81 | | elnn0z 12075 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℤ ∧ 0 ≤ ((𝑥 + 𝑆) − 𝑁))) |
82 | 80, 81 | sylibr 237 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈
ℕ0) |
83 | 24 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (♯‘𝐹) ∈
ℕ0) |
84 | | elfzo0 13169 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) |
85 | | elfz2nn0 13089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (0...𝑁) ↔ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) |
86 | | nn0re 11985 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℝ) |
87 | 86 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ) |
88 | | nn0re 11985 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℕ0
→ 𝑥 ∈
ℝ) |
89 | 88 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑥
≤ 𝑁) → 𝑥 ∈
ℝ) |
90 | 87, 89 | anim12ci 617 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → (𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ)) |
91 | | nnre 11723 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
92 | 91, 91 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
93 | 92 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
94 | 93 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
95 | 90, 94 | jca 515 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → ((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
96 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → 𝑥 ≤ 𝑁) |
97 | | ltle 10807 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁)) |
98 | 86, 91, 97 | syl2an 599 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ)
→ (𝑆 < 𝑁 → 𝑆 ≤ 𝑁)) |
99 | 98 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁) |
100 | 99 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → 𝑆 ≤ 𝑁) |
101 | 95, 96, 100 | jca32 519 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 ∈ ℕ0
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁) ∧ (𝑥 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑥 ≤ 𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁))) |
102 | 84, 85, 101 | syl2anb 601 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁))) |
103 | | le2add 11200 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))) |
104 | 103 | imp 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) ∧ (𝑥 ≤ 𝑁 ∧ 𝑆 ≤ 𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)) |
105 | 102, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (𝑥 + 𝑆) ≤ (𝑁 + 𝑁)) |
106 | 66, 65, 65 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
107 | 106 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℤ → ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
108 | 107, 26 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
109 | 29, 46, 108 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ (0..^𝑁) → (𝑥 ∈ (0...𝑁) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
110 | 109 | imp 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
111 | | lesubadd 11190 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → (((𝑥 + 𝑆) − 𝑁) ≤ 𝑁 ↔ (𝑥 + 𝑆) ≤ (𝑁 + 𝑁))) |
113 | 105, 112 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁) |
114 | 113 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ 𝑁) |
115 | 114, 22 | breqtrdi 5071 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹)) |
116 | 82, 83, 115 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ (0..^𝑁) ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ0 ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))) |
117 | 15, 116 | sylanl1 680 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ0 ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))) |
118 | | elfz2nn0 13089 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹)) ↔ (((𝑥 + 𝑆) − 𝑁) ∈ ℕ0 ∧
(♯‘𝐹) ∈
ℕ0 ∧ ((𝑥 + 𝑆) − 𝑁) ≤ (♯‘𝐹))) |
119 | 117, 118 | sylibr 237 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (0...𝑁)) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹))) |
120 | 119 | adantll 714 |
. . . . . . . . . . . 12
⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → ((𝑥 + 𝑆) − 𝑁) ∈ (0...(♯‘𝐹))) |
121 | 45, 120 | ffvelrnd 6862 |
. . . . . . . . . . 11
⊢ (((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) ∧ ¬ 𝑥 ≤ (𝑁 − 𝑆)) → (𝑃‘((𝑥 + 𝑆) − 𝑁)) ∈ 𝑉) |
122 | 44, 121 | ifclda 4449 |
. . . . . . . . . 10
⊢ ((𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ (𝜑 ∧ 𝑥 ∈ (0...𝑁))) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉) |
123 | 122 | exp32 424 |
. . . . . . . . 9
⊢ (𝑃:(0...(♯‘𝐹))⟶𝑉 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))) |
124 | 13, 123 | syl 17 |
. . . . . . . 8
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉))) |
125 | 11, 124 | mpcom 38 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (0...𝑁) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉)) |
126 | 125 | imp 410 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0...𝑁)) → if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))) ∈ 𝑉) |
127 | | crctcsh.q |
. . . . . 6
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
128 | 126, 127 | fmptd 6888 |
. . . . 5
⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉) |
129 | 12, 4, 2, 22, 15, 1 | crctcshlem2 27756 |
. . . . . . 7
⊢ (𝜑 → (♯‘𝐻) = 𝑁) |
130 | 129 | oveq2d 7186 |
. . . . . 6
⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁)) |
131 | 130 | feq2d 6490 |
. . . . 5
⊢ (𝜑 → (𝑄:(0...(♯‘𝐻))⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉)) |
132 | 128, 131 | mpbird 260 |
. . . 4
⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶𝑉) |
133 | 132 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑄:(0...(♯‘𝐻))⟶𝑉) |
134 | 12, 4 | wlkprop 27553 |
. . . . . 6
⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))) |
135 | 2, 3, 134 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))) |
136 | 135 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))))) |
137 | 22 | eqcomi 2747 |
. . . . . . . . . 10
⊢
(♯‘𝐹) =
𝑁 |
138 | 137 | oveq2i 7181 |
. . . . . . . . 9
⊢
(0..^(♯‘𝐹)) = (0..^𝑁) |
139 | 138 | raleqi 3314 |
. . . . . . . 8
⊢
(∀𝑖 ∈
(0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
140 | | fzo1fzo0n0 13179 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ (0..^𝑁) ∧ 𝑆 ≠ 0)) |
141 | 140 | simplbi2 504 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ (0..^𝑁) → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁))) |
142 | 15, 141 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ≠ 0 → 𝑆 ∈ (1..^𝑁))) |
143 | 142 | imp 410 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝑆 ∈ (1..^𝑁)) |
144 | 143 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝑆 ∈ (1..^𝑁)) |
145 | | simplll 775 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → 𝐹 ∈ Word dom 𝐼) |
146 | | wkslem1 27549 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) |
147 | 146 | cbvralvw 3349 |
. . . . . . . . . . . . 13
⊢
(∀𝑖 ∈
(0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
148 | 147 | biimpi 219 |
. . . . . . . . . . . 12
⊢
(∀𝑖 ∈
(0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
149 | 148 | adantl 485 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
150 | | crctprop 27733 |
. . . . . . . . . . . . . 14
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) |
151 | 137 | fveq2i 6677 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃‘(♯‘𝐹)) = (𝑃‘𝑁) |
152 | 151 | eqeq2i 2751 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘𝑁)) |
153 | 152 | biimpi 219 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘0) = (𝑃‘𝑁)) |
154 | 153 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃‘𝑁) = (𝑃‘0)) |
155 | 154 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘𝑁) = (𝑃‘0)) |
156 | 2, 150, 155 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0)) |
157 | 156 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (𝑃‘𝑁) = (𝑃‘0)) |
158 | 157 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (𝑃‘𝑁) = (𝑃‘0)) |
159 | 144, 127,
1, 22, 145, 149, 158 | crctcshwlkn0lem7 27754 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
160 | 129 | oveq2d 7186 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁)) |
161 | 160 | raleqdv 3316 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑗 ∈
(0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
162 | 161 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
163 | 162 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → (∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
164 | 159, 163 | mpbird 260 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) ∧ ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
165 | 164 | ex 416 |
. . . . . . . 8
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
166 | 139, 165 | syl5bi 245 |
. . . . . . 7
⊢ (((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (𝜑 ∧ 𝑆 ≠ 0)) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
167 | 166 | ex 416 |
. . . . . 6
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → ((𝜑 ∧ 𝑆 ≠ 0) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
168 | 167 | com23 86 |
. . . . 5
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) → (∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
169 | 168 | 3impia 1118 |
. . . 4
⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) → ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
170 | 136, 169 | mpcom 38 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
171 | 10, 133, 170 | 3jca 1129 |
. 2
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))))) |
172 | 12, 4, 2, 22, 15, 1, 127 | crctcshlem3 27757 |
. . . 4
⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
173 | 172 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) |
174 | 12, 4 | iswlk 27552 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
175 | 173, 174 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → (𝐻(Walks‘𝐺)𝑄 ↔ (𝐻 ∈ Word dom 𝐼 ∧ 𝑄:(0...(♯‘𝐻))⟶𝑉 ∧ ∀𝑗 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))))) |
176 | 171, 175 | mpbird 260 |
1
⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(Walks‘𝐺)𝑄) |