frgrogt3nreg

Description: If a finite friendship graph has an order greater than 3, it cannot be k-regular for any k . (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 4-Jun-2021)

		Ref	Expression
	Hypothesis	frgrreggt1.v	$⊢ V = Vtx (G)$
	Assertion	frgrogt3nreg	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to \forall k \in ℕ_{0} \neg G RegUSGraph k$

Proof

Step	Hyp	Ref	Expression
1		frgrreggt1.v	$⊢ V = Vtx (G)$
2		simp1	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to G \in FriendGraph$
3		simp2	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to V \in Fin$
4		hashcl	$⊢ V \in Fin \to \|V\| \in ℕ_{0}$
5		0red	$⊢ \|V\| \in ℕ_{0} \to 0 \in ℝ$
6		3re	$⊢ 3 \in ℝ$
7	6	a1i	$⊢ \|V\| \in ℕ_{0} \to 3 \in ℝ$
8		nn0re	$⊢ \|V\| \in ℕ_{0} \to \|V\| \in ℝ$
9	5 7 8	3jca	$⊢ \|V\| \in ℕ_{0} \to (0 \in ℝ \land 3 \in ℝ \land \|V\| \in ℝ)$
10	9	adantr	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to (0 \in ℝ \land 3 \in ℝ \land \|V\| \in ℝ)$
11		3pos	$⊢ 0 < 3$
12	11	a1i	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to 0 < 3$
13		simpr	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to 3 < \|V\|$
14		lttr	$⊢ (0 \in ℝ \land 3 \in ℝ \land \|V\| \in ℝ) \to ((0 < 3 \land 3 < \|V\|) \to 0 < \|V\|)$
15	14	imp	$⊢ ((0 \in ℝ \land 3 \in ℝ \land \|V\| \in ℝ) \land (0 < 3 \land 3 < \|V\|)) \to 0 < \|V\|$
16	10 12 13 15	syl12anc	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to 0 < \|V\|$
17	16	ex	$⊢ \|V\| \in ℕ_{0} \to (3 < \|V\| \to 0 < \|V\|)$
18		ltne	$⊢ (0 \in ℝ \land 0 < \|V\|) \to \|V\| \neq 0$
19	5 17 18	syl6an	$⊢ \|V\| \in ℕ_{0} \to (3 < \|V\| \to \|V\| \neq 0)$
20		hasheq0	$⊢ V \in Fin \to (\|V\| = 0 \leftrightarrow V = \emptyset)$
21	20	necon3bid	$⊢ V \in Fin \to (\|V\| \neq 0 \leftrightarrow V \neq \emptyset)$
22	21	biimpcd	$⊢ \|V\| \neq 0 \to (V \in Fin \to V \neq \emptyset)$
23	19 22	syl6	$⊢ \|V\| \in ℕ_{0} \to (3 < \|V\| \to (V \in Fin \to V \neq \emptyset))$
24	23	com23	$⊢ \|V\| \in ℕ_{0} \to (V \in Fin \to (3 < \|V\| \to V \neq \emptyset))$
25	4 24	mpcom	$⊢ V \in Fin \to (3 < \|V\| \to V \neq \emptyset)$
26	25	a1i	$⊢ G \in FriendGraph \to (V \in Fin \to (3 < \|V\| \to V \neq \emptyset))$
27	26	3imp	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to V \neq \emptyset$
28	2 3 27	3jca	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to (G \in FriendGraph \land V \in Fin \land V \neq \emptyset)$
29	28	ad2antrl	$⊢ (G RegUSGraph k \land ((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0})) \to (G \in FriendGraph \land V \in Fin \land V \neq \emptyset)$
30		simpl	$⊢ (G RegUSGraph k \land ((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0})) \to G RegUSGraph k$
31	1	frgrregord13	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph k) \to (\|V\| = 1 \lor \|V\| = 3)$
32	29 30 31	syl2anc	$⊢ (G RegUSGraph k \land ((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0})) \to (\|V\| = 1 \lor \|V\| = 3)$
33		1red	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to 1 \in ℝ$
34	6	a1i	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to 3 \in ℝ$
35	8	adantr	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to \|V\| \in ℝ$
36		1lt3	$⊢ 1 < 3$
37	36	a1i	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to 1 < 3$
38	33 34 35 37 13	lttrd	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to 1 < \|V\|$
39	33 38	gtned	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to \|V\| \neq 1$
40		eqneqall	$⊢ \|V\| = 1 \to (\|V\| \neq 1 \to \neg G RegUSGraph k)$
41	39 40	syl5com	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to (\|V\| = 1 \to \neg G RegUSGraph k)$
42		ltne	$⊢ (3 \in ℝ \land 3 < \|V\|) \to \|V\| \neq 3$
43	7 42	sylan	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to \|V\| \neq 3$
44		eqneqall	$⊢ \|V\| = 3 \to (\|V\| \neq 3 \to \neg G RegUSGraph k)$
45	43 44	syl5com	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to (\|V\| = 3 \to \neg G RegUSGraph k)$
46	41 45	jaod	$⊢ (\|V\| \in ℕ_{0} \land 3 < \|V\|) \to ((\|V\| = 1 \lor \|V\| = 3) \to \neg G RegUSGraph k)$
47	46	ex	$⊢ \|V\| \in ℕ_{0} \to (3 < \|V\| \to ((\|V\| = 1 \lor \|V\| = 3) \to \neg G RegUSGraph k))$
48	4 47	syl	$⊢ V \in Fin \to (3 < \|V\| \to ((\|V\| = 1 \lor \|V\| = 3) \to \neg G RegUSGraph k))$
49	48	a1i	$⊢ G \in FriendGraph \to (V \in Fin \to (3 < \|V\| \to ((\|V\| = 1 \lor \|V\| = 3) \to \neg G RegUSGraph k)))$
50	49	3imp	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to ((\|V\| = 1 \lor \|V\| = 3) \to \neg G RegUSGraph k)$
51	50	ad2antrl	$⊢ (G RegUSGraph k \land ((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0})) \to ((\|V\| = 1 \lor \|V\| = 3) \to \neg G RegUSGraph k)$
52	32 51	mpd	$⊢ (G RegUSGraph k \land ((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0})) \to \neg G RegUSGraph k$
53	52	ex	$⊢ G RegUSGraph k \to (((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0}) \to \neg G RegUSGraph k)$
54		ax-1	$⊢ \neg G RegUSGraph k \to (((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0}) \to \neg G RegUSGraph k)$
55	53 54	pm2.61i	$⊢ ((G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \land k \in ℕ_{0}) \to \neg G RegUSGraph k$
56	55	ralrimiva	$⊢ (G \in FriendGraph \land V \in Fin \land 3 < \|V\|) \to \forall k \in ℕ_{0} \neg G RegUSGraph k$

Metamath Proof Explorer

Theorem frgrogt3nreg

Proof