frgrareg - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > frgrareg		Structured version Unicode version

Theorem frgrareg 24794

Description: If a finite friendship graph is k-regular, then k must be 2 (or 0). (Contributed by Alexander van der Vekens, 9-Oct-2018.)

**Assertion**
Ref	Expression
frgrareg	$/\$ FriendGrph $/\$ RegUSGrph $\/$

Proof of Theorem frgrareg Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rusgraprop 24605	. . . . 5 RegUSGrph USGrph $/\$ $/\$ VDeg
2		nn0re 10800	. . . . . . . . . 10
3		1re 9591	. . . . . . . . . 10
4		lenlt 9659	. . . . . . . . . . 11 $/\$
5	4	bicomd 201	. . . . . . . . . 10 $/\$
6	2, 3, 5	sylancl 662	. . . . . . . . 9
7		ioran 490	. . . . . . . . . . 11 $\/$ $/\$
8		df-ne 2664	. . . . . . . . . . . . 13
9		elnnne0 10805	. . . . . . . . . . . . . . . 16 $/\$
10		nnle1eq1 10560	. . . . . . . . . . . . . . . . 17
11		rusgrasn 24621	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ RegUSGrph
12	11	orcd 392	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ RegUSGrph $\/$
13	12	expcom 435	. . . . . . . . . . . . . . . . . . . . . 22 RegUSGrph $\/$
14	13	adantr 465	. . . . . . . . . . . . . . . . . . . . 21 RegUSGrph $/\$ FriendGrph $\/$
15	14	com12 31	. . . . . . . . . . . . . . . . . . . 20 RegUSGrph $/\$ FriendGrph $\/$
16	15	a1d 25	. . . . . . . . . . . . . . . . . . 19 $/\$ RegUSGrph $/\$ FriendGrph $\/$
17	16	a1d 25	. . . . . . . . . . . . . . . . . 18 $/\$ RegUSGrph $/\$ FriendGrph $\/$
18		hashcl 12392	. . . . . . . . . . . . . . . . . . . . 21
19		rusisusgra 24607	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph USGrph
20		usgrav 24014	. . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 RegUSGrph $/\$
22		hasheq0 12397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
23	22	bicomd 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
24	23	necon3bid 2725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
25		elnnne0 10805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
26		df-ne 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
27		eluz2b3 11151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
28		eluz2 11084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
29	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
30		2re 10601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
31	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
32		zre 10864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
33	32	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
34		1lt2 10698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
36	35	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$
37		ltletr 9672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$ $/\$
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$
39	29, 31, 33, 36, 38	syl31anc 1231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
40		eqeq2 2482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 VDeg VDeg
41	40	ralbidv 2903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 VDeg VDeg
42	41	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg VDeg
43		vdgn1frgrav3 24705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 FriendGrph $/\$ VDeg
44		r19.26 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 VDeg $/\$ VDeg VDeg $/\$ VDeg
45		df-ne 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg VDeg
46	45	anbi1i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
47		ancom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
48		pm3.24 880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg $/\$ VDeg
49	48	bifal 1392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg
50	46, 47, 49	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 VDeg $/\$ VDeg
51	50	ralbii 2895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 VDeg $/\$ VDeg
52		r19.3rzv 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
53		falim 1393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 $\/$
54	52, 53	syl6bir 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 $\/$
55	54	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 $\/$
56	51, 55	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 VDeg $/\$ VDeg $\/$
57	44, 56	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 VDeg $/\$ VDeg $\/$
58	57	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 VDeg VDeg $\/$
59	43, 58	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 FriendGrph $/\$ VDeg $\/$
60	59	expcom 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 FriendGrph VDeg $\/$
61	60	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$ $/\$ FriendGrph VDeg $\/$
62	61	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
63	42, 62	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
64	63	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
65	64	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 FriendGrph $/\$ $/\$ VDeg $\/$
66	65	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 FriendGrph VDeg $/\$ $/\$ $\/$
67	66	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 VDeg FriendGrph $/\$ $/\$ $\/$
68	67	3ad2ant3 1019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 USGrph $/\$ $/\$ VDeg FriendGrph $/\$ $/\$ $\/$
69	1, 68	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 RegUSGrph FriendGrph $/\$ $/\$ $\/$
70	69	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 FriendGrph $/\$ RegUSGrph $/\$ $/\$ $\/$
71	70	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ FriendGrph $/\$ RegUSGrph $/\$ $/\$ $\/$
72	71	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
73	72	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
74	39, 73	syldan 470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
75	74	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
76	28, 75	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ FriendGrph $/\$ RegUSGrph $\/$
77	27, 76	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
78	77	expcom 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ FriendGrph $/\$ RegUSGrph $\/$
79	78	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ FriendGrph $/\$ RegUSGrph $\/$
80	26, 79	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ FriendGrph $/\$ RegUSGrph $\/$
81	80	com13 80	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ FriendGrph $/\$ RegUSGrph $\/$
82	25, 81	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
83	82	expcom 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ FriendGrph $/\$ RegUSGrph $\/$
84	83	com25 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ FriendGrph $/\$ RegUSGrph $\/$
85	84	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 FriendGrph $/\$ RegUSGrph $\/$
86	24, 85	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FriendGrph $/\$ RegUSGrph $\/$
87	86	com13 80	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FriendGrph $/\$ RegUSGrph $\/$
88	87	pm2.43i 47	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FriendGrph $/\$ RegUSGrph $\/$
89	88	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ FriendGrph $/\$ RegUSGrph $\/$
90	89	expd 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ FriendGrph RegUSGrph $\/$
91	90	expcom 435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 FriendGrph RegUSGrph $\/$
92	91	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph FriendGrph $\/$
93	92	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ RegUSGrph FriendGrph $\/$
94	21, 93	mpcom 36	. . . . . . . . . . . . . . . . . . . . . . 23 RegUSGrph FriendGrph $\/$
95	94	imp 429	. . . . . . . . . . . . . . . . . . . . . 22 RegUSGrph $/\$ FriendGrph $\/$
96	95	com15 93	. . . . . . . . . . . . . . . . . . . . 21 RegUSGrph $/\$ FriendGrph $\/$
97	18, 96	syl 16	. . . . . . . . . . . . . . . . . . . 20 RegUSGrph $/\$ FriendGrph $\/$
98	97	imp 429	. . . . . . . . . . . . . . . . . . 19 $/\$ RegUSGrph $/\$ FriendGrph $\/$
99	98	com13 80	. . . . . . . . . . . . . . . . . 18 $/\$ RegUSGrph $/\$ FriendGrph $\/$
100	17, 99	pm2.61i 164	. . . . . . . . . . . . . . . . 17 $/\$ RegUSGrph $/\$ FriendGrph $\/$
101	10, 100	syl6bi 228	. . . . . . . . . . . . . . . 16 $/\$ RegUSGrph $/\$ FriendGrph $\/$
102	9, 101	sylbir 213	. . . . . . . . . . . . . . 15 $/\$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
103	102	expcom 435	. . . . . . . . . . . . . 14 $/\$ RegUSGrph $/\$ FriendGrph $\/$
104	103	com23 78	. . . . . . . . . . . . 13 $/\$ RegUSGrph $/\$ FriendGrph $\/$
105	8, 104	sylbir 213	. . . . . . . . . . . 12 $/\$ RegUSGrph $/\$ FriendGrph $\/$
106	105	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
107	7, 106	sylbi 195	. . . . . . . . . 10 $\/$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
108	107	com13 80	. . . . . . . . 9 $\/$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
109	6, 108	sylbid 215	. . . . . . . 8 $\/$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
110	109	com25 91	. . . . . . 7 RegUSGrph $/\$ FriendGrph $\/$ $/\$ $\/$
111	110	3ad2ant2 1018	. . . . . 6 USGrph $/\$ $/\$ VDeg RegUSGrph $/\$ FriendGrph $\/$ $/\$ $\/$
112	111	expd 436	. . . . 5 USGrph $/\$ $/\$ VDeg RegUSGrph FriendGrph $\/$ $/\$ $\/$
113	1, 112	mpcom 36	. . . 4 RegUSGrph FriendGrph $\/$ $/\$ $\/$
114	113	impcom 430	. . 3 FriendGrph $/\$ RegUSGrph $\/$ $/\$ $\/$
115	114	com14 88	. 2 $\/$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
116		simprl 755	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph FriendGrph
117		simpl 457	. . . . . 6 $/\$
118	117	ad2antlr 726	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
119		simpr 461	. . . . . 6 $/\$
120	119	ad2antlr 726	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
121		simpl 457	. . . . . 6 $/\$ $/\$
122		simpr 461	. . . . . 6 FriendGrph $/\$ RegUSGrph RegUSGrph
123	121, 122	anim12ci 567	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph RegUSGrph $/\$
124		frgrareggt1 24793	. . . . . 6 FriendGrph $/\$ $/\$ RegUSGrph $/\$
125	124	imp 429	. . . . 5 FriendGrph $/\$ $/\$ $/\$ RegUSGrph $/\$
126	116, 118, 120, 123, 125	syl31anc 1231	. . . 4 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
127	126	olcd 393	. . 3 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
128	127	exp31 604	. 2 $/\$ FriendGrph $/\$ RegUSGrph $\/$
129		ax-1 6	. . 3 $\/$ FriendGrph $/\$ RegUSGrph $\/$
130	129	a1d 25	. 2 $\/$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
131	115, 128, 130	pm2.61ii 165	1 $/\$ FriendGrph $/\$ RegUSGrph $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wfal 1384

