frgrareg - Metamath Proof Explorer

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

Theorem frgrareg 25238

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 25050	. . . . 5 RegUSGrph USGrph $/\$ $/\$ VDeg
2		nn0re 10721	. . . . . . . . . 10
3		1re 9506	. . . . . . . . . 10
4		lenlt 9574	. . . . . . . . . . 11 $/\$
5	4	bicomd 201	. . . . . . . . . 10 $/\$
6	2, 3, 5	sylancl 660	. . . . . . . . 9
7		ioran 488	. . . . . . . . . . 11 $\/$ $/\$
8		df-ne 2579	. . . . . . . . . . . . 13
9		elnnne0 10726	. . . . . . . . . . . . . . . 16 $/\$
10		nnle1eq1 10480	. . . . . . . . . . . . . . . . 17
11		rusgrasn 25066	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ RegUSGrph
12	11	orcd 390	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ RegUSGrph $\/$
13	12	expcom 433	. . . . . . . . . . . . . . . . . . . . . 22 RegUSGrph $\/$
14	13	adantr 463	. . . . . . . . . . . . . . . . . . . . 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 12330	. . . . . . . . . . . . . . . . . . . . 21
19		rusisusgra 25052	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph USGrph
20		usgrav 24459	. . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 RegUSGrph $/\$
22		hasheq0 12336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
23	22	bicomd 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
24	23	necon3bid 2640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
25		elnnne0 10726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
26		df-ne 2579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
27		eluz2b3 11074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
28		eluz2 11007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
29	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
30		2re 10522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
31	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
32		zre 10785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
33	32	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
34		1lt2 10619	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
36	35	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$
37		ltletr 9587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$ $/\$
38	37	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$
39	29, 31, 33, 36, 38	syl31anc 1229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
40		eqeq2 2397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 VDeg VDeg
41	40	ralbidv 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 VDeg VDeg
42	41	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg VDeg
43		vdgn1frgrav3 25149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 FriendGrph $/\$ VDeg
44		r19.26 2909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 VDeg $/\$ VDeg VDeg $/\$ VDeg
45		df-ne 2579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg VDeg
46	45	anbi1i 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
47		ancom 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
48		pm3.24 880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg $/\$ VDeg
49	48	bifal 1412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg
50	46, 47, 49	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 VDeg $/\$ VDeg
51	50	ralbii 2813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 VDeg $/\$ VDeg
52		r19.3rzv 3838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
53		falim 1413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 VDeg VDeg $\/$
59	43, 58	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 FriendGrph $/\$ VDeg $\/$
60	59	expcom 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 FriendGrph VDeg $\/$
61	60	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$ $/\$ FriendGrph VDeg $\/$
62	61	impcom 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
63	42, 62	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
64	63	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 FriendGrph $/\$ $/\$ $/\$ VDeg $\/$
65	64	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 FriendGrph $/\$ $/\$ VDeg $\/$
66	65	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 FriendGrph VDeg $/\$ $/\$ $\/$
67	66	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 VDeg FriendGrph $/\$ $/\$ $\/$
68	67	3ad2ant3 1017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 USGrph $/\$ $/\$ VDeg FriendGrph $/\$ $/\$ $\/$
69	1, 68	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 RegUSGrph FriendGrph $/\$ $/\$ $\/$
70	69	impcom 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 FriendGrph $/\$ RegUSGrph $/\$ $/\$ $\/$
71	70	impcom 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ FriendGrph $/\$ RegUSGrph $/\$ $/\$ $\/$
72	71	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
73	72	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
74	39, 73	syldan 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
75	74	3adant1 1012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
76	28, 75	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ FriendGrph $/\$ RegUSGrph $\/$
77	27, 76	sylbir 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
78	77	expcom 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ FriendGrph $/\$ RegUSGrph $\/$
84	83	com25 91	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ FriendGrph $/\$ RegUSGrph $\/$
85	84	expd 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ FriendGrph $/\$ RegUSGrph $\/$
90	89	expd 434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ FriendGrph RegUSGrph $\/$
91	90	expcom 433	. . . . . . . . . . . . . . . . . . . . . . . . . 26 FriendGrph RegUSGrph $\/$
92	91	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph FriendGrph $\/$
93	92	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ RegUSGrph FriendGrph $\/$
94	21, 93	mpcom 36	. . . . . . . . . . . . . . . . . . . . . . 23 RegUSGrph FriendGrph $\/$
95	94	imp 427	. . . . . . . . . . . . . . . . . . . . . 22 RegUSGrph $/\$ FriendGrph $\/$
96	95	com15 93	. . . . . . . . . . . . . . . . . . . . 21 RegUSGrph $/\$ FriendGrph $\/$
97	18, 96	syl 16	. . . . . . . . . . . . . . . . . . . 20 RegUSGrph $/\$ FriendGrph $\/$
98	97	imp 427	. . . . . . . . . . . . . . . . . . 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 433	. . . . . . . . . . . . . 14 $/\$ RegUSGrph $/\$ FriendGrph $\/$
104	103	com23 78	. . . . . . . . . . . . 13 $/\$ RegUSGrph $/\$ FriendGrph $\/$
105	8, 104	sylbir 213	. . . . . . . . . . . 12 $/\$ RegUSGrph $/\$ FriendGrph $\/$
106	105	adantr 463	. . . . . . . . . . 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 1016	. . . . . 6 USGrph $/\$ $/\$ VDeg RegUSGrph $/\$ FriendGrph $\/$ $/\$ $\/$
112	111	expd 434	. . . . 5 USGrph $/\$ $/\$ VDeg RegUSGrph FriendGrph $\/$ $/\$ $\/$
113	1, 112	mpcom 36	. . . 4 RegUSGrph FriendGrph $\/$ $/\$ $\/$
114	113	impcom 428	. . 3 FriendGrph $/\$ RegUSGrph $\/$ $/\$ $\/$
115	114	com14 88	. 2 $\/$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
116		simprl 754	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph FriendGrph
117		simpl 455	. . . . . 6 $/\$
118	117	ad2antlr 724	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
119		simpr 459	. . . . . 6 $/\$
120	119	ad2antlr 724	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
121		simpl 455	. . . . . 6 $/\$ $/\$
122		simpr 459	. . . . . 6 FriendGrph $/\$ RegUSGrph RegUSGrph
123	121, 122	anim12ci 565	. . . . 5 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph RegUSGrph $/\$
124		frgrareggt1 25237	. . . . . 6 FriendGrph $/\$ $/\$ RegUSGrph $/\$
125	124	imp 427	. . . . 5 FriendGrph $/\$ $/\$ $/\$ RegUSGrph $/\$
126	116, 118, 120, 123, 125	syl31anc 1229	. . . 4 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph
127	126	olcd 391	. . 3 $/\$ $/\$ $/\$ FriendGrph $/\$ RegUSGrph $\/$
128	127	exp31 602	. 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 366 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wfal 1404

