frgrareg - Metamath Proof Explorer

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

Theorem frgrareg 25838

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 25650	. . . . 5 RegUSGrph USGrph $/\$ $/\$ VDeg
2		nn0re 10875	. . . . . . . . . 10
3		1re 9639	. . . . . . . . . 10
4		lenlt 9709	. . . . . . . . . . 11 $/\$
5	4	bicomd 205	. . . . . . . . . 10 $/\$
6	2, 3, 5	sylancl 667	. . . . . . . . 9
7		ioran 493	. . . . . . . . . . 11 $\/$ $/\$
8		df-ne 2623	. . . . . . . . . . . . 13
9		elnnne0 10880	. . . . . . . . . . . . . . . 16 $/\$
10		nnle1eq1 10634	. . . . . . . . . . . . . . . . 17
11		rusgrasn 25666	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ RegUSGrph
12	11	orcd 394	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ RegUSGrph $\/$
13	12	expcom 437	. . . . . . . . . . . . . . . . . . . . . 22 RegUSGrph $\/$
14	13	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 RegUSGrph $/\$ FriendGrph $\/$
15	14	com12 32	. . . . . . . . . . . . . . . . . . . 20 RegUSGrph $/\$ FriendGrph $\/$
16	15	a1d 26	. . . . . . . . . . . . . . . . . . 19 $/\$ RegUSGrph $/\$ FriendGrph $\/$
17	16	a1d 26	. . . . . . . . . . . . . . . . . 18 $/\$ RegUSGrph $/\$ FriendGrph $\/$
18		hashcl 12535	. . . . . . . . . . . . . . . . . . . . 21
19		rusisusgra 25652	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph USGrph
20		usgrav 25058	. . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph $/\$
21	19, 20	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 RegUSGrph $/\$
22		hasheq0 12541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
23	22	bicomd 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
24	23	necon3bid 2667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
25		elnnne0 10880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
26		df-ne 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
27		eluz2b3 11229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
28		eluz2 11162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
29	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
30		2re 10676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
31	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
32		zre 10938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
33	32	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
34		1lt2 10773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
36	35	anim1i 571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$
37		ltletr 9722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$ $/\$
38	37	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$
39	29, 31, 33, 36, 38	syl31anc 1270	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
40		eqeq2 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 VDeg VDeg
41	40	ralbidv 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 VDeg VDeg
42	41	ad2antll 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg VDeg
43		vdgn1frgrav3 25749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 FriendGrph $/\$ VDeg
44		r19.26 2916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 VDeg $/\$ VDeg VDeg $/\$ VDeg
45		df-ne 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg VDeg
46	45	anbi1i 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
47		ancom 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
48		pm3.24 892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg $/\$ VDeg
49	48	bifal 1456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg
50	46, 47, 49	3bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 VDeg $/\$ VDeg
51	50	ralbii 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 VDeg $/\$ VDeg
52		r19.3rzv 3861	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
53		falim 1457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 $\/$
54	52, 53	syl6bir 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 $\/$
55	54	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 $\/$
56	51, 55	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 VDeg $/\$ VDeg $\/$
57	44, 56	sylbir 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 VDeg $/\$ VDeg $\/$
58	57	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 VDeg VDeg $\/$
59	43, 58	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 FriendGrph $/\$ VDeg $\/$
60	59	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 FriendGrph VDeg $\/$
61	60	ad2antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$ $/\$ FriendGrph VDeg $\/$
62	61	impcom 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
63	42, 62	sylbid 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
64	63	com23 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
65	64	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 FriendGrph $/\$ $/\$ VDeg $\/$
66	65	com24 90	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 FriendGrph VDeg $/\$ $/\$ $\/$
67	66	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 VDeg FriendGrph $/\$ $/\$ $\/$
68	67	3ad2ant3 1030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 USGrph $/\$ $/\$ VDeg FriendGrph $/\$ $/\$ $\/$
69	1, 68	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 RegUSGrph FriendGrph $/\$ $/\$ $\/$
70	69	impcom 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 FriendGrph $/\$ RegUSGrph $/\$ $/\$ $\/$
71	70	impcom 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ FriendGrph $/\$ RegUSGrph $/\$ $/\$ $\/$
72	71	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
73	72	ex 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
74	39, 73	syldan 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
75	74	3adant1 1025	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
76	28, 75	sylbi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ FriendGrph $/\$ RegUSGrph $\/$
77	27, 76	sylbir 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
78	77	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ FriendGrph $/\$ RegUSGrph $\/$
79	78	com23 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ FriendGrph $/\$ RegUSGrph $\/$
80	26, 79	sylbir 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ FriendGrph $/\$ RegUSGrph $\/$
81	80	com13 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ FriendGrph $/\$ RegUSGrph $\/$
82	25, 81	sylbir 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
83	82	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ FriendGrph $/\$ RegUSGrph $\/$
84	83	com25 94	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ FriendGrph $/\$ RegUSGrph $\/$
85	84	expd 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 FriendGrph $/\$ RegUSGrph $\/$
86	24, 85	syl6bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FriendGrph $/\$ RegUSGrph $\/$
87	86	com13 83	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FriendGrph $/\$ RegUSGrph $\/$
88	87	pm2.43i 49	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FriendGrph $/\$ RegUSGrph $\/$
89	88	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ FriendGrph $/\$ RegUSGrph $\/$
90	89	expd 438	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ FriendGrph RegUSGrph $\/$
91	90	expcom 437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 FriendGrph RegUSGrph $\/$
92	91	com24 90	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph FriendGrph $\/$
93	92	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ RegUSGrph FriendGrph $\/$
94	21, 93	mpcom 37	. . . . . . . . . . . . . . . . . . . . . . 23 RegUSGrph FriendGrph $\/$
95	94	imp 431	. . . . . . . . . . . . . . . . . . . . . 22 RegUSGrph $/\$ FriendGrph $\/$
96	95	com15 96	. . . . . . . . . . . . . . . . . . . . 21 RegUSGrph $/\$ FriendGrph $\/$
97	18, 96	syl 17	. . . . . . . . . . . . . . . . . . . 20 RegUSGrph $/\$ FriendGrph $\/$
98	97	imp 431	. . . . . . . . . . . . . . . . . . 19 $/\$ RegUSGrph $/\$ FriendGrph $\/$
99	98	com13 83	. . . . . . . . . . . . . . . . . 18 $/\$ RegUSGrph $/\$ FriendGrph $\/$
100	17, 99	pm2.61i 168	. . . . . . . . . . . . . . . . 17 $/\$ RegUSGrph $/\$ FriendGrph $\/$
101	10, 100	syl6bi 232	. . . . . . . . . . . . . . . 16 $/\$ RegUSGrph $/\$ FriendGrph $\/$
102	9, 101	sylbir 217	. . . . . . . . . . . . . . 15 $/\$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
103	102	expcom 437	. . . . . . . . . . . . . 14 $/\$ RegUSGrph $/\$ FriendGrph $\/$
104	103	com23 81	. . . . . . . . . . . . 13 $/\$ RegUSGrph $/\$ FriendGrph $\/$
105	8, 104	sylbir 217	. . . . . . . . . . . 12 $/\$ RegUSGrph $/\$ FriendGrph $\/$
106	105	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
107	7, 106	sylbi 199	. . . . . . . . . 10 $\/$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
108	107	com13 83	. . . . . . . . 9 $\/$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
109	6, 108	sylbid 219	. . . . . . . 8 $\/$ $/\$ RegUSGrph $/\$ FriendGrph $\/$
110	109	com25 94	. . . . . . 7 RegUSGrph $/\$ FriendGrph $\/$ $/\$ $\/$
111	110	3ad2ant2 1029	. . . . . 6 USGrph $/\$ $/\$ VDeg RegUSGrph $/\$ FriendGrph $\/$ $/\$ $\/$
112	111	expd 438	. . . . 5 USGrph $/\$ $/\$ VDeg RegUSGrph FriendGrph $\/$ $/\$ $\/$
113	1, 112	mpcom 37	. . . 4 RegUSGrph FriendGrph $\/$ $/\$ $\/$
114	113	impcom 432	. . 3 FriendGrph $/\$ RegUSGrph $\/$ $/\$ $\/$
115	114	com14 91	. 2 $\/$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
116		simprl 763	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph FriendGrph
117		simpl 459	. . . . . 6 $/\$
118	117	ad2antlr 732	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
119		simpr 463	. . . . . 6 $/\$
120	119	ad2antlr 732	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
121		simpl 459	. . . . . 6 $/\$ $/\$
122		simpr 463	. . . . . 6 FriendGrph $/\$ RegUSGrph RegUSGrph
123	121, 122	anim12ci 570	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph RegUSGrph $/\$
124		frgrareggt1 25837	. . . . . 6 FriendGrph $/\$ $/\$ RegUSGrph $/\$
125	124	imp 431	. . . . 5 FriendGrph $/\$ $/\$ $/\$ RegUSGrph $/\$
126	116, 118, 120, 123, 125	syl31anc 1270	. . . 4 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
127	126	olcd 395	. . 3 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
128	127	exp31 608	. 2 $/\$ FriendGrph $/\$ RegUSGrph $\/$
129		2a1 28	. 2 $\/$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
130	115, 128, 129	pm2.61ii 169	1 $/\$ FriendGrph $/\$ RegUSGrph $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wfal 1448

