frgrareg - Metamath Proof Explorer

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

Theorem frgrareg 24989

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 24801	. . . . 5 RegUSGrph USGrph $/\$ $/\$ VDeg
2		nn0re 10810	. . . . . . . . . 10
3		1re 9598	. . . . . . . . . 10
4		lenlt 9666	. . . . . . . . . . 11 $/\$
5	4	bicomd 201	. . . . . . . . . 10 $/\$
6	2, 3, 5	sylancl 662	. . . . . . . . 9
7		ioran 490	. . . . . . . . . . 11 $\/$ $/\$
8		df-ne 2640	. . . . . . . . . . . . 13
9		elnnne0 10815	. . . . . . . . . . . . . . . 16 $/\$
10		nnle1eq1 10570	. . . . . . . . . . . . . . . . 17
11		rusgrasn 24817	. . . . . . . . . . . . . . . . . . . . . . . 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 12407	. . . . . . . . . . . . . . . . . . . . 21
19		rusisusgra 24803	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph USGrph
20		usgrav 24210	. . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 RegUSGrph $/\$
22		hasheq0 12412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
23	22	bicomd 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
24	23	necon3bid 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
25		elnnne0 10815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
26		df-ne 2640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
27		eluz2b3 11164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
28		eluz2 11096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
29	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
30		2re 10611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
31	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
32		zre 10874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
33	32	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
34		1lt2 10708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
36	35	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$
37		ltletr 9679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$ $/\$
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$
39	29, 31, 33, 36, 38	syl31anc 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
40		eqeq2 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 VDeg VDeg
41	40	ralbidv 2882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 VDeg VDeg
42	41	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg VDeg
43		vdgn1frgrav3 24900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 FriendGrph $/\$ VDeg
44		r19.26 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 VDeg $/\$ VDeg VDeg $/\$ VDeg
45		df-ne 2640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg VDeg
46	45	anbi1i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
47		ancom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
48		pm3.24 882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg $/\$ VDeg
49	48	bifal 1396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg
50	46, 47, 49	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 VDeg $/\$ VDeg
51	50	ralbii 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 VDeg $/\$ VDeg
52		r19.3rzv 3908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
53		falim 1397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1019	. . . . . 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 756	. . . . 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 24988	. . . . . 6 FriendGrph $/\$ $/\$ RegUSGrph $/\$
125	124	imp 429	. . . . 5 FriendGrph $/\$ $/\$ $/\$ RegUSGrph $/\$
126	116, 118, 120, 123, 125	syl31anc 1232	. . . 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 974

wceq 1383

wfal 1388

wcel 1804

wne 2638

wral 2793

cvv 3095

c0 3770

cop 4020 class class class wbr 4437

cfv 5578 (class class class)co 6281

cfn 7518

cr 9494

cc0 9495

c1 9496

clt 9631

cle 9632

cn 10542

c2 10591

cn0 10801

cz 10870

cuz 11090

chash 12384 USGrph cusg 24202 VDeg cvdg 24765 RegUSGrph crusgra 24795 FriendGrph cfrgra 24860

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-ot 4023 df-uni 4235 df-int 4272 df-iun 4317 df-disj 4408 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-er 7313 df-ec 7315 df-qs 7319 df-map 7424 df-pm 7425 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-sup 7903 df-oi 7938 df-card 8323 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10213 df-nn 10543 df-2 10600 df-3 10601 df-n0 10802 df-z 10871 df-uz 11091 df-rp 11230 df-xadd 11328 df-fz 11682 df-fzo 11804 df-fl 11908 df-mod 11976 df-seq 12087 df-exp 12146 df-hash 12385 df-word 12521 df-lsw 12522 df-concat 12523 df-s1 12524 df-substr 12525 df-reps 12528 df-csh 12739 df-s2 12792 df-cj 12911 df-re 12912 df-im 12913 df-sqrt 13047 df-abs 13048 df-clim 13290 df-sum 13488 df-dvds 13864 df-gcd 14022 df-prm 14095 df-phi 14173 df-usgra 24205 df-nbgra 24292 df-wlk 24380 df-trail 24381 df-pth 24382 df-spth 24383 df-wlkon 24386 df-spthon 24389 df-wwlk 24551 df-wwlkn 24552 df-clwwlk 24623 df-clwwlkn 24624 df-2wlkonot 24730 df-2spthonot 24732 df-2spthsot 24733 df-vdgr 24766 df-rgra 24796 df-rusgra 24797 df-frgra 24861

This theorem is referenced by: frgraregord013 24990

W3C validator