Step | Hyp | Ref
| Expression |
1 | | 2a1 28 |
. 2
⊢ (2 ≤
(#‘𝑃) → (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))) |
2 | | clwwlkprop 26298 |
. . . 4
⊢ (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉)) |
3 | | lencl 13179 |
. . . . . 6
⊢ (𝑃 ∈ Word 𝑉 → (#‘𝑃) ∈
ℕ0) |
4 | | nn0re 11178 |
. . . . . . . . 9
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℝ) |
5 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℝ) |
7 | 4, 6 | ltnled 10063 |
. . . . . . . 8
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) < 2 ↔ ¬ 2 ≤ (#‘𝑃))) |
8 | | nn0lt2 11317 |
. . . . . . . . . 10
⊢
(((#‘𝑃) ∈
ℕ0 ∧ (#‘𝑃) < 2) → ((#‘𝑃) = 0 ∨ (#‘𝑃) = 1)) |
9 | | usgrav 25867 |
. . . . . . . . . . . . 13
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
10 | | isclwwlk 26296 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) ↔ (𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸))) |
11 | | lsw 13204 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ Word 𝑉 → ( lastS ‘𝑃) = (𝑃‘((#‘𝑃) − 1))) |
12 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) = 0
→ ((#‘𝑃) −
1) = (0 − 1)) |
13 | 12 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) = 0
→ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘(0 − 1))) |
14 | 11, 13 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 0) → ( lastS ‘𝑃) = (𝑃‘(0 − 1))) |
15 | 14 | preq1d 4218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 0) → {( lastS ‘𝑃), (𝑃‘0)} = {(𝑃‘(0 − 1)), (𝑃‘0)}) |
16 | | hasheq0 13015 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = 0 ↔ 𝑃 = ∅)) |
17 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 = ∅ → (𝑃‘(0 − 1)) =
(∅‘(0 − 1))) |
18 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 = ∅ → (𝑃‘0) =
(∅‘0)) |
19 | 17, 18 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃 = ∅ → {(𝑃‘(0 − 1)), (𝑃‘0)} = {(∅‘(0
− 1)), (∅‘0)}) |
20 | | 0fv 6137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∅‘(0 − 1)) = ∅ |
21 | | 0fv 6137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∅‘0) = ∅ |
22 | 20, 21 | preq12i 4217 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
{(∅‘(0 − 1)), (∅‘0)} = {∅,
∅} |
23 | 19, 22 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃 = ∅ → {(𝑃‘(0 − 1)), (𝑃‘0)} = {∅,
∅}) |
24 | 16, 23 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ Word 𝑉 → ((#‘𝑃) = 0 → {(𝑃‘(0 − 1)), (𝑃‘0)} = {∅,
∅})) |
25 | 24 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 0) → {(𝑃‘(0 − 1)), (𝑃‘0)} = {∅,
∅}) |
26 | 15, 25 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 0) → {( lastS ‘𝑃), (𝑃‘0)} = {∅,
∅}) |
27 | 26 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 0) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 ↔ {∅, ∅} ∈ ran 𝐸)) |
28 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ∅ =
∅ |
29 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 USGrph 𝐸 ∧ {∅, ∅} ∈ ran 𝐸) → ∅ ≠
∅) |
30 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∅
= ∅ → (∅ ≠ ∅ → 2 ≤ (#‘𝑃))) |
31 | 28, 29, 30 | mpsyl 66 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 USGrph 𝐸 ∧ {∅, ∅} ∈ ran 𝐸) → 2 ≤ (#‘𝑃)) |
32 | 31 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢
({∅, ∅} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → 2 ≤ (#‘𝑃))) |
33 | 27, 32 | syl6bi 242 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 0) → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → 2 ≤ (#‘𝑃)))) |
34 | 33 | impancom 455 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((#‘𝑃) = 0 → (𝑉 USGrph 𝐸 → 2 ≤ (#‘𝑃)))) |
35 | 34 | 3adant2 1073 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → ((#‘𝑃) = 0 → (𝑉 USGrph 𝐸 → 2 ≤ (#‘𝑃)))) |
36 | 10, 35 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → ((#‘𝑃) = 0 → (𝑉 USGrph 𝐸 → 2 ≤ (#‘𝑃))))) |
37 | 36 | com24 93 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 USGrph 𝐸 → ((#‘𝑃) = 0 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃))))) |
38 | 9, 37 | mpcom 37 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → ((#‘𝑃) = 0 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))) |
39 | 38 | com12 32 |
. . . . . . . . . . 11
⊢
((#‘𝑃) = 0
→ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))) |
40 | 11 | preq1d 4218 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Word 𝑉 → {( lastS ‘𝑃), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 1)), (𝑃‘0)}) |
41 | 40 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((#‘𝑃) − 1)), (𝑃‘0)} ∈ ran 𝐸)) |
42 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝑃) = 1
→ ((#‘𝑃) −
1) = (1 − 1)) |
43 | 42 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝑃) = 1
→ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘(1 − 1))) |
44 | | 1m1e0 10966 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1
− 1) = 0 |
45 | 44 | fveq2i 6106 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑃‘(1 − 1)) = (𝑃‘0) |
46 | 43, 45 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝑃) = 1
→ (𝑃‘((#‘𝑃) − 1)) = (𝑃‘0)) |
47 | 46 | preq1d 4218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝑃) = 1
→ {(𝑃‘((#‘𝑃) − 1)), (𝑃‘0)} = {(𝑃‘0), (𝑃‘0)}) |
48 | 47 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝑃) = 1
→ ({(𝑃‘((#‘𝑃) − 1)), (𝑃‘0)} ∈ ran 𝐸 ↔ {(𝑃‘0), (𝑃‘0)} ∈ ran 𝐸)) |
49 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑃‘0) = (𝑃‘0) |
50 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑃‘0), (𝑃‘0)} ∈ ran 𝐸) → (𝑃‘0) ≠ (𝑃‘0)) |
51 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑃‘0) = (𝑃‘0) → ((𝑃‘0) ≠ (𝑃‘0) → (𝑃 ∈ Word 𝑉 → 2 ≤ (#‘𝑃)))) |
52 | 49, 50, 51 | mpsyl 66 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑉 USGrph 𝐸 ∧ {(𝑃‘0), (𝑃‘0)} ∈ ran 𝐸) → (𝑃 ∈ Word 𝑉 → 2 ≤ (#‘𝑃))) |
53 | 52 | expcom 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({(𝑃‘0), (𝑃‘0)} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → (𝑃 ∈ Word 𝑉 → 2 ≤ (#‘𝑃)))) |
54 | 48, 53 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑃) = 1
→ ({(𝑃‘((#‘𝑃) − 1)), (𝑃‘0)} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → (𝑃 ∈ Word 𝑉 → 2 ≤ (#‘𝑃))))) |
55 | 54 | com14 94 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ Word 𝑉 → ({(𝑃‘((#‘𝑃) − 1)), (𝑃‘0)} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → ((#‘𝑃) = 1 → 2 ≤ (#‘𝑃))))) |
56 | 41, 55 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ Word 𝑉 → ({( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸 → (𝑉 USGrph 𝐸 → ((#‘𝑃) = 1 → 2 ≤ (#‘𝑃))))) |
57 | 56 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 ∈ Word 𝑉 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → ((#‘𝑃) = 1 → 2 ≤ (#‘𝑃)))) |
58 | 57 | 3adant2 1073 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸) → (𝑉 USGrph 𝐸 → ((#‘𝑃) = 1 → 2 ≤ (#‘𝑃)))) |
59 | 10, 58 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 USGrph 𝐸 → ((#‘𝑃) = 1 → 2 ≤ (#‘𝑃))))) |
60 | 59 | com23 84 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → ((#‘𝑃) = 1 → 2 ≤ (#‘𝑃))))) |
61 | 9, 60 | mpcom 37 |
. . . . . . . . . . . 12
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → ((#‘𝑃) = 1 → 2 ≤ (#‘𝑃)))) |
62 | 61 | com3r 85 |
. . . . . . . . . . 11
⊢
((#‘𝑃) = 1
→ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))) |
63 | 39, 62 | jaoi 393 |
. . . . . . . . . 10
⊢
(((#‘𝑃) = 0
∨ (#‘𝑃) = 1)
→ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))) |
64 | 8, 63 | syl 17 |
. . . . . . . . 9
⊢
(((#‘𝑃) ∈
ℕ0 ∧ (#‘𝑃) < 2) → (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))) |
65 | 64 | ex 449 |
. . . . . . . 8
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) < 2 → (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃))))) |
66 | 7, 65 | sylbird 249 |
. . . . . . 7
⊢
((#‘𝑃) ∈
ℕ0 → (¬ 2 ≤ (#‘𝑃) → (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃))))) |
67 | 66 | com24 93 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ0 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 USGrph 𝐸 → (¬ 2 ≤ (#‘𝑃) → 2 ≤ (#‘𝑃))))) |
68 | 3, 67 | syl 17 |
. . . . 5
⊢ (𝑃 ∈ Word 𝑉 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 USGrph 𝐸 → (¬ 2 ≤ (#‘𝑃) → 2 ≤ (#‘𝑃))))) |
69 | 68 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V ∧ 𝑃 ∈ Word 𝑉) → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 USGrph 𝐸 → (¬ 2 ≤ (#‘𝑃) → 2 ≤ (#‘𝑃))))) |
70 | 2, 69 | mpcom 37 |
. . 3
⊢ (𝑃 ∈ (𝑉 ClWWalks 𝐸) → (𝑉 USGrph 𝐸 → (¬ 2 ≤ (#‘𝑃) → 2 ≤ (#‘𝑃)))) |
71 | 70 | com13 86 |
. 2
⊢ (¬ 2
≤ (#‘𝑃) →
(𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃)))) |
72 | 1, 71 | pm2.61i 175 |
1
⊢ (𝑉 USGrph 𝐸 → (𝑃 ∈ (𝑉 ClWWalks 𝐸) → 2 ≤ (#‘𝑃))) |