Step | Hyp | Ref
| Expression |
1 | | clwlksfclwwlk.c |
. . . . . 6
⊢ 𝐶 = {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁} |
2 | 1 | rabeq2i 3170 |
. . . . 5
⊢ (𝑐 ∈ 𝐶 ↔ (𝑐 ∈ (ClWalkS‘𝐺) ∧ (#‘𝐴) = 𝑁)) |
3 | | fusgrusgr 40541 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph
) |
4 | | usgrupgr 40412 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph
) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ UPGraph
) |
6 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ UPGraph
) |
7 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
8 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
9 | | clwlksfclwwlk.1 |
. . . . . . . . . . 11
⊢ 𝐴 = (1st ‘𝑐) |
10 | | clwlksfclwwlk.2 |
. . . . . . . . . . 11
⊢ 𝐵 = (2nd ‘𝑐) |
11 | 7, 8, 9, 10 | upgrclwlkcompim 40988 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) |
12 | 6, 11 | sylan 487 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) |
13 | | lencl 13179 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word dom
(iEdg‘𝐺) →
(#‘𝐴) ∈
ℕ0) |
14 | | clwlksfclwwlk.f |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) |
15 | 9, 10, 1, 14 | clwlksfclwwlk2wrd 41265 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word (Vtx‘𝐺)) |
16 | 15 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
17 | | swrdcl 13271 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ∈ Word (Vtx‘𝐺) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word (Vtx‘𝐺)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word (Vtx‘𝐺)) |
19 | | ffz0iswrd 13187 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺)) |
20 | 19 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
21 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ) |
23 | 22 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ) |
24 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) = 𝑁 → (0...(#‘𝐴)) = (0...𝑁)) |
25 | 24 | feq2d 5944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) = 𝑁 → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺))) |
26 | 22 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ0) |
27 | | ffz0hash 13088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (#‘𝐵) = (𝑁 + 1)) |
28 | 26, 27 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (#‘𝐵) = (𝑁 + 1)) |
29 | 28 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (#‘𝐵) = (𝑁 + 1))) |
30 | 21 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℝ) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ) |
32 | 31 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1)) |
33 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐵) =
(𝑁 + 1) → (𝑁 ≤ (#‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1))) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (#‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1))) |
35 | 32, 34 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (#‘𝐵)) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 ∈ ℙ →
((#‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (#‘𝐵))) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
((#‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (#‘𝐵))) |
38 | 29, 37 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → 𝑁 ≤ (#‘𝐵))) |
39 | 38 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (#‘𝐵))) |
40 | 25, 39 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) = 𝑁 → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (#‘𝐵)))) |
41 | 40 | 3imp21 1269 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (#‘𝐵)) |
42 | | swrdn0 13282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (#‘𝐵)) → (𝐵 substr 〈0, 𝑁〉) ≠ ∅) |
43 | 20, 23, 41, 42 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, 𝑁〉) ≠ ∅) |
44 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) = 𝑁 → 〈0, (#‘𝐴)〉 = 〈0, 𝑁〉) |
45 | 44 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) = (𝐵 substr 〈0, 𝑁〉)) |
46 | 45 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐴) = 𝑁 → ((𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅ ↔ (𝐵 substr 〈0, 𝑁〉) ≠
∅)) |
47 | 46 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅ ↔ (𝐵 substr 〈0, 𝑁〉) ≠
∅)) |
48 | 43, 47 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅) |
49 | 48 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((#‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅))) |
50 | 49 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅))) |
51 | 50 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅)) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅)) |
53 | 52 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅) |
54 | 18, 53 | jca 553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅)) |
55 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺)) |
56 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USGraph
) |
57 | 55, 56 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺))) |
58 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) |
59 | | prmuz2 15246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
(ℤ≥‘2)) |
60 | | ffz0hash 13088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → (#‘𝐵) = ((#‘𝐴) + 1)) |
61 | 60 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → (#‘𝐵) = ((#‘𝐴) + 1)) |
62 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝐴) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤
(#‘𝐴))) |
63 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 2 ∈
ℝ |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
ℤ → 2 ∈ ℝ) |
65 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ ℝ) |
66 | | peano2re 10088 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((#‘𝐴) ∈
ℝ → ((#‘𝐴)
+ 1) ∈ ℝ) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
+ 1) ∈ ℝ) |
68 | 64, 65, 67 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → (2 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈
ℝ)) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → (2 ∈ ℝ ∧
(#‘𝐴) ∈ ℝ
∧ ((#‘𝐴) + 1)
∈ ℝ)) |
70 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ (#‘𝐴)) |
71 | 65 | lep1d 10834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
≤ ((#‘𝐴) +
1)) |
72 | 71 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → (#‘𝐴) ≤ ((#‘𝐴) + 1)) |
73 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((2
∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) →
((2 ≤ (#‘𝐴) ∧
(#‘𝐴) ≤
((#‘𝐴) + 1)) → 2
≤ ((#‘𝐴) +
1))) |
74 | 73 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((2
∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) ∧ (2
≤ (#‘𝐴) ∧
(#‘𝐴) ≤
((#‘𝐴) + 1))) →
2 ≤ ((#‘𝐴) +
1)) |
75 | 69, 70, 72, 74 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1)) |
76 | 75 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((2
∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1)) |
77 | 62, 76 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ ((#‘𝐴) + 1)) |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → ((#‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ ((#‘𝐴) + 1))) |
79 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
80 | 79 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
82 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐵) =
((#‘𝐴) + 1) → (2
≤ (#‘𝐵) ↔ 2
≤ ((#‘𝐴) +
1))) |
83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (2 ≤ (#‘𝐵) ↔ 2 ≤ ((#‘𝐴) + 1))) |
84 | 78, 81, 83 | 3imtr4d 282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
85 | 84 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐵) =
((#‘𝐴) + 1) →
((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
86 | 61, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
87 | 86 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
88 | 87 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
90 | 59, 89 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℙ →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (#‘𝐵))) |
91 | 90 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (#‘𝐵))) |
92 | 91 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤
(#‘𝐵)) |
93 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) |
94 | 7, 8 | usgrf 40385 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) =
2}) |
95 | 94 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) →
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) = 2} ∧
𝐴 ∈ Word dom
(iEdg‘𝐺))) |
96 | | clwlkclwwlklem2 41209 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) = 2} ∧
𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))) |
97 | 95, 96 | syl3an1 1351 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))) |
98 | | edgaval 25794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐺 ∈ USGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
99 | 98 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐺 ∈ USGraph → ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))) |
100 | 99 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐺 ∈ USGraph →
(∀𝑖 ∈
(0..^((#‘𝐴) −
1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺))) |
101 | 98 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐺 ∈ USGraph → ({(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈
(Edg‘𝐺) ↔
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran
(iEdg‘𝐺))) |
102 | 100, 101 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ USGraph → ((( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))) |
103 | 102 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) → (((
lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))) |
104 | 103 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺)))) |
105 | 97, 104 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺))) |
106 | 57, 58, 92, 93, 105 | syl121anc 1323 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺))) |
107 | 9, 10, 1, 14 | clwlksfclwwlk1hash 41267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) ∈ (0...(#‘𝐵))) |
108 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺)) |
109 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) →
(#‘𝐴) ∈
(0...(#‘𝐵))) |
110 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(#‘𝐴) ∈
ℤ) |
111 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
− 1) ∈ ℤ) |
112 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ ℤ) |
113 | 65 | lem1d 10836 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
− 1) ≤ (#‘𝐴)) |
114 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
(ℤ≥‘((#‘𝐴) − 1)) ↔ (((#‘𝐴) − 1) ∈ ℤ
∧ (#‘𝐴) ∈
ℤ ∧ ((#‘𝐴)
− 1) ≤ (#‘𝐴))) |
115 | 111, 112,
113, 114 | syl3anbrc 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ (ℤ≥‘((#‘𝐴) − 1))) |
116 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
(ℤ≥‘((#‘𝐴) − 1)) → (0..^((#‘𝐴) − 1)) ⊆
(0..^(#‘𝐴))) |
117 | 110, 115,
116 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(0..^((#‘𝐴) −
1)) ⊆ (0..^(#‘𝐴))) |
118 | 117 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝑖 ∈
(0..^((#‘𝐴) −
1))) → 𝑖 ∈
(0..^(#‘𝐴))) |
119 | 118 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝑖 ∈ (0..^(#‘𝐴))) |
120 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝑖 ∈ (0..^(#‘𝐴))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
121 | 108, 109,
119, 120 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
122 | 121 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵‘𝑖) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖)) |
123 | | elfzom1elp1fzo 12402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝐴) ∈
ℤ ∧ 𝑖 ∈
(0..^((#‘𝐴) −
1))) → (𝑖 + 1) ∈
(0..^(#‘𝐴))) |
124 | 110, 123 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝑖 ∈
(0..^((#‘𝐴) −
1))) → (𝑖 + 1) ∈
(0..^(#‘𝐴))) |
125 | 124 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝐴))) |
126 | | swrd0fv 13291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1))) |
127 | 126 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))) |
128 | 108, 109,
125, 127 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))) |
129 | 122, 128 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}) |
130 | 129 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(𝐵 ∈ Word
(Vtx‘𝐺) → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}))) |
131 | 107, 15, 130 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ 𝐶 → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))})) |
132 | 131 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}) |
133 | 132 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
134 | 133 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ 𝐶 → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
135 | 134 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
136 | 9, 10, 1, 14 | clwlksfclwwlk2sswd 41268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) = (#‘(𝐵 substr 〈0, (#‘𝐴)〉))) |
137 | 136 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) − 1) = ((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)) |
138 | 137 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((#‘𝐴) − 1) = ((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) −
1)) |
139 | 138 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) →
(0..^((#‘𝐴) −
1)) = (0..^((#‘(𝐵
substr 〈0, (#‘𝐴)〉)) − 1))) |
140 | 139 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
141 | 135, 140 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
142 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ ↔ (#‘𝐴) ∈
ℙ)) |
143 | 142 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ → (#‘𝐴) ∈
ℙ)) |
144 | 143 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (#‘𝐴) ∈
ℙ)) |
145 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐴) ∈
ℙ → (#‘𝐴)
∈ ℕ) |
146 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) ↔
((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵))) |
147 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → 1
∈ ℤ) |
148 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
((#‘𝐵) ∈
ℕ0 → (#‘𝐵) ∈ ℤ) |
149 | 148 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
(#‘𝐵) ∈
ℤ) |
150 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈ ℤ) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
(#‘𝐴) ∈
ℤ) |
152 | 147, 149,
151 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → (1
∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
153 | 152 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) → (1
∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
154 | 153 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
155 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(#‘𝐴) ≤
(#‘𝐵)) |
156 | | nnge1 10923 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((#‘𝐴) ∈
ℕ → 1 ≤ (#‘𝐴)) |
157 | 155, 156 | anim12ci 589 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (1 ≤ (#‘𝐴)
∧ (#‘𝐴) ≤
(#‘𝐵))) |
158 | 154, 157 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
159 | 146, 158 | sylanb 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
160 | | elfz2 12204 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
(1...(#‘𝐵)) ↔
((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
161 | 159, 160 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (#‘𝐴) ∈
(1...(#‘𝐵))) |
162 | | swrd0fvlsw 13295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)) = (𝐵‘((#‘𝐴) − 1))) |
163 | 162 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘((#‘𝐴) − 1)) = ( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉))) |
164 | | swrd0fv0 13292 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘0) = (𝐵‘0)) |
165 | 164 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘0) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)) |
166 | 163, 165 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}) |
167 | 166 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
(1...(#‘𝐵)) →
(𝐵 ∈ Word
(Vtx‘𝐺) →
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)})) |
168 | 161, 167 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (𝐵 ∈ Word
(Vtx‘𝐺) →
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)})) |
169 | 168 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
((#‘𝐴) ∈ ℕ
→ (𝐵 ∈ Word
(Vtx‘𝐺) →
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)}))) |
170 | 169 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(𝐵 ∈ Word
(Vtx‘𝐺) →
((#‘𝐴) ∈ ℕ
→ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
171 | 107, 15, 170 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) ∈ ℕ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
172 | 145, 171 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
ℙ → (𝑐 ∈
𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)})) |
173 | 144, 172 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (𝑐 ∈ 𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
174 | 173 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
175 | 174 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
176 | 175 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
177 | 176 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℙ →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
178 | 177 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
179 | 178 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}) |
180 | 179 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈
(Edg‘𝐺) ↔ {(
lastS ‘(𝐵 substr
〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
181 | 141, 180 | 3anbi23d 1394 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)))) |
182 | 106, 181 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
183 | | 3simpc 1053 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)) → (∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
185 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅) ∧
∀𝑖 ∈
(0..^((#‘(𝐵 substr
〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)) ↔ (((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅) ∧ (∀𝑖 ∈ (0..^((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺)))) |
186 | 54, 184, 185 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word
(Vtx‘𝐺) ∧ (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅) ∧
∀𝑖 ∈
(0..^((#‘(𝐵 substr
〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
187 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
188 | 7, 187 | isclwwlks 41188 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈
(ClWWalkS‘𝐺) ↔
(((𝐵 substr 〈0,
(#‘𝐴)〉) ∈
Word (Vtx‘𝐺) ∧
(𝐵 substr 〈0,
(#‘𝐴)〉) ≠
∅) ∧ ∀𝑖
∈ (0..^((#‘(𝐵
substr 〈0, (#‘𝐴)〉)) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
189 | 186, 188 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalkS‘𝐺)) |
190 | 136 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 ↔ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
191 | 190 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
192 | 191 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
193 | 192 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁) |
194 | 193 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁) |
195 | 189, 194 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalkS‘𝐺) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
196 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ) |
197 | | isclwwlksn 41190 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalkS‘𝐺) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁))) |
198 | 196, 197 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalkS‘𝐺) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁))) |
199 | 195, 198 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺)) |
200 | 199 | exp31 628 |
. . . . . . . . . . . . . . . 16
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺)))) |
201 | 200 | exp41 636 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))))) |
202 | 13, 201 | mpancom 700 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Word dom
(iEdg‘𝐺) →
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))))) |
203 | 202 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺)))))) |
204 | 203 | 3impib 1254 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))) |
205 | 204 | com12 32 |
. . . . . . . . . . 11
⊢
((#‘𝐴) = 𝑁 → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))) |
206 | 205 | com14 94 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))) |
207 | 206 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))) |
208 | 12, 207 | mpd 15 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalkS‘𝐺)) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺)))) |
209 | 208 | expcom 450 |
. . . . . . 7
⊢ (𝑐 ∈ (ClWalkS‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))) |
210 | 209 | com24 93 |
. . . . . 6
⊢ (𝑐 ∈ (ClWalkS‘𝐺) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))))) |
211 | 210 | imp 444 |
. . . . 5
⊢ ((𝑐 ∈ (ClWalkS‘𝐺) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺)))) |
212 | 2, 211 | sylbi 206 |
. . . 4
⊢ (𝑐 ∈ 𝐶 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺)))) |
213 | 212 | pm2.43i 50 |
. . 3
⊢ (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺))) |
214 | 213 | impcom 445 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ 𝐶) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalkSN 𝐺)) |
215 | 214, 14 | fmptd 6292 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalkSN 𝐺)) |