wcel 1826

wne 2577

wral 2732

cvv 3034

c0 3711

cop 3950 class class class wbr 4367

cfv 5496 (class class class)co 6196

cfn 7435

cr 9402

cc0 9403

c1 9404

clt 9539

cle 9540

cn 10452

c2 10502

cn0 10712

cz 10781

cuz 11001

chash 12307 USGrph cusg 24451 VDeg cvdg 25014 RegUSGrph crusgra 25044 FriendGrph cfrgra 25109

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-inf2 7972 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-ot 3953 df-uni 4164 df-int 4200 df-iun 4245 df-disj 4339 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-1st 6699 df-2nd 6700 df-recs 6960 df-rdg 6994 df-1o 7048 df-2o 7049 df-oadd 7052 df-er 7229 df-ec 7231 df-qs 7235 df-map 7340 df-pm 7341 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-sup 7816 df-oi 7850 df-card 8233 df-cda 8461 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-n0 10713 df-z 10782 df-uz 11002 df-rp 11140 df-xadd 11240 df-ico 11456 df-fz 11594 df-fzo 11718 df-fl 11828 df-mod 11897 df-seq 12011 df-exp 12070 df-hash 12308 df-word 12446 df-lsw 12447 df-concat 12448 df-s1 12449 df-substr 12450 df-reps 12453 df-csh 12671 df-s2 12724 df-cj 12934 df-re 12935 df-im 12936 df-sqrt 13070 df-abs 13071 df-clim 13313 df-sum 13511 df-dvds 13989 df-gcd 14147 df-prm 14220 df-phi 14298 df-usgra 24454 df-nbgra 24541 df-wlk 24629 df-trail 24630 df-pth 24631 df-spth 24632 df-wlkon 24635 df-spthon 24638 df-wwlk 24800 df-wwlkn 24801 df-clwwlk 24872 df-clwwlkn 24873 df-2wlkonot 24979 df-2spthonot 24981 df-2spthsot 24982 df-vdgr 25015 df-rgra 25045 df-rusgra 25046 df-frgra 25110

This theorem is referenced by: frgraregord013 25239

W3C validator