Step | Hyp | Ref
| Expression |
1 | | clwlkfclwwlk.c |
. . . . . 6
⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} |
2 | 1 | rabeq2i 3170 |
. . . . 5
⊢ (𝑐 ∈ 𝐶 ↔ (𝑐 ∈ (𝑉 ClWalks 𝐸) ∧ (#‘𝐴) = 𝑁)) |
3 | | clwlkfclwwlk.1 |
. . . . . . . 8
⊢ 𝐴 = (1st ‘𝑐) |
4 | | clwlkfclwwlk.2 |
. . . . . . . 8
⊢ 𝐵 = (2nd ‘𝑐) |
5 | 3, 4 | clwlkcompim 26292 |
. . . . . . 7
⊢ (𝑐 ∈ (𝑉 ClWalks 𝐸) → ((𝐴 ∈ Word dom 𝐸 ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))))) |
6 | | lencl 13179 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word dom 𝐸 → (#‘𝐴) ∈
ℕ0) |
7 | | clwlkfclwwlk.f |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) |
8 | 3, 4, 1, 7 | clwlkfclwwlk2wrd 26367 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word 𝑉) |
9 | 8 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word 𝑉) |
10 | | swrdcl 13271 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ Word 𝑉 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word 𝑉) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word 𝑉) |
12 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 𝐴 ∈ Word dom 𝐸) |
13 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝑉 USGrph 𝐸) |
14 | 12, 13 | anim12ci 589 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (𝑉 USGrph 𝐸 ∧ 𝐴 ∈ Word dom 𝐸)) |
15 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(#‘𝐴))⟶𝑉) |
16 | | prmuz2 15246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
(ℤ≥‘2)) |
17 | | ffz0hash 13088 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) → (#‘𝐵) = ((#‘𝐴) + 1)) |
18 | 17 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) → (#‘𝐵) = ((#‘𝐴) + 1)) |
19 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐴) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤
(#‘𝐴))) |
20 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 2 ∈
ℝ |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐴) ∈
ℤ → 2 ∈ ℝ) |
22 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ ℝ) |
23 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐴) ∈
ℝ → ((#‘𝐴)
+ 1) ∈ ℝ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
+ 1) ∈ ℝ) |
25 | 21, 22, 24 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
ℤ → (2 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈
ℝ)) |
26 | 25 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → (2 ∈ ℝ ∧
(#‘𝐴) ∈ ℝ
∧ ((#‘𝐴) + 1)
∈ ℝ)) |
27 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ (#‘𝐴)) |
28 | 22 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
≤ ((#‘𝐴) +
1)) |
29 | 28 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → (#‘𝐴) ≤ ((#‘𝐴) + 1)) |
30 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((2
∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) →
((2 ≤ (#‘𝐴) ∧
(#‘𝐴) ≤
((#‘𝐴) + 1)) → 2
≤ ((#‘𝐴) +
1))) |
31 | 30 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((2
∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) ∧ (2
≤ (#‘𝐴) ∧
(#‘𝐴) ≤
((#‘𝐴) + 1))) →
2 ≤ ((#‘𝐴) +
1)) |
32 | 26, 27, 29, 31 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1)) |
33 | 32 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((2
∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1)) |
34 | 19, 33 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ ((#‘𝐴) + 1)) |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → ((#‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ ((#‘𝐴) + 1))) |
36 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
37 | 36 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
38 | 37 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
39 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐵) =
((#‘𝐴) + 1) → (2
≤ (#‘𝐵) ↔ 2
≤ ((#‘𝐴) +
1))) |
40 | 39 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (2 ≤ (#‘𝐵) ↔ 2 ≤ ((#‘𝐴) + 1))) |
41 | 35, 38, 40 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
42 | 41 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐵) =
((#‘𝐴) + 1) →
((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
43 | 18, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
45 | 44 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
46 | 45 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
47 | 16, 46 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℙ →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom 𝐸) ∧
𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (#‘𝐵))) |
48 | 47 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (((((((#‘𝐴) ∈ ℕ0
∧ 𝐴 ∈ Word dom
𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (#‘𝐵))) |
49 | 48 | impcom 445 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → 2 ≤
(#‘𝐵)) |
50 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) |
51 | | clwlkisclwwlklem1 26315 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 USGrph 𝐸 ∧ 𝐴 ∈ Word dom 𝐸) ∧ (𝐵:(0...(#‘𝐴))⟶𝑉 ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran 𝐸)) |
52 | 14, 15, 49, 50, 51 | syl121anc 1323 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran 𝐸)) |
53 | 3, 4, 1, 7 | clwlkfclwwlk1hash 26369 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) ∈ (0...(#‘𝐵))) |
54 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝐵 ∈ Word 𝑉) |
55 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (#‘𝐴) ∈ (0...(#‘𝐵))) |
56 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(#‘𝐴) ∈
ℤ) |
57 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
− 1) ∈ ℤ) |
58 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ ℤ) |
59 | 22 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
− 1) ≤ (#‘𝐴)) |
60 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
(ℤ≥‘((#‘𝐴) − 1)) ↔ (((#‘𝐴) − 1) ∈ ℤ
∧ (#‘𝐴) ∈
ℤ ∧ ((#‘𝐴)
− 1) ≤ (#‘𝐴))) |
61 | 57, 58, 59, 60 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ (ℤ≥‘((#‘𝐴) − 1))) |
62 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) ∈
(ℤ≥‘((#‘𝐴) − 1)) → (0..^((#‘𝐴) − 1)) ⊆
(0..^(#‘𝐴))) |
63 | 56, 61, 62 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(0..^((#‘𝐴) −
1)) ⊆ (0..^(#‘𝐴))) |
64 | 63 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝑖 ∈
(0..^((#‘𝐴) −
1))) → 𝑖 ∈
(0..^(#‘𝐴))) |
65 | 64 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝑖 ∈ (0..^(#‘𝐴))) |
66 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝑖 ∈ (0..^(#‘𝐴))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
67 | 54, 55, 65, 66 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
68 | 67 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵‘𝑖) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖)) |
69 | | elfzom1elp1fzo 12402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝐴) ∈
ℤ ∧ 𝑖 ∈
(0..^((#‘𝐴) −
1))) → (𝑖 + 1) ∈
(0..^(#‘𝐴))) |
70 | 56, 69 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝑖 ∈
(0..^((#‘𝐴) −
1))) → (𝑖 + 1) ∈
(0..^(#‘𝐴))) |
71 | 70 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝐴))) |
72 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1))) |
73 | 72 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))) |
74 | 54, 55, 71, 73 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))) |
75 | 68, 74 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word 𝑉 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}) |
76 | 75 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(𝐵 ∈ Word 𝑉 → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}))) |
77 | 53, 8, 76 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ 𝐶 → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))})) |
78 | 77 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}) |
79 | 78 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
80 | 79 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ 𝐶 → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
81 | 80 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
82 | 3, 4, 1, 7 | clwlkfclwwlk2sswd 26370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) = (#‘(𝐵 substr 〈0, (#‘𝐴)〉))) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) − 1) = ((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)) |
84 | 83 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → ((#‘𝐴) − 1) = ((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) −
1)) |
85 | 84 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) →
(0..^((#‘𝐴) −
1)) = (0..^((#‘(𝐵
substr 〈0, (#‘𝐴)〉)) − 1))) |
86 | 85 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
87 | 81, 86 | bitrd 267 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸)) |
88 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ ↔ (#‘𝐴) ∈
ℙ)) |
89 | 88 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ → (#‘𝐴) ∈
ℙ)) |
90 | 89 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (#‘𝐴) ∈
ℙ)) |
91 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐴) ∈
ℙ → (#‘𝐴)
∈ ℕ) |
92 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) ↔
((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵))) |
93 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → 1
∈ ℤ) |
94 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐵) ∈
ℕ0 → (#‘𝐵) ∈ ℤ) |
95 | 94 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
(#‘𝐵) ∈
ℤ) |
96 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈ ℤ) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
(#‘𝐴) ∈
ℤ) |
98 | 93, 95, 97 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → (1
∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
99 | 98 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) → (1
∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
100 | 99 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
101 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(#‘𝐴) ≤
(#‘𝐵)) |
102 | | nnge1 10923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝐴) ∈
ℕ → 1 ≤ (#‘𝐴)) |
103 | 101, 102 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (1 ≤ (#‘𝐴)
∧ (#‘𝐴) ≤
(#‘𝐵))) |
104 | 100, 103 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
105 | 92, 104 | sylanb 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
106 | | elfz2 12204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
(1...(#‘𝐵)) ↔
((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
107 | 105, 106 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (#‘𝐴) ∈
(1...(#‘𝐵))) |
108 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)) = (𝐵‘((#‘𝐴) − 1))) |
109 | 108 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘((#‘𝐴) − 1)) = ( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉))) |
110 | | swrd0fv0 13292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘0) = (𝐵‘0)) |
111 | 110 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘0) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)) |
112 | 109, 111 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐵 ∈ Word 𝑉 ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}) |
113 | 112 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) ∈
(1...(#‘𝐵)) →
(𝐵 ∈ Word 𝑉 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
114 | 107, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (𝐵 ∈ Word 𝑉 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
115 | 114 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
((#‘𝐴) ∈ ℕ
→ (𝐵 ∈ Word 𝑉 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
116 | 115 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(𝐵 ∈ Word 𝑉 → ((#‘𝐴) ∈ ℕ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)}))) |
117 | 53, 8, 116 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) ∈ ℕ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
118 | 91, 117 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝐴) ∈
ℙ → (𝑐 ∈
𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)})) |
119 | 90, 118 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (𝑐 ∈ 𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
120 | 119 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
121 | 120 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
122 | 121 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
123 | 122 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈ ℙ →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom 𝐸) ∧
𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
124 | 123 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (((((((#‘𝐴) ∈ ℕ0
∧ 𝐴 ∈ Word dom
𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
125 | 124 | impcom 445 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}) |
126 | 125 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran 𝐸 ↔ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸)) |
127 | 87, 126 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → ((( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran 𝐸) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸))) |
128 | 52, 127 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸)) |
129 | | 3simpc 1053 |
. . . . . . . . . . . . . . . 16
⊢ ((( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸) → (∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸)) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸)) |
131 | | 3anass 1035 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word 𝑉 ∧ (∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸))) |
132 | 11, 130, 131 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸)) |
133 | | usgrav 25867 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
134 | 133 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
135 | 134 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
136 | | isclwwlk 26296 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸))) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑉 ClWWalks 𝐸) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ ran 𝐸))) |
138 | 132, 137 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑉 ClWWalks 𝐸)) |
139 | 82 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 ↔ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
140 | 139 | biimpcd 238 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
141 | 140 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
142 | 141 | imp 444 |
. . . . . . . . . . . . . 14
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁) |
143 | 142 | adantr 480 |
. . . . . . . . . . . . 13
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁) |
144 | 138, 143 | jca 553 |
. . . . . . . . . . . 12
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
145 | 133 | simpld 474 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 USGrph 𝐸 → 𝑉 ∈ V) |
146 | 145 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → 𝑉 ∈ V) |
147 | 133 | simprd 478 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
148 | 147 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → 𝐸 ∈ V) |
149 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
150 | 149 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ0) |
151 | 150 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ0) |
152 | 146, 148,
151 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
153 | 152 | 3adant2 1073 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
154 | 153 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈
ℕ0)) |
155 | | isclwwlkn 26297 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑁 ∈ ℕ0)
→ ((𝐵 substr 〈0,
(#‘𝐴)〉) ∈
((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁))) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . 12
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑉 ClWWalks 𝐸) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁))) |
157 | 144, 156 | mpbird 246 |
. . . . . . . . . . 11
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
158 | 157 | exp31 628 |
. . . . . . . . . 10
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom 𝐸) ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)))) |
159 | 158 | exp41 636 |
. . . . . . . . 9
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom 𝐸) →
(𝐵:(0...(#‘𝐴))⟶𝑉 → ((∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))))))) |
160 | 6, 159 | mpancom 700 |
. . . . . . . 8
⊢ (𝐴 ∈ Word dom 𝐸 → (𝐵:(0...(#‘𝐴))⟶𝑉 → ((∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))))))) |
161 | 160 | imp31 447 |
. . . . . . 7
⊢ (((𝐴 ∈ Word dom 𝐸 ∧ 𝐵:(0...(#‘𝐴))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))(𝐸‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))))) |
162 | 5, 161 | syl 17 |
. . . . . 6
⊢ (𝑐 ∈ (𝑉 ClWalks 𝐸) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))))) |
163 | 162 | imp 444 |
. . . . 5
⊢ ((𝑐 ∈ (𝑉 ClWalks 𝐸) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)))) |
164 | 2, 163 | sylbi 206 |
. . . 4
⊢ (𝑐 ∈ 𝐶 → (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)))) |
165 | 164 | pm2.43i 50 |
. . 3
⊢ (𝑐 ∈ 𝐶 → ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) |
166 | 165 | impcom 445 |
. 2
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ 𝐶) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) |
167 | 166, 7 | fmptd 6292 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶((𝑉 ClWWalksN 𝐸)‘𝑁)) |