Metamath Proof Explorer

Theorem usgrgt2cycl

Description: A non-trivial cycle in a simple graph has a length greater than 2. (Contributed by BTernaryTau, 24-Sep-2023)

Ref Expression
Assertion usgrgt2cycl ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 < ( ♯ ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 cycliswlk ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
2 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
3 1 2 syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
4 3 nn0red ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℝ )
5 4 adantr ⊢ ( ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ∈ ℝ )
6 2 nn0ge0d ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 0 ≤ ( ♯ ‘ 𝐹 ) )
7 1 6 syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → 0 ≤ ( ♯ ‘ 𝐹 ) )
8 7 adantr ⊢ ( ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 0 ≤ ( ♯ ‘ 𝐹 ) )
9 relwlk ⊢ Rel ( Walks ‘ 𝐺 )
10 9 brrelex1i ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ V )
11 hasheq0 ⊢ ( 𝐹 ∈ V → ( ( ♯ ‘ 𝐹 ) = 0 ↔ 𝐹 = ∅ ) )
12 11 necon3bid ⊢ ( 𝐹 ∈ V → ( ( ♯ ‘ 𝐹 ) ≠ 0 ↔ 𝐹 ≠ ∅ ) )
13 12 bicomd ⊢ ( 𝐹 ∈ V → ( 𝐹 ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ≠ 0 ) )
14 1 10 13 3syl ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐹 ≠ ∅ ↔ ( ♯ ‘ 𝐹 ) ≠ 0 ) )
15 14 biimpa ⊢ ( ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ≠ 0 )
16 5 8 15 ne0gt0d ⊢ ( ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐹 ) )
17 16 3adant1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 0 < ( ♯ ‘ 𝐹 ) )
18 usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
19 umgrn1cycl ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 1 )
20 18 19 sylan ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 1 )
21 20 3adant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ≠ 1 )
22 0nn0 ⊢ 0 ∈ ℕ0
23 nn0ltp1ne ⊢ ( ( 0 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( 0 + 1 ) < ( ♯ ‘ 𝐹 ) ↔ ( 0 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 0 + 1 ) ) ) )
24 22 3 23 sylancr ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ( 0 + 1 ) < ( ♯ ‘ 𝐹 ) ↔ ( 0 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 0 + 1 ) ) ) )
25 0p1e1 ⊢ ( 0 + 1 ) = 1
26 25 breq1i ⊢ ( ( 0 + 1 ) < ( ♯ ‘ 𝐹 ) ↔ 1 < ( ♯ ‘ 𝐹 ) )
27 25 neeq2i ⊢ ( ( ♯ ‘ 𝐹 ) ≠ ( 0 + 1 ) ↔ ( ♯ ‘ 𝐹 ) ≠ 1 )
28 27 anbi2i ⊢ ( ( 0 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 0 + 1 ) ) ↔ ( 0 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 1 ) )
29 24 26 28 3bitr3g ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 1 < ( ♯ ‘ 𝐹 ) ↔ ( 0 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 1 ) ) )
30 29 3ad2ant2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( 1 < ( ♯ ‘ 𝐹 ) ↔ ( 0 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 1 ) ) )
31 17 21 30 mpbir2and ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 1 < ( ♯ ‘ 𝐹 ) )
32 usgrn2cycl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 2 )
33 32 3adant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ≠ 2 )
34 df-2 ⊢ 2 = ( 1 + 1 )
35 34 breq1i ⊢ ( 2 < ( ♯ ‘ 𝐹 ) ↔ ( 1 + 1 ) < ( ♯ ‘ 𝐹 ) )
36 1nn0 ⊢ 1 ∈ ℕ0
37 nn0ltp1ne ⊢ ( ( 1 ∈ ℕ0 ∧ ( ♯ ‘ 𝐹 ) ∈ ℕ0 ) → ( ( 1 + 1 ) < ( ♯ ‘ 𝐹 ) ↔ ( 1 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 1 + 1 ) ) ) )
38 36 3 37 sylancr ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ( 1 + 1 ) < ( ♯ ‘ 𝐹 ) ↔ ( 1 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 1 + 1 ) ) ) )
39 35 38 syl5bb ⊢ ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 2 < ( ♯ ‘ 𝐹 ) ↔ ( 1 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 1 + 1 ) ) ) )
40 39 3ad2ant2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( 2 < ( ♯ ‘ 𝐹 ) ↔ ( 1 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 1 + 1 ) ) ) )
41 34 neeq2i ⊢ ( ( ♯ ‘ 𝐹 ) ≠ 2 ↔ ( ♯ ‘ 𝐹 ) ≠ ( 1 + 1 ) )
42 41 anbi2i ⊢ ( ( 1 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 2 ) ↔ ( 1 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ ( 1 + 1 ) ) )
43 40 42 bitr4di ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → ( 2 < ( ♯ ‘ 𝐹 ) ↔ ( 1 < ( ♯ ‘ 𝐹 ) ∧ ( ♯ ‘ 𝐹 ) ≠ 2 ) ) )
44 31 33 43 mpbir2and ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ 𝐹 ≠ ∅ ) → 2 < ( ♯ ‘ 𝐹 ) )