Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2622 |
. . . . . 6
⊢
(Edg‘𝐺) =
(Edg‘𝐺) |
3 | 1, 2 | clwwlknp 26887 |
. . . . 5
⊢ (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑋), (𝑋‘0)} ∈ (Edg‘𝐺))) |
4 | | swrdcl 13419 |
. . . . . . . . . 10
⊢ (𝑋 ∈ Word (Vtx‘𝐺) → (𝑋 substr 〈0, 𝑀〉) ∈ Word (Vtx‘𝐺)) |
5 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) → (𝑋 substr 〈0, 𝑀〉) ∈ Word (Vtx‘𝐺)) |
6 | 5 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 substr 〈0, 𝑀〉) ∈ Word
(Vtx‘𝐺)) |
7 | | nnz 11399 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
8 | | eluzp1m1 11711 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘𝑀)) |
9 | 8 | ex 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℤ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
10 | 7, 9 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘𝑀))) |
11 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
12 | 7, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℤ) |
13 | | nnre 11027 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
14 | 13 | lem1d 10957 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ≤ 𝑀) |
15 | | eluzuzle 11696 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑀 − 1) ∈ ℤ ∧
(𝑀 − 1) ≤ 𝑀) → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) |
16 | 12, 14, 15 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℕ → ((𝑁 − 1) ∈
(ℤ≥‘𝑀) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) |
17 | 10, 16 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)))) |
18 | 17 | imp 445 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1))) |
19 | | fzoss2 12496 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 − 1) ∈
(ℤ≥‘(𝑀 − 1)) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) |
21 | 20 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (0..^(𝑀 − 1)) ⊆ (0..^(𝑁 − 1))) |
22 | | ssralv 3666 |
. . . . . . . . . . . . 13
⊢
((0..^(𝑀 − 1))
⊆ (0..^(𝑁 − 1))
→ (∀𝑖 ∈
(0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
24 | | simpll 790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑋 ∈ Word (Vtx‘𝐺)) |
25 | 24 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑋 ∈ Word (Vtx‘𝐺)) |
26 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) ↔ ((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) |
27 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ∈ ℝ) |
28 | | peano2re 10209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
29 | 13, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ∈ ℕ → (𝑀 + 1) ∈
ℝ) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 + 1) ∈ ℝ) |
31 | | zre 11381 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
32 | 31 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑁 ∈ ℝ) |
33 | 13 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ∈ ℕ → 𝑀 ≤ (𝑀 + 1)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ≤ (𝑀 + 1)) |
35 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 + 1) ≤ 𝑁) |
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 + 1) ≤ 𝑁) |
37 | 27, 30, 32, 34, 36 | letrd 10194 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → 𝑀 ≤ 𝑁) |
38 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℕ0) |
39 | 38 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈
ℕ0) |
40 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℤ) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈ ℤ) |
42 | | 0red 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 0 ∈
ℝ) |
43 | 13 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈
ℝ) |
44 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) |
45 | 42, 43, 44 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑁
∈ ℝ)) |
46 | 45 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
47 | 38 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑀 ∈ ℕ → 0 ≤
𝑀) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → 0 ≤
𝑀) |
49 | 48 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁)) |
50 | | letr 10131 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((0
∈ ℝ ∧ 𝑀
∈ ℝ ∧ 𝑁
∈ ℝ) → ((0 ≤ 𝑀 ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁)) |
51 | 46, 49, 50 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 0 ≤ 𝑁) |
52 | 41, 51 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁)) |
53 | | elnn0z 11390 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℤ
∧ 0 ≤ 𝑁)) |
54 | 52, 53 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈
ℕ0) |
55 | 54 | adantlrr 757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑁 ∈
ℕ0) |
56 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → 𝑀 ≤ 𝑁) |
57 | 39, 55, 56 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) ∧ 𝑀 ≤ 𝑁) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
58 | 37, 57 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 ∈ ℕ ∧ (𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁)) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
59 | 58 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
60 | 59 | 3adant1 1079 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑀 + 1) ≤ 𝑁) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
61 | 26, 60 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈
(ℤ≥‘(𝑀 + 1)) → (𝑀 ∈ ℕ → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁))) |
62 | 61 | impcom 446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
63 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
64 | 62, 63 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → 𝑀 ∈ (0...𝑁)) |
65 | 64 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ∈ (0...𝑁)) |
66 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑋) = 𝑁 → (0...(#‘𝑋)) = (0...𝑁)) |
67 | 66 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑋) = 𝑁 → (𝑀 ∈ (0...(#‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) → (𝑀 ∈ (0...(#‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) |
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑀 ∈ (0...(#‘𝑋)) ↔ 𝑀 ∈ (0...𝑁))) |
70 | 65, 69 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 ∈ (0...(#‘𝑋))) |
71 | 70 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑀 ∈ (0...(#‘𝑋))) |
72 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) ↔ ((𝑀 − 1) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ (𝑀 − 1) ≤ 𝑀)) |
73 | 12, 7, 14, 72 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
(ℤ≥‘(𝑀 − 1))) |
74 | | fzoss2 12496 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈
(ℤ≥‘(𝑀 − 1)) → (0..^(𝑀 − 1)) ⊆ (0..^𝑀)) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ →
(0..^(𝑀 − 1)) ⊆
(0..^𝑀)) |
76 | 75 | sseld 3602 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → (𝑖 ∈ (0..^(𝑀 − 1)) → 𝑖 ∈ (0..^𝑀))) |
77 | 76 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑖 ∈ (0..^(𝑀 − 1)) → 𝑖 ∈ (0..^𝑀))) |
78 | 77 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → 𝑖 ∈ (0..^𝑀)) |
79 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(#‘𝑋)) ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑋 substr 〈0, 𝑀〉)‘𝑖) = (𝑋‘𝑖)) |
80 | 25, 71, 78, 79 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ((𝑋 substr 〈0, 𝑀〉)‘𝑖) = (𝑋‘𝑖)) |
81 | 80 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑋‘𝑖) = ((𝑋 substr 〈0, 𝑀〉)‘𝑖)) |
82 | | fzonn0p1p1 12546 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^((𝑀 − 1) + 1))) |
83 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
84 | | npcan1 10455 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑀 ∈ ℕ → ((𝑀 − 1) + 1) = 𝑀) |
86 | 85 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑀 ∈ ℕ →
(0..^((𝑀 − 1) + 1)) =
(0..^𝑀)) |
87 | 86 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ → ((𝑖 + 1) ∈ (0..^((𝑀 − 1) + 1)) ↔ (𝑖 + 1) ∈ (0..^𝑀))) |
88 | 82, 87 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ → (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^𝑀))) |
89 | 88 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑖 ∈ (0..^(𝑀 − 1)) → (𝑖 + 1) ∈ (0..^𝑀))) |
90 | 89 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑖 + 1) ∈ (0..^𝑀)) |
91 | | swrd0fv 13439 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(#‘𝑋)) ∧ (𝑖 + 1) ∈ (0..^𝑀)) → ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1)) = (𝑋‘(𝑖 + 1))) |
92 | 25, 71, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1)) = (𝑋‘(𝑖 + 1))) |
93 | 92 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → (𝑋‘(𝑖 + 1)) = ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))) |
94 | 81, 93 | preq12d 4276 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → {(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} = {((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))}) |
95 | 94 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) ∧ 𝑖 ∈ (0..^(𝑀 − 1))) → ({(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
96 | 95 | ralbidva 2985 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑀 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
97 | 23, 96 | sylibd 229 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
98 | 97 | impancom 456 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
99 | 98 | imp 445 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
100 | 24, 70 | jca 554 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(#‘𝑋)))) |
101 | 100 | adantlr 751 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(#‘𝑋)))) |
102 | | swrd0len 13422 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Word (Vtx‘𝐺) ∧ 𝑀 ∈ (0...(#‘𝑋))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = 𝑀) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = 𝑀) |
104 | 103 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ((#‘(𝑋 substr 〈0, 𝑀〉)) − 1) = (𝑀 − 1)) |
105 | 104 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) →
(0..^((#‘(𝑋 substr
〈0, 𝑀〉)) −
1)) = (0..^(𝑀 −
1))) |
106 | 105 | raleqdv 3144 |
. . . . . . . . 9
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^(𝑀 − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺))) |
107 | 99, 106 | mpbird 247 |
. . . . . . . 8
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺)) |
108 | 24, 70, 102 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = 𝑀) |
109 | 85 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 = ((𝑀 − 1) + 1)) |
110 | 109 | ad2antrl 764 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → 𝑀 = ((𝑀 − 1) + 1)) |
111 | 108, 110 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)) |
112 | 111 | adantlr 751 |
. . . . . . . 8
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)) |
113 | 6, 107, 112 | 3jca 1242 |
. . . . . . 7
⊢ ((((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))) → ((𝑋 substr 〈0, 𝑀〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑋 substr
〈0, 𝑀〉)) −
1)){((𝑋 substr 〈0,
𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1))) |
114 | 113 | ex 450 |
. . . . . 6
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺)) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑋 substr 〈0, 𝑀〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑋 substr
〈0, 𝑀〉)) −
1)){((𝑋 substr 〈0,
𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
115 | 114 | 3adant3 1081 |
. . . . 5
⊢ (((𝑋 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑋) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑋‘𝑖), (𝑋‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {( lastS ‘𝑋), (𝑋‘0)} ∈ (Edg‘𝐺)) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑋 substr 〈0, 𝑀〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑋 substr
〈0, 𝑀〉)) −
1)){((𝑋 substr 〈0,
𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
116 | 3, 115 | syl 17 |
. . . 4
⊢ (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → ((𝑋 substr 〈0, 𝑀〉) ∈ Word
(Vtx‘𝐺) ∧
∀𝑖 ∈
(0..^((#‘(𝑋 substr
〈0, 𝑀〉)) −
1)){((𝑋 substr 〈0,
𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
117 | 116 | impcom 446 |
. . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → ((𝑋 substr 〈0, 𝑀〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1))) |
118 | | nnm1nn0 11334 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (𝑀 − 1) ∈
ℕ0) |
119 | 118 | ad2antrr 762 |
. . . 4
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑀 − 1) ∈
ℕ0) |
120 | 1, 2 | iswwlksnx 26731 |
. . . 4
⊢ ((𝑀 − 1) ∈
ℕ0 → ((𝑋 substr 〈0, 𝑀〉) ∈ ((𝑀 − 1) WWalksN 𝐺) ↔ ((𝑋 substr 〈0, 𝑀〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
121 | 119, 120 | syl 17 |
. . 3
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → ((𝑋 substr 〈0, 𝑀〉) ∈ ((𝑀 − 1) WWalksN 𝐺) ↔ ((𝑋 substr 〈0, 𝑀〉) ∈ Word (Vtx‘𝐺) ∧ ∀𝑖 ∈ (0..^((#‘(𝑋 substr 〈0, 𝑀〉)) − 1)){((𝑋 substr 〈0, 𝑀〉)‘𝑖), ((𝑋 substr 〈0, 𝑀〉)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ (#‘(𝑋 substr 〈0, 𝑀〉)) = ((𝑀 − 1) + 1)))) |
122 | 117, 121 | mpbird 247 |
. 2
⊢ (((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) ∧ 𝑋 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑋 substr 〈0, 𝑀〉) ∈ ((𝑀 − 1) WWalksN 𝐺)) |
123 | 122 | ex 450 |
1
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘(𝑀 + 1))) → (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → (𝑋 substr 〈0, 𝑀〉) ∈ ((𝑀 − 1) WWalksN 𝐺))) |