frgrreggt1

Description: If a finite nonempty friendship graph is K-regular with K > 1 , then K must be 2 . (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 3-Jun-2021)

		Ref	Expression
	Hypothesis	frgrreggt1.v	$⊢ V = Vtx (G)$
	Assertion	frgrreggt1	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to ((G RegUSGraph K \land 1 < K) \to K = 2)$

Proof

Step	Hyp	Ref	Expression
1		frgrreggt1.v	$⊢ V = Vtx (G)$
2		simp1	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to G \in FriendGraph$
3	2	anim1ci	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (G RegUSGraph K \land G \in FriendGraph)$
4		simp3	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to V \neq \emptyset$
5		simp2	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to V \in Fin$
6	4 5	jca	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to (V \neq \emptyset \land V \in Fin)$
7	6	adantr	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (V \neq \emptyset \land V \in Fin)$
8	1	numclwwlk7lem	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin)) \to K \in ℕ_{0}$
9	3 7 8	syl2anc	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to K \in ℕ_{0}$
10		2z	$⊢ 2 \in ℤ$
11	10	a1i	$⊢ (K \in ℕ_{0} \land 2 < K) \to 2 \in ℤ$
12		nn0z	$⊢ K \in ℕ_{0} \to K \in ℤ$
13	12	adantr	$⊢ (K \in ℕ_{0} \land 2 < K) \to K \in ℤ$
14		peano2zm	$⊢ K \in ℤ \to K - 1 \in ℤ$
15	13 14	syl	$⊢ (K \in ℕ_{0} \land 2 < K) \to K - 1 \in ℤ$
16		zltlem1	$⊢ (2 \in ℤ \land K \in ℤ) \to (2 < K \leftrightarrow 2 \leq K - 1)$
17	10 12 16	sylancr	$⊢ K \in ℕ_{0} \to (2 < K \leftrightarrow 2 \leq K - 1)$
18	17	biimpa	$⊢ (K \in ℕ_{0} \land 2 < K) \to 2 \leq K - 1$
19		eluz2	$⊢ K - 1 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land K - 1 \in ℤ \land 2 \leq K - 1)$
20	11 15 18 19	syl3anbrc	$⊢ (K \in ℕ_{0} \land 2 < K) \to K - 1 \in ℤ_{\geq 2}$
21		exprmfct	$⊢ K - 1 \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (K - 1)$
22	20 21	syl	$⊢ (K \in ℕ_{0} \land 2 < K) \to \exists p \in ℙ p ∥ (K - 1)$
23	5	anim1ci	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (G RegUSGraph K \land V \in Fin)$
24	1	finrusgrfusgr	$⊢ (G RegUSGraph K \land V \in Fin) \to G \in FinUSGraph$
25	23 24	syl	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to G \in FinUSGraph$
26	25	3ad2ant3	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to G \in FinUSGraph$
27		simp1l	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to p \in ℙ$
28		numclwwlk8	$⊢ (G \in FinUSGraph \land p \in ℙ) \to \|p ClWWalksN G\| \mod p = 0$
29	26 27 28	syl2anc	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to \|p ClWWalksN G\| \mod p = 0$
30	3	3ad2ant3	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to (G RegUSGraph K \land G \in FriendGraph)$
31		pm3.22	$⊢ (V \in Fin \land V \neq \emptyset) \to (V \neq \emptyset \land V \in Fin)$
32	31	3adant1	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to (V \neq \emptyset \land V \in Fin)$
33	32	adantr	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (V \neq \emptyset \land V \in Fin)$
34	33	3ad2ant3	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to (V \neq \emptyset \land V \in Fin)$
35		simp1	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to (p \in ℙ \land p ∥ (K - 1))$
36	1	numclwwlk7	$⊢ ((G RegUSGraph K \land G \in FriendGraph) \land (V \neq \emptyset \land V \in Fin) \land (p \in ℙ \land p ∥ (K - 1))) \to \|p ClWWalksN G\| \mod p = 1$
37	30 34 35 36	syl3anc	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to \|p ClWWalksN G\| \mod p = 1$
38		eqeq1	$⊢ \|p ClWWalksN G\| \mod p = 0 \to (\|p ClWWalksN G\| \mod p = 1 \leftrightarrow 0 = 1)$
39		ax-1ne0	$⊢ 1 \neq 0$
40	39	nesymi	$⊢ \neg 0 = 1$
41	40	pm2.21i	$⊢ 0 = 1 \to K = 2$
42	38 41	syl6bi	$⊢ \|p ClWWalksN G\| \mod p = 0 \to (\|p ClWWalksN G\| \mod p = 1 \to K = 2)$
43	29 37 42	sylc	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to K = 2$
44	43	a1d	$⊢ ((p \in ℙ \land p ∥ (K - 1)) \land (K \in ℕ_{0} \land 2 < K) \land ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K)) \to (1 < K \to K = 2)$
45	44	3exp	$⊢ (p \in ℙ \land p ∥ (K - 1)) \to ((K \in ℕ_{0} \land 2 < K) \to (((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (1 < K \to K = 2)))$
46	45	rexlimiva	$⊢ \exists p \in ℙ p ∥ (K - 1) \to ((K \in ℕ_{0} \land 2 < K) \to (((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (1 < K \to K = 2)))$
47	22 46	mpcom	$⊢ (K \in ℕ_{0} \land 2 < K) \to (((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (1 < K \to K = 2))$
48	47	expcom	$⊢ 2 < K \to (K \in ℕ_{0} \to (((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (1 < K \to K = 2)))$
49	48	com23	$⊢ 2 < K \to (((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (K \in ℕ_{0} \to (1 < K \to K = 2)))$
50		1red	$⊢ K \in ℕ_{0} \to 1 \in ℝ$
51		nn0re	$⊢ K \in ℕ_{0} \to K \in ℝ$
52	50 51	ltnled	$⊢ K \in ℕ_{0} \to (1 < K \leftrightarrow \neg K \leq 1)$
53		1e2m1	$⊢ 1 = 2 - 1$
54	53	a1i	$⊢ K \in ℕ_{0} \to 1 = 2 - 1$
55	54	breq2d	$⊢ K \in ℕ_{0} \to (K \leq 1 \leftrightarrow K \leq 2 - 1)$
56	55	notbid	$⊢ K \in ℕ_{0} \to (\neg K \leq 1 \leftrightarrow \neg K \leq 2 - 1)$
57		zltlem1	$⊢ (K \in ℤ \land 2 \in ℤ) \to (K < 2 \leftrightarrow K \leq 2 - 1)$
58	12 10 57	sylancl	$⊢ K \in ℕ_{0} \to (K < 2 \leftrightarrow K \leq 2 - 1)$
59	58	bicomd	$⊢ K \in ℕ_{0} \to (K \leq 2 - 1 \leftrightarrow K < 2)$
60	59	notbid	$⊢ K \in ℕ_{0} \to (\neg K \leq 2 - 1 \leftrightarrow \neg K < 2)$
61	52 56 60	3bitrd	$⊢ K \in ℕ_{0} \to (1 < K \leftrightarrow \neg K < 2)$
62		2re	$⊢ 2 \in ℝ$
63		lttri3	$⊢ (K \in ℝ \land 2 \in ℝ) \to (K = 2 \leftrightarrow (\neg K < 2 \land \neg 2 < K))$
64	63	biimprd	$⊢ (K \in ℝ \land 2 \in ℝ) \to ((\neg K < 2 \land \neg 2 < K) \to K = 2)$
65	51 62 64	sylancl	$⊢ K \in ℕ_{0} \to ((\neg K < 2 \land \neg 2 < K) \to K = 2)$
66	65	expd	$⊢ K \in ℕ_{0} \to (\neg K < 2 \to (\neg 2 < K \to K = 2))$
67	61 66	sylbid	$⊢ K \in ℕ_{0} \to (1 < K \to (\neg 2 < K \to K = 2))$
68	67	com3r	$⊢ \neg 2 < K \to (K \in ℕ_{0} \to (1 < K \to K = 2))$
69	68	a1d	$⊢ \neg 2 < K \to (((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (K \in ℕ_{0} \to (1 < K \to K = 2)))$
70	49 69	pm2.61i	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (K \in ℕ_{0} \to (1 < K \to K = 2))$
71	9 70	mpd	$⊢ ((G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \land G RegUSGraph K) \to (1 < K \to K = 2)$
72	71	expimpd	$⊢ (G \in FriendGraph \land V \in Fin \land V \neq \emptyset) \to ((G RegUSGraph K \land 1 < K) \to K = 2)$

Metamath Proof Explorer

Theorem frgrreggt1

Proof