Proof of Theorem usgrgt2cycl
| Step | Hyp | Ref
| Expression |
| 1 | | cycliswlk 29818 |
. . . . . . . 8
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) |
| 2 | | wlkcl 29633 |
. . . . . . . 8
⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
| 3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝐹(Cycles‘𝐺)𝑃 → (♯‘𝐹) ∈
ℕ0) |
| 4 | 3 | nn0red 12588 |
. . . . . 6
⊢ (𝐹(Cycles‘𝐺)𝑃 → (♯‘𝐹) ∈ ℝ) |
| 5 | 4 | adantr 480 |
. . . . 5
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ∈
ℝ) |
| 6 | 2 | nn0ge0d 12590 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 0 ≤ (♯‘𝐹)) |
| 7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝐹(Cycles‘𝐺)𝑃 → 0 ≤ (♯‘𝐹)) |
| 8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 0 ≤
(♯‘𝐹)) |
| 9 | | relwlk 29644 |
. . . . . . . 8
⊢ Rel
(Walks‘𝐺) |
| 10 | 9 | brrelex1i 5741 |
. . . . . . 7
⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ V) |
| 11 | | hasheq0 14402 |
. . . . . . . . 9
⊢ (𝐹 ∈ V →
((♯‘𝐹) = 0
↔ 𝐹 =
∅)) |
| 12 | 11 | necon3bid 2985 |
. . . . . . . 8
⊢ (𝐹 ∈ V →
((♯‘𝐹) ≠ 0
↔ 𝐹 ≠
∅)) |
| 13 | 12 | bicomd 223 |
. . . . . . 7
⊢ (𝐹 ∈ V → (𝐹 ≠ ∅ ↔
(♯‘𝐹) ≠
0)) |
| 14 | 1, 10, 13 | 3syl 18 |
. . . . . 6
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹 ≠ ∅ ↔ (♯‘𝐹) ≠ 0)) |
| 15 | 14 | biimpa 476 |
. . . . 5
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ≠ 0) |
| 16 | 5, 8, 15 | ne0gt0d 11398 |
. . . 4
⊢ ((𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 0 <
(♯‘𝐹)) |
| 17 | 16 | 3adant1 1131 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 0 <
(♯‘𝐹)) |
| 18 | | usgrumgr 29198 |
. . . . 5
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UMGraph) |
| 19 | | umgrn1cycl 29827 |
. . . . 5
⊢ ((𝐺 ∈ UMGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 1) |
| 20 | 18, 19 | sylan 580 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 1) |
| 21 | 20 | 3adant3 1133 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ≠ 1) |
| 22 | | 0nn0 12541 |
. . . . . 6
⊢ 0 ∈
ℕ0 |
| 23 | | nn0ltp1ne 35117 |
. . . . . 6
⊢ ((0
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) → ((0 +
1) < (♯‘𝐹)
↔ (0 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ (0 + 1)))) |
| 24 | 22, 3, 23 | sylancr 587 |
. . . . 5
⊢ (𝐹(Cycles‘𝐺)𝑃 → ((0 + 1) < (♯‘𝐹) ↔ (0 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (0 +
1)))) |
| 25 | | 0p1e1 12388 |
. . . . . 6
⊢ (0 + 1) =
1 |
| 26 | 25 | breq1i 5150 |
. . . . 5
⊢ ((0 + 1)
< (♯‘𝐹)
↔ 1 < (♯‘𝐹)) |
| 27 | 25 | neeq2i 3006 |
. . . . . 6
⊢
((♯‘𝐹)
≠ (0 + 1) ↔ (♯‘𝐹) ≠ 1) |
| 28 | 27 | anbi2i 623 |
. . . . 5
⊢ ((0 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (0 +
1)) ↔ (0 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ 1)) |
| 29 | 24, 26, 28 | 3bitr3g 313 |
. . . 4
⊢ (𝐹(Cycles‘𝐺)𝑃 → (1 < (♯‘𝐹) ↔ (0 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠
1))) |
| 30 | 29 | 3ad2ant2 1135 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (1 <
(♯‘𝐹) ↔ (0
< (♯‘𝐹)
∧ (♯‘𝐹)
≠ 1))) |
| 31 | 17, 21, 30 | mpbir2and 713 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 1 <
(♯‘𝐹)) |
| 32 | | usgrn2cycl 29829 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 2) |
| 33 | 32 | 3adant3 1133 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (♯‘𝐹) ≠ 2) |
| 34 | | df-2 12329 |
. . . . . 6
⊢ 2 = (1 +
1) |
| 35 | 34 | breq1i 5150 |
. . . . 5
⊢ (2 <
(♯‘𝐹) ↔ (1
+ 1) < (♯‘𝐹)) |
| 36 | | 1nn0 12542 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
| 37 | | nn0ltp1ne 35117 |
. . . . . 6
⊢ ((1
∈ ℕ0 ∧ (♯‘𝐹) ∈ ℕ0) → ((1 +
1) < (♯‘𝐹)
↔ (1 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ (1 + 1)))) |
| 38 | 36, 3, 37 | sylancr 587 |
. . . . 5
⊢ (𝐹(Cycles‘𝐺)𝑃 → ((1 + 1) < (♯‘𝐹) ↔ (1 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (1 +
1)))) |
| 39 | 35, 38 | bitrid 283 |
. . . 4
⊢ (𝐹(Cycles‘𝐺)𝑃 → (2 < (♯‘𝐹) ↔ (1 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ (1 +
1)))) |
| 40 | 39 | 3ad2ant2 1135 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (2 <
(♯‘𝐹) ↔ (1
< (♯‘𝐹)
∧ (♯‘𝐹)
≠ (1 + 1)))) |
| 41 | 34 | neeq2i 3006 |
. . . 4
⊢
((♯‘𝐹)
≠ 2 ↔ (♯‘𝐹) ≠ (1 + 1)) |
| 42 | 41 | anbi2i 623 |
. . 3
⊢ ((1 <
(♯‘𝐹) ∧
(♯‘𝐹) ≠ 2)
↔ (1 < (♯‘𝐹) ∧ (♯‘𝐹) ≠ (1 + 1))) |
| 43 | 40, 42 | bitr4di 289 |
. 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → (2 <
(♯‘𝐹) ↔ (1
< (♯‘𝐹)
∧ (♯‘𝐹)
≠ 2))) |
| 44 | 31, 33, 43 | mpbir2and 713 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ 𝐹 ≠ ∅) → 2 <
(♯‘𝐹)) |