wcel 1886

wne 2621

wral 2736

cvv 3044

c0 3730

cop 3973 class class class wbr 4401

cfv 5581 (class class class)co 6288

cfn 7566

cr 9535

cc0 9536

c1 9537

clt 9672

cle 9673

cn 10606

c2 10656

cn0 10866

cz 10934

cuz 11156

chash 12512 USGrph cusg 25050 VDeg cvdg 25614 RegUSGrph crusgra 25644 FriendGrph cfrgra 25709

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-ot 3976 df-uni 4198 df-int 4234 df-iun 4279 df-disj 4373 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-2o 7180 df-oadd 7183 df-er 7360 df-ec 7362 df-qs 7366 df-map 7471 df-pm 7472 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-sup 7953 df-inf 7954 df-oi 8022 df-card 8370 df-cda 8595 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-rp 11300 df-xadd 11407 df-ico 11638 df-fz 11782 df-fzo 11913 df-fl 12025 df-mod 12094 df-seq 12211 df-exp 12270 df-hash 12513 df-word 12661 df-lsw 12662 df-concat 12663 df-s1 12664 df-substr 12665 df-reps 12668 df-csh 12886 df-s2 12939 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-sum 13746 df-dvds 14299 df-gcd 14462 df-prm 14616 df-phi 14707 df-usgra 25053 df-nbgra 25141 df-wlk 25229 df-trail 25230 df-pth 25231 df-spth 25232 df-wlkon 25235 df-spthon 25238 df-wwlk 25400 df-wwlkn 25401 df-clwwlk 25472 df-clwwlkn 25473 df-2wlkonot 25579 df-2spthonot 25581 df-2spthsot 25582 df-vdgr 25615 df-rgra 25645 df-rusgra 25646 df-frgra 25710

This theorem is referenced by: frgraregord013 25839

W3C validator