wcel 1767

wne 2662

wral 2814

cvv 3113

c0 3785

cop 4033 class class class wbr 4447

cfv 5586 (class class class)co 6282

cfn 7513

cr 9487

cc0 9488

c1 9489

clt 9624

cle 9625

cn 10532

c2 10581

cn0 10791

cz 10860

cuz 11078

chash 12369 USGrph cusg 24006 VDeg cvdg 24569 RegUSGrph crusgra 24599 FriendGrph cfrgra 24664

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-inf2 8054 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565 ax-pre-sup 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-ot 4036 df-uni 4246 df-int 4283 df-iun 4327 df-disj 4418 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-se 4839 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-isom 5595 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-2o 7128 df-oadd 7131 df-er 7308 df-ec 7310 df-qs 7314 df-map 7419 df-pm 7420 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-sup 7897 df-oi 7931 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-div 10203 df-nn 10533 df-2 10590 df-3 10591 df-n0 10792 df-z 10861 df-uz 11079 df-rp 11217 df-xadd 11315 df-fz 11669 df-fzo 11789 df-fl 11893 df-mod 11961 df-seq 12072 df-exp 12131 df-hash 12370 df-word 12504 df-lsw 12505 df-concat 12506 df-s1 12507 df-substr 12508 df-reps 12511 df-csh 12719 df-s2 12772 df-cj 12891 df-re 12892 df-im 12893 df-sqrt 13027 df-abs 13028 df-clim 13270 df-sum 13468 df-dvds 13844 df-gcd 14000 df-prm 14073 df-phi 14151 df-usgra 24009 df-nbgra 24096 df-wlk 24184 df-trail 24185 df-pth 24186 df-spth 24187 df-wlkon 24190 df-spthon 24193 df-wwlk 24355 df-wwlkn 24356 df-clwwlk 24427 df-clwwlkn 24428 df-2wlkonot 24534 df-2spthonot 24536 df-2spthsot 24537 df-vdgr 24570 df-rgra 24600 df-rusgra 24601 df-frgra 24665

This theorem is referenced by: frgraregord013 24795

W3C validator