Step | Hyp | Ref
| Expression |
1 | | cycliswlk 26160 |
. . 3
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
2 | | wlkbprop 26051 |
. . . 4
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | | iscycl 26153 |
. . . . . 6
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
4 | 3 | 3adant1 1072 |
. . . . 5
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
5 | | pthistrl 26102 |
. . . . . . . 8
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → 𝐹(𝑉 Trails 𝐸)𝑃) |
6 | | trliswlk 26069 |
. . . . . . . 8
⊢ (𝐹(𝑉 Trails 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
7 | 5, 6 | syl 17 |
. . . . . . 7
⊢ (𝐹(𝑉 Paths 𝐸)𝑃 → 𝐹(𝑉 Walks 𝐸)𝑃) |
8 | | usgrwlknloop 26093 |
. . . . . . . . . . 11
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) |
9 | | nne 2786 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(#‘𝐹) ≠ 1 ↔
(#‘𝐹) =
1) |
10 | | 0z 11265 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 ∈
ℤ |
11 | | 1z 11284 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 1 ∈
ℤ |
12 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 0 <
1 |
13 | | fzolb 12345 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (0 ∈
(0..^1) ↔ (0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 0 <
1)) |
14 | 10, 11, 12, 13 | mpbir3an 1237 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 0 ∈
(0..^1) |
15 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((#‘𝐹) = 1
→ (0..^(#‘𝐹)) =
(0..^1)) |
16 | 14, 15 | syl5eleqr 2695 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((#‘𝐹) = 1
→ 0 ∈ (0..^(#‘𝐹))) |
17 | 16 | anim2i 591 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) = 1) → (∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ 0 ∈ (0..^(#‘𝐹)))) |
18 | 17 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) → ((#‘𝐹) = 1 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ 0 ∈ (0..^(#‘𝐹))))) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0) →
((#‘𝐹) = 1 →
(∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ 0 ∈ (0..^(#‘𝐹))))) |
20 | 19 | impcom 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((#‘𝐹) = 1
∧ (∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0)) →
(∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ 0 ∈ (0..^(#‘𝐹)))) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → (𝑃‘𝑘) = (𝑃‘0)) |
22 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = 0 → (𝑘 + 1) = (0 + 1)) |
23 | 22 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘(0 + 1))) |
24 | 21, 23 | neeq12d 2843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 0 → ((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))) |
25 | 24 | rspccva 3281 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1))) |
26 | 20, 25 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) = 1
∧ (∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0)) → (𝑃‘0) ≠ (𝑃‘(0 +
1))) |
27 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 + 1) =
1 |
28 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 =
(#‘𝐹) → 1 =
(#‘𝐹)) |
29 | 28 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((#‘𝐹) = 1
→ 1 = (#‘𝐹)) |
30 | 27, 29 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐹) = 1
→ (0 + 1) = (#‘𝐹)) |
31 | 30 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐹) = 1
→ (𝑃‘(0 + 1)) =
(𝑃‘(#‘𝐹))) |
32 | 31 | neeq2d 2842 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) = 1
→ ((𝑃‘0) ≠
(𝑃‘(0 + 1)) ↔
(𝑃‘0) ≠ (𝑃‘(#‘𝐹)))) |
33 | | df-ne 2782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃‘0) ≠ (𝑃‘(#‘𝐹)) ↔ ¬ (𝑃‘0) = (𝑃‘(#‘𝐹))) |
34 | 32, 33 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) = 1
→ ((𝑃‘0) ≠
(𝑃‘(0 + 1)) ↔
¬ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
35 | 26, 34 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) = 1
∧ (∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0)) →
((#‘𝐹) = 1 →
¬ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘𝐹) = 1
→ ((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0) →
((#‘𝐹) = 1 →
¬ (𝑃‘0) = (𝑃‘(#‘𝐹))))) |
37 | 36 | pm2.43a 52 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) = 1
→ ((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0) → ¬
(𝑃‘0) = (𝑃‘(#‘𝐹)))) |
38 | 9, 37 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (¬
(#‘𝐹) ≠ 1 →
((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0) → ¬
(𝑃‘0) = (𝑃‘(#‘𝐹)))) |
39 | 38 | com12 32 |
. . . . . . . . . . . . . 14
⊢
((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0) → (¬
(#‘𝐹) ≠ 1 →
¬ (𝑃‘0) = (𝑃‘(#‘𝐹)))) |
40 | 39 | con4d 113 |
. . . . . . . . . . . . 13
⊢
((∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ (#‘𝐹) ∈ ℕ0) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (#‘𝐹) ≠ 1)) |
41 | 40 | ex 449 |
. . . . . . . . . . . 12
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) → ((#‘𝐹) ∈ ℕ0 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (#‘𝐹) ≠ 1))) |
42 | 41 | com23 84 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → ((#‘𝐹) ∈ ℕ0 →
(#‘𝐹) ≠
1))) |
43 | 8, 42 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Walks 𝐸)𝑃) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → ((#‘𝐹) ∈ ℕ0 →
(#‘𝐹) ≠
1))) |
44 | 43 | ex 449 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → ((#‘𝐹) ∈ ℕ0 →
(#‘𝐹) ≠
1)))) |
45 | 44 | com14 94 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
ℕ0 → (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 1)))) |
46 | 45 | 3ad2ant1 1075 |
. . . . . . 7
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Walks 𝐸)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 1)))) |
47 | 7, 46 | syl5 33 |
. . . . . 6
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Paths 𝐸)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 1)))) |
48 | 47 | impd 446 |
. . . . 5
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 1))) |
49 | 4, 48 | sylbid 229 |
. . . 4
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 1))) |
50 | 2, 49 | syl 17 |
. . 3
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 1))) |
51 | 1, 50 | mpcom 37 |
. 2
⊢ (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 1)) |
52 | 51 | impcom 445 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 1) |