Step | Hyp | Ref
| Expression |
1 | | clwlksfclwwlk.c |
. . . . . 6
⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} |
2 | 1 | rabeq2i 3197 |
. . . . 5
⊢ (𝑐 ∈ 𝐶 ↔ (𝑐 ∈ (ClWalks‘𝐺) ∧ (#‘𝐴) = 𝑁)) |
3 | | fusgrusgr 26214 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ USGraph
) |
4 | | usgrupgr 26077 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph
) |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ FinUSGraph → 𝐺 ∈ UPGraph
) |
6 | 5 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ UPGraph
) |
7 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
8 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
9 | | clwlksfclwwlk.1 |
. . . . . . . . . . 11
⊢ 𝐴 = (1st ‘𝑐) |
10 | | clwlksfclwwlk.2 |
. . . . . . . . . . 11
⊢ 𝐵 = (2nd ‘𝑐) |
11 | 7, 8, 9, 10 | upgrclwlkcompim 26677 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UPGraph ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) |
12 | 6, 11 | sylan 488 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → ((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) |
13 | | lencl 13324 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ Word dom
(iEdg‘𝐺) →
(#‘𝐴) ∈
ℕ0) |
14 | | clwlksfclwwlk.f |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) |
15 | 9, 10, 1, 14 | clwlksfclwwlk2wrd 26958 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word (Vtx‘𝐺)) |
16 | 15 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
17 | | swrdcl 13419 |
. . . . . . . . . . . . . . . . . . . . . . 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 13332 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → 𝐵 ∈ Word (Vtx‘𝐺)) |
20 | 19 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵 ∈ Word (Vtx‘𝐺)) |
21 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℕ) |
22 | 21 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ) |
23 | 22 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ) |
24 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) = 𝑁 → (0...(#‘𝐴)) = (0...𝑁)) |
25 | 24 | feq2d 6031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) = 𝑁 → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ↔ 𝐵:(0...𝑁)⟶(Vtx‘𝐺))) |
26 | 22 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∈
ℕ0) |
27 | | ffz0hash 13231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℕ0
∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (#‘𝐵) = (𝑁 + 1)) |
28 | 26, 27 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝐵:(0...𝑁)⟶(Vtx‘𝐺)) → (#‘𝐵) = (𝑁 + 1)) |
29 | 28 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → (#‘𝐵) = (𝑁 + 1))) |
30 | 21 | nnred 11035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
ℝ) |
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → 𝑁 ∈ ℝ) |
32 | 31 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (𝑁 + 1)) |
33 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝐵) =
(𝑁 + 1) → (𝑁 ≤ (#‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1))) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → (𝑁 ≤ (#‘𝐵) ↔ 𝑁 ≤ (𝑁 + 1))) |
35 | 32, 34 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑁 ∈ ℙ ∧
(#‘𝐵) = (𝑁 + 1)) → 𝑁 ≤ (#‘𝐵)) |
36 | 35 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 ∈ ℙ →
((#‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (#‘𝐵))) |
37 | 36 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
((#‘𝐵) = (𝑁 + 1) → 𝑁 ≤ (#‘𝐵))) |
38 | 29, 37 | syldc 48 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵:(0...𝑁)⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (#‘𝐵))) |
39 | 25, 38 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) = 𝑁 → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ≤ (#‘𝐵)))) |
40 | 39 | 3imp21 1277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ≤ (#‘𝐵)) |
41 | | swrdn0 13430 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (#‘𝐵)) → (𝐵 substr 〈0, 𝑁〉) ≠ ∅) |
42 | 20, 23, 40, 41 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, 𝑁〉) ≠ ∅) |
43 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) = 𝑁 → 〈0, (#‘𝐴)〉 = 〈0, 𝑁〉) |
44 | 43 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) = (𝐵 substr 〈0, 𝑁〉)) |
45 | 44 | neeq1d 2853 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((#‘𝐴) = 𝑁 → ((𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅ ↔ (𝐵 substr 〈0, 𝑁〉) ≠
∅)) |
46 | 45 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅ ↔ (𝐵 substr 〈0, 𝑁〉) ≠
∅)) |
47 | 42, 46 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ (#‘𝐴) = 𝑁 ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅) |
48 | 47 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((#‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅))) |
49 | 48 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅))) |
50 | 49 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅)) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅)) |
52 | 51 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅) |
53 | 18, 52 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ Word (Vtx‘𝐺) ∧ (𝐵 substr 〈0, (#‘𝐴)〉) ≠ ∅)) |
54 | | simp-5r 809 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 𝐴 ∈ Word dom (iEdg‘𝐺)) |
55 | 3 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐺 ∈ USGraph
) |
56 | 54, 55 | anim12ci 591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom (iEdg‘𝐺))) |
57 | | simp-5r 809 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) |
58 | | prmuz2 15408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℙ → 𝑁 ∈
(ℤ≥‘2)) |
59 | | ffz0hash 13231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → (#‘𝐵) = ((#‘𝐴) + 1)) |
60 | 59 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → (#‘𝐵) = ((#‘𝐴) + 1)) |
61 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝐴) ∈
(ℤ≥‘2) ↔ (2 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤
(#‘𝐴))) |
62 | | 2re 11090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ 2 ∈
ℝ |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
ℤ → 2 ∈ ℝ) |
64 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ ℝ) |
65 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((#‘𝐴) ∈
ℝ → ((#‘𝐴)
+ 1) ∈ ℝ) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
+ 1) ∈ ℝ) |
67 | 63, 64, 66 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → (2 ∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈
ℝ)) |
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → (2 ∈ ℝ ∧
(#‘𝐴) ∈ ℝ
∧ ((#‘𝐴) + 1)
∈ ℝ)) |
69 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ (#‘𝐴)) |
70 | 64 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
≤ ((#‘𝐴) +
1)) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → (#‘𝐴) ≤ ((#‘𝐴) + 1)) |
72 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((2
∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) →
((2 ≤ (#‘𝐴) ∧
(#‘𝐴) ≤
((#‘𝐴) + 1)) → 2
≤ ((#‘𝐴) +
1))) |
73 | 72 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((2
∈ ℝ ∧ (#‘𝐴) ∈ ℝ ∧ ((#‘𝐴) + 1) ∈ ℝ) ∧ (2
≤ (#‘𝐴) ∧
(#‘𝐴) ≤
((#‘𝐴) + 1))) →
2 ≤ ((#‘𝐴) +
1)) |
74 | 68, 69, 71, 73 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝐴) ∈
ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1)) |
75 | 74 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((2
∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 2 ≤ (#‘𝐴)) → 2 ≤ ((#‘𝐴) + 1)) |
76 | 61, 75 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ ((#‘𝐴) + 1)) |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → ((#‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ ((#‘𝐴) + 1))) |
78 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
79 | 78 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
80 | 79 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
↔ (#‘𝐴) ∈
(ℤ≥‘2))) |
81 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐵) =
((#‘𝐴) + 1) → (2
≤ (#‘𝐵) ↔ 2
≤ ((#‘𝐴) +
1))) |
82 | 81 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (2 ≤ (#‘𝐵) ↔ 2 ≤ ((#‘𝐴) + 1))) |
83 | 77, 80, 82 | 3imtr4d 283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐵) =
((#‘𝐴) + 1) ∧
(#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
84 | 83 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐵) =
((#‘𝐴) + 1) →
((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
85 | 60, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → ((#‘𝐴) = 𝑁 → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵)))) |
87 | 86 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ (ℤ≥‘2)
→ 2 ≤ (#‘𝐵))) |
89 | 58, 88 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑁 ∈ ℙ →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (#‘𝐵))) |
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → 2 ≤ (#‘𝐵))) |
91 | 90 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 2 ≤
(#‘𝐵)) |
92 | | simp-4r 807 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) |
93 | 7, 8 | usgrf 26050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) =
2}) |
94 | 93 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) →
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) = 2} ∧
𝐴 ∈ Word dom
(iEdg‘𝐺))) |
95 | | clwlkclwwlklem2 26901 |
. . . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺))) |
96 | 94, 95 | syl3an1 1359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))) |
97 | | biid 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (( lastS
‘𝐵) = (𝐵‘0) ↔ ( lastS
‘𝐵) = (𝐵‘0)) |
98 | | edgval 25941 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
99 | 98 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)) |
100 | 99 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑖 ∈
(0..^((#‘𝐴) −
1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺)) |
101 | 98 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ({(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈
(Edg‘𝐺) ↔
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran
(iEdg‘𝐺)) |
102 | 97, 100, 101 | 3anbi123i 1251 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺)) ↔ (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ ran (iEdg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ ran (iEdg‘𝐺))) |
103 | 96, 102 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐺 ∈ USGraph ∧ 𝐴 ∈ Word dom
(iEdg‘𝐺)) ∧
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) ∧ 2 ≤ (#‘𝐵)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) → (( lastS ‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺))) |
104 | 56, 57, 91, 92, 103 | syl121anc 1331 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (( lastS
‘𝐵) = (𝐵‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈ (Edg‘𝐺))) |
105 | 9, 10, 1, 14 | clwlksfclwwlk1hash 26960 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) ∈ (0...(#‘𝐵))) |
106 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝐵 ∈ Word (Vtx‘𝐺)) |
107 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) →
(#‘𝐴) ∈
(0...(#‘𝐵))) |
108 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(#‘𝐴) ∈
ℤ) |
109 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
− 1) ∈ ℤ) |
110 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ ℤ) |
111 | 64 | lem1d 10957 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝐴)
− 1) ≤ (#‘𝐴)) |
112 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
(ℤ≥‘((#‘𝐴) − 1)) ↔ (((#‘𝐴) − 1) ∈ ℤ
∧ (#‘𝐴) ∈
ℤ ∧ ((#‘𝐴)
− 1) ≤ (#‘𝐴))) |
113 | 109, 110,
111, 112 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
ℤ → (#‘𝐴)
∈ (ℤ≥‘((#‘𝐴) − 1))) |
114 | | fzoss2 12496 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
(ℤ≥‘((#‘𝐴) − 1)) → (0..^((#‘𝐴) − 1)) ⊆
(0..^(#‘𝐴))) |
115 | 108, 113,
114 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(0..^((#‘𝐴) −
1)) ⊆ (0..^(#‘𝐴))) |
116 | 115 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝑖 ∈
(0..^((#‘𝐴) −
1))) → 𝑖 ∈
(0..^(#‘𝐴))) |
117 | 116 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → 𝑖 ∈ (0..^(#‘𝐴))) |
118 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ 𝑖 ∈ (0..^(#‘𝐴))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
119 | 106, 107,
117, 118 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖) = (𝐵‘𝑖)) |
120 | 119 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵‘𝑖) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖)) |
121 | | elfzom1elp1fzo 12534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((#‘𝐴) ∈
ℤ ∧ 𝑖 ∈
(0..^((#‘𝐴) −
1))) → (𝑖 + 1) ∈
(0..^(#‘𝐴))) |
122 | 108, 121 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝑖 ∈
(0..^((#‘𝐴) −
1))) → (𝑖 + 1) ∈
(0..^(#‘𝐴))) |
123 | 122 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝑖 + 1) ∈ (0..^(#‘𝐴))) |
124 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1)) = (𝐵‘(𝑖 + 1))) |
125 | 124 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (0...(#‘𝐵)) ∧ (𝑖 + 1) ∈ (0..^(#‘𝐴))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))) |
126 | 106, 107,
123, 125 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → (𝐵‘(𝑖 + 1)) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))) |
127 | 120, 126 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
𝐵 ∈ Word
(Vtx‘𝐺) ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}) |
128 | 127 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(𝐵 ∈ Word
(Vtx‘𝐺) → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}))) |
129 | 105, 15, 128 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ 𝐶 → (𝑖 ∈ (0..^((#‘𝐴) − 1)) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))})) |
130 | 129 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} = {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))}) |
131 | 130 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑐 ∈ 𝐶 ∧ 𝑖 ∈ (0..^((#‘𝐴) − 1))) → ({(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
132 | 131 | ralbidva 2985 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑐 ∈ 𝐶 → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
133 | 132 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (∀𝑖 ∈ (0..^((#‘𝐴) − 1)){(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((#‘𝐴) − 1)){((𝐵 substr 〈0, (#‘𝐴)〉)‘𝑖), ((𝐵 substr 〈0, (#‘𝐴)〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
134 | 9, 10, 1, 14 | clwlksfclwwlk2sswd 26961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) = (#‘(𝐵 substr 〈0, (#‘𝐴)〉))) |
135 | 134 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) − 1) = ((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) − 1)) |
136 | 135 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((#‘𝐴) − 1) = ((#‘(𝐵 substr 〈0, (#‘𝐴)〉)) −
1)) |
137 | 136 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) →
(0..^((#‘𝐴) −
1)) = (0..^((#‘(𝐵
substr 〈0, (#‘𝐴)〉)) − 1))) |
138 | 137 | raleqdv 3144 |
. . . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺))) |
139 | 133, 138 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . 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‘𝐺))) |
140 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ ↔ (#‘𝐴) ∈
ℙ)) |
141 | 140 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑁 = (#‘𝐴) → (𝑁 ∈ ℙ → (#‘𝐴) ∈
ℙ)) |
142 | 141 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (#‘𝐴) ∈
ℙ)) |
143 | | prmnn 15388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((#‘𝐴) ∈
ℙ → (#‘𝐴)
∈ ℕ) |
144 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) ↔
((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵))) |
145 | | 1zzd 11408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → 1
∈ ℤ) |
146 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
((#‘𝐵) ∈
ℕ0 → (#‘𝐵) ∈ ℤ) |
147 | 146 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
(#‘𝐵) ∈
ℤ) |
148 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢
((#‘𝐴) ∈
ℕ0 → (#‘𝐴) ∈ ℤ) |
149 | 148 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) →
(#‘𝐴) ∈
ℤ) |
150 | 145, 147,
149 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0) → (1
∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
151 | 150 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) → (1
∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
152 | 151 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈
ℤ)) |
153 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((#‘𝐴) ∈
ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) →
(#‘𝐴) ≤
(#‘𝐵)) |
154 | | nnge1 11046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
((#‘𝐴) ∈
ℕ → 1 ≤ (#‘𝐴)) |
155 | 153, 154 | anim12ci 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (1 ≤ (#‘𝐴)
∧ (#‘𝐴) ≤
(#‘𝐵))) |
156 | 152, 155 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((#‘𝐴)
∈ ℕ0 ∧ (#‘𝐵) ∈ ℕ0 ∧
(#‘𝐴) ≤
(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
157 | 144, 156 | sylanb 489 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ ((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
158 | | elfz2 12333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((#‘𝐴) ∈
(1...(#‘𝐵)) ↔
((1 ∈ ℤ ∧ (#‘𝐵) ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) ∧ (1 ≤
(#‘𝐴) ∧
(#‘𝐴) ≤
(#‘𝐵)))) |
159 | 157, 158 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (#‘𝐴) ∈
(1...(#‘𝐵))) |
160 | | swrd0fvlsw 13443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)) = (𝐵‘((#‘𝐴) − 1))) |
161 | 160 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘((#‘𝐴) − 1)) = ( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉))) |
162 | | swrd0fv0 13440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → ((𝐵 substr 〈0, (#‘𝐴)〉)‘0) = (𝐵‘0)) |
163 | 162 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → (𝐵‘0) = ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)) |
164 | 161, 163 | preq12d 4276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝐵 ∈ Word (Vtx‘𝐺) ∧ (#‘𝐴) ∈ (1...(#‘𝐵))) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}) |
165 | 164 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((#‘𝐴) ∈
(1...(#‘𝐵)) →
(𝐵 ∈ Word
(Vtx‘𝐺) →
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)})) |
166 | 159, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝐴) ∈
(0...(#‘𝐵)) ∧
(#‘𝐴) ∈ ℕ)
→ (𝐵 ∈ Word
(Vtx‘𝐺) →
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)})) |
167 | 166 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
((#‘𝐴) ∈ ℕ
→ (𝐵 ∈ Word
(Vtx‘𝐺) →
{(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)}))) |
168 | 167 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
((#‘𝐴) ∈
(0...(#‘𝐵)) →
(𝐵 ∈ Word
(Vtx‘𝐺) →
((#‘𝐴) ∈ ℕ
→ {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
169 | 105, 15, 168 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) ∈ ℕ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
170 | 143, 169 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((#‘𝐴) ∈
ℙ → (𝑐 ∈
𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS
‘(𝐵 substr 〈0,
(#‘𝐴)〉)),
((𝐵 substr 〈0,
(#‘𝐴)〉)‘0)})) |
171 | 142, 170 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((#‘𝐴) = 𝑁 → (𝑁 ∈ ℙ → (𝑐 ∈ 𝐶 → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
172 | 171 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
173 | 172 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}))) |
174 | 173 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (𝑁 ∈ ℙ → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
175 | 174 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℙ →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
176 | 175 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) →
(((((((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)})) |
177 | 176 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → {(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} = {( lastS ‘(𝐵 substr 〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)}) |
178 | 177 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ({(𝐵‘((#‘𝐴) − 1)), (𝐵‘0)} ∈
(Edg‘𝐺) ↔ {(
lastS ‘(𝐵 substr
〈0, (#‘𝐴)〉)), ((𝐵 substr 〈0, (#‘𝐴)〉)‘0)} ∈ (Edg‘𝐺))) |
179 | 139, 178 | 3anbi23d 1402 |
. . . . . . . . . . . . . . . . . . . . . . 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‘𝐺)))) |
180 | 104, 179 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 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‘𝐺))) |
181 | | 3simpc 1060 |
. . . . . . . . . . . . . . . . . . . . . 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‘𝐺))) |
182 | 180, 181 | 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‘𝐺))) |
183 | | 3anass 1042 |
. . . . . . . . . . . . . . . . . . . . 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‘𝐺)))) |
184 | 53, 182, 183 | sylanbrc 698 |
. . . . . . . . . . . . . . . . . . . 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‘𝐺))) |
185 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
186 | 7, 185 | isclwwlks 26880 |
. . . . . . . . . . . . . . . . . . . 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‘𝐺))) |
187 | 184, 186 | sylibr 224 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalks‘𝐺)) |
188 | 134 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 ↔ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
189 | 188 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
190 | 189 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
191 | 190 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁) |
192 | 191 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁) |
193 | 187, 192 | jca 554 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalks‘𝐺) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁)) |
194 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → 𝑁 ∈ ℕ) |
195 | | isclwwlksn 26882 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalks‘𝐺) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁))) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝐵 substr 〈0, (#‘𝐴)〉) ∈ (ClWWalks‘𝐺) ∧ (#‘(𝐵 substr 〈0, (#‘𝐴)〉)) = 𝑁))) |
197 | 193, 196 | mpbird 247 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) ∧ 𝑐 ∈ 𝐶) ∧ (𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ)) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)) |
198 | 197 | exp31 630 |
. . . . . . . . . . . . . . . 16
⊢
((((((#‘𝐴)
∈ ℕ0 ∧ 𝐴 ∈ Word dom (iEdg‘𝐺)) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ (∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴)))) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
199 | 198 | exp41 638 |
. . . . . . . . . . . . . . 15
⊢
(((#‘𝐴) ∈
ℕ0 ∧ 𝐴
∈ Word dom (iEdg‘𝐺)) → (𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))))) |
200 | 13, 199 | mpancom 703 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ Word dom
(iEdg‘𝐺) →
(𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))))) |
201 | 200 | imp 445 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) → ((∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))))) |
202 | 201 | 3impib 1262 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
203 | 202 | com12 32 |
. . . . . . . . . . 11
⊢
((#‘𝐴) = 𝑁 → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
204 | 203 | com14 96 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (((𝐴 ∈ Word dom
(iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
205 | 204 | adantr 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (((𝐴 ∈ Word dom (iEdg‘𝐺) ∧ 𝐵:(0...(#‘𝐴))⟶(Vtx‘𝐺)) ∧ ∀𝑖 ∈ (0..^(#‘𝐴))((iEdg‘𝐺)‘(𝐴‘𝑖)) = {(𝐵‘𝑖), (𝐵‘(𝑖 + 1))} ∧ (𝐵‘0) = (𝐵‘(#‘𝐴))) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
206 | 12, 205 | mpd 15 |
. . . . . . . 8
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ (ClWalks‘𝐺)) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
207 | 206 | expcom 451 |
. . . . . . 7
⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝑐 ∈ 𝐶 → ((#‘𝐴) = 𝑁 → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
208 | 207 | com24 95 |
. . . . . 6
⊢ (𝑐 ∈ (ClWalks‘𝐺) → ((#‘𝐴) = 𝑁 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))))) |
209 | 208 | imp 445 |
. . . . 5
⊢ ((𝑐 ∈ (ClWalks‘𝐺) ∧ (#‘𝐴) = 𝑁) → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
210 | 2, 209 | sylbi 207 |
. . . 4
⊢ (𝑐 ∈ 𝐶 → (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)))) |
211 | 210 | pm2.43i 52 |
. . 3
⊢ (𝑐 ∈ 𝐶 → ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺))) |
212 | 211 | impcom 446 |
. 2
⊢ (((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) ∧ 𝑐 ∈ 𝐶) → (𝐵 substr 〈0, (#‘𝐴)〉) ∈ (𝑁 ClWWalksN 𝐺)) |
213 | 212, 14 | fmptd 6385 |
1
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺)) |