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 
|- ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 < ( # ` F ) )

Proof

Step Hyp Ref Expression
1 cycliswlk 
 |-  ( F ( Cycles ` G ) P -> F ( Walks ` G ) P )
2 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
3 1 2 syl 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) e. NN0 )
4 3 nn0red 
 |-  ( F ( Cycles ` G ) P -> ( # ` F ) e. RR )
5 4 adantr 
 |-  ( ( F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) e. RR )
6 2 nn0ge0d 
 |-  ( F ( Walks ` G ) P -> 0 <_ ( # ` F ) )
7 1 6 syl 
 |-  ( F ( Cycles ` G ) P -> 0 <_ ( # ` F ) )
8 7 adantr 
 |-  ( ( F ( Cycles ` G ) P /\ F =/= (/) ) -> 0 <_ ( # ` F ) )
9 relwlk 
 |-  Rel ( Walks ` G )
10 9 brrelex1i 
 |-  ( F ( Walks ` G ) P -> F e. _V )
11 hasheq0 
 |-  ( F e. _V -> ( ( # ` F ) = 0 <-> F = (/) ) )
12 11 necon3bid 
 |-  ( F e. _V -> ( ( # ` F ) =/= 0 <-> F =/= (/) ) )
13 12 bicomd 
 |-  ( F e. _V -> ( F =/= (/) <-> ( # ` F ) =/= 0 ) )
14 1 10 13 3syl 
 |-  ( F ( Cycles ` G ) P -> ( F =/= (/) <-> ( # ` F ) =/= 0 ) )
15 14 biimpa 
 |-  ( ( F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) =/= 0 )
16 5 8 15 ne0gt0d 
 |-  ( ( F ( Cycles ` G ) P /\ F =/= (/) ) -> 0 < ( # ` F ) )
17 16 3adant1 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 0 < ( # ` F ) )
18 usgrumgr 
 |-  ( G e. USGraph -> G e. UMGraph )
19 umgrn1cycl 
 |-  ( ( G e. UMGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 1 )
20 18 19 sylan 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 1 )
21 20 3adant3 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) =/= 1 )
22 0nn0 
 |-  0 e. NN0
23 nn0ltp1ne 
 |-  ( ( 0 e. NN0 /\ ( # ` F ) e. NN0 ) -> ( ( 0 + 1 ) < ( # ` F ) <-> ( 0 < ( # ` F ) /\ ( # ` F ) =/= ( 0 + 1 ) ) ) )
24 22 3 23 sylancr 
 |-  ( F ( Cycles ` G ) P -> ( ( 0 + 1 ) < ( # ` F ) <-> ( 0 < ( # ` F ) /\ ( # ` F ) =/= ( 0 + 1 ) ) ) )
25 0p1e1 
 |-  ( 0 + 1 ) = 1
26 25 breq1i 
 |-  ( ( 0 + 1 ) < ( # ` F ) <-> 1 < ( # ` F ) )
27 25 neeq2i 
 |-  ( ( # ` F ) =/= ( 0 + 1 ) <-> ( # ` F ) =/= 1 )
28 27 anbi2i 
 |-  ( ( 0 < ( # ` F ) /\ ( # ` F ) =/= ( 0 + 1 ) ) <-> ( 0 < ( # ` F ) /\ ( # ` F ) =/= 1 ) )
29 24 26 28 3bitr3g 
 |-  ( F ( Cycles ` G ) P -> ( 1 < ( # ` F ) <-> ( 0 < ( # ` F ) /\ ( # ` F ) =/= 1 ) ) )
30 29 3ad2ant2 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( 1 < ( # ` F ) <-> ( 0 < ( # ` F ) /\ ( # ` F ) =/= 1 ) ) )
31 17 21 30 mpbir2and 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 1 < ( # ` F ) )
32 usgrn2cycl 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P ) -> ( # ` F ) =/= 2 )
33 32 3adant3 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( # ` F ) =/= 2 )
34 df-2 
 |-  2 = ( 1 + 1 )
35 34 breq1i 
 |-  ( 2 < ( # ` F ) <-> ( 1 + 1 ) < ( # ` F ) )
36 1nn0 
 |-  1 e. NN0
37 nn0ltp1ne 
 |-  ( ( 1 e. NN0 /\ ( # ` F ) e. NN0 ) -> ( ( 1 + 1 ) < ( # ` F ) <-> ( 1 < ( # ` F ) /\ ( # ` F ) =/= ( 1 + 1 ) ) ) )
38 36 3 37 sylancr 
 |-  ( F ( Cycles ` G ) P -> ( ( 1 + 1 ) < ( # ` F ) <-> ( 1 < ( # ` F ) /\ ( # ` F ) =/= ( 1 + 1 ) ) ) )
39 35 38 syl5bb 
 |-  ( F ( Cycles ` G ) P -> ( 2 < ( # ` F ) <-> ( 1 < ( # ` F ) /\ ( # ` F ) =/= ( 1 + 1 ) ) ) )
40 39 3ad2ant2 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( 2 < ( # ` F ) <-> ( 1 < ( # ` F ) /\ ( # ` F ) =/= ( 1 + 1 ) ) ) )
41 34 neeq2i 
 |-  ( ( # ` F ) =/= 2 <-> ( # ` F ) =/= ( 1 + 1 ) )
42 41 anbi2i 
 |-  ( ( 1 < ( # ` F ) /\ ( # ` F ) =/= 2 ) <-> ( 1 < ( # ` F ) /\ ( # ` F ) =/= ( 1 + 1 ) ) )
43 40 42 bitr4di 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> ( 2 < ( # ` F ) <-> ( 1 < ( # ` F ) /\ ( # ` F ) =/= 2 ) ) )
44 31 33 43 mpbir2and 
 |-  ( ( G e. USGraph /\ F ( Cycles ` G ) P /\ F =/= (/) ) -> 2 < ( # ` F ) )