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 \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to 2 < \|F\|$

Proof

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

Metamath Proof Explorer

Theorem usgrgt2cycl

Proof