Proof of Theorem usgrgt2cycl
Step | Hyp | Ref
| Expression |
1 | | cycliswlk 27890 |
. . . . . . . 8
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
2 | | wlkcl 27708 |
. . . . . . . 8
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝐹(Cycles‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
4 | 3 | nn0red 12156 |
. . . . . 6
⊢ (𝐹(Cycles‘𝐺)𝑃 → (♯‘𝐹) ∈ ℝ) |
5 | 4 | adantr 484 |
. . . . 5
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ∈
ℝ) |
6 | 2 | nn0ge0d 12158 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 0 ≤ (♯‘𝐹)) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝐹(Cycles‘𝐺)𝑃 → 0 ≤ (♯‘𝐹)) |
8 | 7 | adantr 484 |
. . . . 5
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 0 ≤
(♯‘𝐹)) |
9 | | relwlk 27718 |
. . . . . . . 8
⊢ Rel
(Walks‘𝐺) |
10 | 9 | brrelex1i 5610 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ V) |
11 | | hasheq0 13935 |
. . . . . . . . 9
⊢ (𝐹 ∈ V →
((♯‘𝐹) = 0
↔ 𝐹 =
∅)) |
12 | 11 | necon3bid 2985 |
. . . . . . . 8
⊢ (𝐹 ∈ V →
((♯‘𝐹) ≠ 0
↔ 𝐹 ≠
∅)) |
13 | 12 | bicomd 226 |
. . . . . . 7
⊢ (𝐹 ∈ V → (𝐹 ≠ ∅ ↔
(♯‘𝐹) ≠
0)) |
14 | 1, 10, 13 | 3syl 18 |
. . . . . 6
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹 ≠ ∅ ↔ (♯‘𝐹) ≠ 0)) |
15 | 14 | biimpa 480 |
. . . . 5
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ≠ 0) |
16 | 5, 8, 15 | ne0gt0d 10974 |
. . . 4
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 0 <
(♯‘𝐹)) |
17 | 16 | 3adant1 1132 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 0 <
(♯‘𝐹)) |
18 | | usgrumgr 27275 |
. . . . 5
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UMGraph) |
19 | | umgrn1cycl 27896 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 1) |
20 | 18, 19 | sylan 583 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 1) |
21 | 20 | 3adant3 1134 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ≠ 1) |
22 | | 0nn0 12110 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
23 | | nn0ltp1ne 32788 |
. . . . . 6
⊢ ((0
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) → ((0 +
1) < (♯‘𝐹)
↔ (0 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ (0 + 1)))) |
24 | 22, 3, 23 | sylancr 590 |
. . . . 5
⊢ (𝐹(Cycles‘𝐺)𝑃 → ((0 + 1) < (♯‘𝐹) ↔ (0 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (0 +
1)))) |
25 | | 0p1e1 11957 |
. . . . . 6
⊢ (0 + 1) =
1 |
26 | 25 | breq1i 5065 |
. . . . 5
⊢ ((0 + 1)
< (♯‘𝐹)
↔ 1 < (♯‘𝐹)) |
27 | 25 | neeq2i 3006 |
. . . . . 6
⊢
((♯‘𝐹)
≠ (0 + 1) ↔ (♯‘𝐹) ≠ 1) |
28 | 27 | anbi2i 626 |
. . . . 5
⊢ ((0 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (0 +
1)) ↔ (0 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ 1)) |
29 | 24, 26, 28 | 3bitr3g 316 |
. . . 4
⊢ (𝐹(Cycles‘𝐺)𝑃 → (1 < (♯‘𝐹) ↔ (0 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠
1))) |
30 | 29 | 3ad2ant2 1136 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (1 <
(♯‘𝐹) ↔ (0
< (♯‘𝐹)
∧ (♯‘𝐹)
≠ 1))) |
31 | 17, 21, 30 | mpbir2and 713 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 1 <
(♯‘𝐹)) |
32 | | usgrn2cycl 27898 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 2) |
33 | 32 | 3adant3 1134 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ≠ 2) |
34 | | df-2 11898 |
. . . . . 6
⊢ 2 = (1 +
1) |
35 | 34 | breq1i 5065 |
. . . . 5
⊢ (2 <
(♯‘𝐹) ↔ (1
+ 1) < (♯‘𝐹)) |
36 | | 1nn0 12111 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
37 | | nn0ltp1ne 32788 |
. . . . . 6
⊢ ((1
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) → ((1 +
1) < (♯‘𝐹)
↔ (1 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ (1 + 1)))) |
38 | 36, 3, 37 | sylancr 590 |
. . . . 5
⊢ (𝐹(Cycles‘𝐺)𝑃 → ((1 + 1) < (♯‘𝐹) ↔ (1 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (1 +
1)))) |
39 | 35, 38 | syl5bb 286 |
. . . 4
⊢ (𝐹(Cycles‘𝐺)𝑃 → (2 < (♯‘𝐹) ↔ (1 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (1 +
1)))) |
40 | 39 | 3ad2ant2 1136 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (2 <
(♯‘𝐹) ↔ (1
< (♯‘𝐹)
∧ (♯‘𝐹)
≠ (1 + 1)))) |
41 | 34 | neeq2i 3006 |
. . . 4
⊢
((♯‘𝐹)
≠ 2 ↔ (♯‘𝐹) ≠ (1 + 1)) |
42 | 41 | anbi2i 626 |
. . 3
⊢ ((1 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ 2)
↔ (1 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ (1 + 1))) |
43 | 40, 42 | bitr4di 292 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (2 <
(♯‘𝐹) ↔ (1
< (♯‘𝐹)
∧ (♯‘𝐹)
≠ 2))) |
44 | 31, 33, 43 | mpbir2and 713 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 <
(♯‘𝐹)) |