frgrareg - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > frgrareg		Structured version Unicode version

Theorem frgrareg 30857

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 30693	. . . . 5 RegUSGrph USGrph $/\$ $/\$ VDeg
2		nn0re 10698	. . . . . . . . . 10
3		1re 9495	. . . . . . . . . 10
4		lenlt 9563	. . . . . . . . . . 11 $/\$
5	4	bicomd 201	. . . . . . . . . 10 $/\$
6	2, 3, 5	sylancl 662	. . . . . . . . 9
7		ioran 490	. . . . . . . . . . 11 $\/$ $/\$
8		df-ne 2649	. . . . . . . . . . . . 13
9		elnnne0 10703	. . . . . . . . . . . . . . . 16 $/\$
10		nnle1eq1 10460	. . . . . . . . . . . . . . . . 17
11		rusgrasn 30704	. . . . . . . . . . . . . . . . . . . . . . . 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 12242	. . . . . . . . . . . . . . . . . . . . 21
19		rusisusgra 30695	. . . . . . . . . . . . . . . . . . . . . . . . 25 RegUSGrph USGrph
20		usgrav 23421	. . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph $/\$
21	19, 20	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 RegUSGrph $/\$
22		hasheq0 12247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
23	22	bicomd 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
24	23	necon3bid 2709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
25		elnnne0 10703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
26		df-ne 2649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
27		eluz2b3 11038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
28		eluz2 10977	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
29	3	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
30		2re 10501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
31	30	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
32		zre 10760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
33	32	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
34		1lt2 10598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
36	35	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$
37		ltletr 9576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$ $/\$
38	37	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$
39	29, 31, 33, 36, 38	syl31anc 1222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
40		eqeq2 2469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 VDeg VDeg
41	40	ralbidv 2845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 VDeg VDeg
42	41	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 FriendGrph $/\$ $/\$ $/\$ VDeg VDeg
43		vdgn1frgrav3 30768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 FriendGrph $/\$ VDeg
44		r19.26 2953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 VDeg $/\$ VDeg VDeg $/\$ VDeg
45		df-ne 2649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg VDeg
46	45	anbi1i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
47		ancom 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg VDeg $/\$ VDeg
48		pm3.24 877	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 VDeg $/\$ VDeg
49	48	bifal 1383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 VDeg $/\$ VDeg
50	46, 47, 49	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 VDeg $/\$ VDeg
51	50	ralbii 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 VDeg $/\$ VDeg
52		r19.3rzv 3880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
53		falim 1384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1010	. . . . . 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 30856	. . . . . 6 FriendGrph $/\$ $/\$ RegUSGrph $/\$
125	124	imp 429	. . . . 5 FriendGrph $/\$ $/\$ $/\$ RegUSGrph $/\$
126	116, 118, 120, 123, 125	syl31anc 1222	. . . 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 965

wceq 1370

wfal 1375

wcel 1758

wne 2647

wral 2798

cvv 3076

c0 3744

cop 3990 class class class wbr 4399

cfv 5525 (class class class)co 6199

cfn 7419

cr 9391

cc0 9392

c1 9393

clt 9528

cle 9529

cn 10432

c2 10481

cn0 10689

cz 10756

cuz 10971

chash 12219 USGrph cusg 23415 VDeg cvdg 23714 RegUSGrph crusgra 30687 FriendGrph cfrgra 30727

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4510 ax-sep 4520 ax-nul 4528 ax-pow 4577 ax-pr 4638 ax-un 6481 ax-inf2 7957 ax-cnex 9448 ax-resscn 9449 ax-1cn 9450 ax-icn 9451 ax-addcl 9452 ax-addrcl 9453 ax-mulcl 9454 ax-mulrcl 9455 ax-mulcom 9456 ax-addass 9457 ax-mulass 9458 ax-distr 9459 ax-i2m1 9460 ax-1ne0 9461 ax-1rid 9462 ax-rnegex 9463 ax-rrecex 9464 ax-cnre 9465 ax-pre-lttri 9466 ax-pre-lttrn 9467 ax-pre-ltadd 9468 ax-pre-mulgt0 9469 ax-pre-sup 9470

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2649 df-nel 2650 df-ral 2803 df-rex 2804 df-reu 2805 df-rmo 2806 df-rab 2807 df-v 3078 df-sbc 3293 df-csb 3395 df-dif 3438 df-un 3440 df-in 3442 df-ss 3449 df-pss 3451 df-nul 3745 df-if 3899 df-pw 3969 df-sn 3985 df-pr 3987 df-tp 3989 df-op 3991 df-ot 3993 df-uni 4199 df-int 4236 df-iun 4280 df-disj 4370 df-br 4400 df-opab 4458 df-mpt 4459 df-tr 4493 df-eprel 4739 df-id 4743 df-po 4748 df-so 4749 df-fr 4786 df-se 4787 df-we 4788 df-ord 4829 df-on 4830 df-lim 4831 df-suc 4832 df-xp 4953 df-rel 4954 df-cnv 4955 df-co 4956 df-dm 4957 df-rn 4958 df-res 4959 df-ima 4960 df-iota 5488 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-isom 5534 df-riota 6160 df-ov 6202 df-oprab 6203 df-mpt2 6204 df-om 6586 df-1st 6686 df-2nd 6687 df-recs 6941 df-rdg 6975 df-1o 7029 df-2o 7030 df-oadd 7033 df-er 7210 df-ec 7212 df-qs 7216 df-map 7325 df-pm 7326 df-en 7420 df-dom 7421 df-sdom 7422 df-fin 7423 df-sup 7801 df-oi 7834 df-card 8219 df-cda 8447 df-pnf 9530 df-mnf 9531 df-xr 9532 df-ltxr 9533 df-le 9534 df-sub 9707 df-neg 9708 df-div 10104 df-nn 10433 df-2 10490 df-3 10491 df-n0 10690 df-z 10757 df-uz 10972 df-rp 11102 df-xadd 11200 df-fz 11554 df-fzo 11665 df-fl 11758 df-mod 11825 df-seq 11923 df-exp 11982 df-hash 12220 df-word 12346 df-lsw 12347 df-concat 12348 df-s1 12349 df-substr 12350 df-reps 12353 df-csh 12543 df-s2 12592 df-cj 12705 df-re 12706 df-im 12707 df-sqr 12841 df-abs 12842 df-clim 13083 df-sum 13281 df-dvds 13653 df-gcd 13808 df-prm 13881 df-phi 13958 df-usgra 23417 df-nbgra 23483 df-wlk 23566 df-trail 23567 df-pth 23568 df-spth 23569 df-wlkon 23572 df-spthon 23575 df-vdgr 23715 df-wwlk 30460 df-wwlkn 30461 df-2wlkonot 30524 df-2spthonot 30526 df-2spthsot 30527 df-clwwlk 30563 df-clwwlkn 30564 df-rgra 30688 df-rusgra 30689 df-frgra 30728

This theorem is referenced by: frgraregord013 30858

W3C validator