numclwlk2lem2f - Mathbox for Alexander van der Vekens

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

Theorem numclwlk2lem2f 30722

Description: R is a function. (Contributed by Alexander van der Vekens, 5-Oct-2018.)

**Hypotheses**
Ref	Expression
numclwwlk.c	ClWWalksN
numclwwlk.f
numclwwlk.g	$/\$
numclwwlk.q	WWalksN $/\$ lastS
numclwwlk.h	$/\$
numclwwlk.r	substr

**Assertion**
Ref	Expression
numclwlk2lem2f	FriendGrph $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem numclwlk2lem2f**
Step	Hyp	Ref	Expression
1		nnnn0 10607	. . . . . . . . . 10
2		2nn0 10617	. . . . . . . . . . 11
3	2	a1i 11	. . . . . . . . . 10
4	1, 3	nn0addcld 10661	. . . . . . . . 9
5	4	anim2i 569	. . . . . . . 8 $/\$ $/\$
6	5	3adant1 1006	. . . . . . 7 FriendGrph $/\$ $/\$ $/\$
7		numclwwlk.c	. . . . . . . . 9 ClWWalksN
8		numclwwlk.f	. . . . . . . . 9
9		numclwwlk.g	. . . . . . . . 9 $/\$
10		numclwwlk.q	. . . . . . . . 9 WWalksN $/\$ lastS
11		numclwwlk.h	. . . . . . . . 9 $/\$
12	7, 8, 9, 10, 11	numclwwlkovh 30720	. . . . . . . 8 $/\$ $/\$
13	12	eleq2d 2510	. . . . . . 7 $/\$ $/\$
14	6, 13	syl 16	. . . . . 6 FriendGrph $/\$ $/\$ $/\$
15		fveq1 5711	. . . . . . . . 9
16	15	eqeq1d 2451	. . . . . . . 8
17		fveq1 5711	. . . . . . . . 9
18	17, 15	neeq12d 2643	. . . . . . . 8
19	16, 18	anbi12d 710	. . . . . . 7 $/\$ $/\$
20	19	elrab 3138	. . . . . 6 $/\$ $/\$ $/\$
21	14, 20	syl6bb 261	. . . . 5 FriendGrph $/\$ $/\$ $/\$ $/\$
22	4	3ad2ant3 1011	. . . . . . . 8 FriendGrph $/\$ $/\$
23	7	numclwwlkfvc 30696	. . . . . . . . 9 ClWWalksN
24	23	eleq2d 2510	. . . . . . . 8 ClWWalksN
25	22, 24	syl 16	. . . . . . 7 FriendGrph $/\$ $/\$ ClWWalksN
26	25	anbi1d 704	. . . . . 6 FriendGrph $/\$ $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$
27		peano2nn 10355	. . . . . . . . . . . . 13
28		nnz 10689	. . . . . . . . . . . . . . . 16
29		2z 10699	. . . . . . . . . . . . . . . . 17
30	29	a1i 11	. . . . . . . . . . . . . . . 16
31	28, 30	zaddcld 10772	. . . . . . . . . . . . . . 15
32		uzid 10896	. . . . . . . . . . . . . . 15
33	31, 32	syl 16	. . . . . . . . . . . . . 14
34		nncn 10351	. . . . . . . . . . . . . . . . 17
35		ax-1cn 9361	. . . . . . . . . . . . . . . . . 18
36	35	a1i 11	. . . . . . . . . . . . . . . . 17
37	34, 36, 36	addassd 9429	. . . . . . . . . . . . . . . 16
38		1p1e2 10456	. . . . . . . . . . . . . . . . . 18
39	38	a1i 11	. . . . . . . . . . . . . . . . 17
40	39	oveq2d 6128	. . . . . . . . . . . . . . . 16
41	37, 40	eqtrd 2475	. . . . . . . . . . . . . . 15
42	41	fveq2d 5716	. . . . . . . . . . . . . 14
43	33, 42	eleqtrrd 2520	. . . . . . . . . . . . 13
44	27, 43	jca 532	. . . . . . . . . . . 12 $/\$
45	44	3ad2ant3 1011	. . . . . . . . . . 11 FriendGrph $/\$ $/\$ $/\$
46	45	adantr 465	. . . . . . . . . 10 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ $/\$
47		simprl 755	. . . . . . . . . 10 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ ClWWalksN
48		wwlksubclwwlk 30492	. . . . . . . . . 10 $/\$ ClWWalksN substr WWalksN
49	46, 47, 48	sylc 60	. . . . . . . . 9 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN
50		pncan1 9793	. . . . . . . . . . . . . . 15
51	50	eqcomd 2448	. . . . . . . . . . . . . 14
52	34, 51	syl 16	. . . . . . . . . . . . 13
53	52	fveq2d 5716	. . . . . . . . . . . 12 WWalksN WWalksN
54	53	eleq2d 2510	. . . . . . . . . . 11 substr WWalksN substr WWalksN
55	54	3ad2ant3 1011	. . . . . . . . . 10 FriendGrph $/\$ $/\$ substr WWalksN substr WWalksN
56	55	adantr 465	. . . . . . . . 9 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN substr WWalksN
57	49, 56	mpbird 232	. . . . . . . 8 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN
58		clwwlknprop 30461	. . . . . . . . . . . . 13 ClWWalksN $/\$ $/\$ Word $/\$ $/\$
59		simprl 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ $/\$ $/\$ $/\$
60		simprr 756	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ Word Word
61		peano2nn0 10641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
62	1, 61	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63		nnre 10350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	lep1d 10285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		elfz2nn0 11501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
66	1, 62, 64, 65	syl3anbrc 1172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
67		2cnd 10415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
68		addsubass 9641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
69		2m1e1 10457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
70	69	oveq2i 6123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
71	68, 70	syl6eq 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
72	34, 67, 36, 71	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	72	oveq2d 6128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74	66, 73	eleqtrrd 2520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75		elfzp1b 11558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
76	28, 31, 75	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
77	74, 76	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
78	77	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word
79		oveq2 6120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
80	79	eleq2d 2510	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
81	80	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word
82	78, 81	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ Word
83		swrd0fv0 12357	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ substr
84	60, 82, 83	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ Word substr
85	84	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word substr
86	85	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ Word substr
87	86	impcom 430	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ $/\$ substr
88	87	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
89		simpl 457	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
90	88, 89	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
91		swrd0fvlsw 12360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word $/\$ lastS substr
92	60, 82, 91	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ Word lastS substr
93	34, 50	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
94	34, 67	pncand 9741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
95	93, 94	eqtr4d 2478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
96	95	fveq2d 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97	96	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ Word
98	92, 97	eqtr2d 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ Word lastS substr
99	98	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word lastS substr
100	99	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word lastS substr
101	100	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ lastS substr
102	101	neeq1d 2641	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Word $/\$ $/\$ lastS substr
103	102	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word $/\$ $/\$ lastS substr
104	103	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ Word $/\$ $/\$ lastS substr
105	104	impcom 430	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
106	105	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
107		neeq2 2646	. . . . . . . . . . . . . . . . . . . . . . . 24 lastS substr lastS substr
108	107	eqcoms 2446	. . . . . . . . . . . . . . . . . . . . . . 23 lastS substr lastS substr
109	108	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr lastS substr
110	106, 109	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
111	90, 110	jca 532	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
112	59, 111	mpancom 669	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
113	112	exp31 604	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ $/\$ substr $/\$ lastS substr
114	113	com23 78	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ $/\$ substr $/\$ lastS substr
115	114	ex 434	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ substr $/\$ lastS substr
116	115	adantl 466	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ $/\$ substr $/\$ lastS substr
117	116	impcom 430	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
118	117	3adant1 1006	. . . . . . . . . . . . 13 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
119	58, 118	syl 16	. . . . . . . . . . . 12 ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
120	119	imp 429	. . . . . . . . . . 11 ClWWalksN $/\$ $/\$ $/\$ substr $/\$ lastS substr
121	120	com12 31	. . . . . . . . . 10 $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
122	121	3adant1 1006	. . . . . . . . 9 FriendGrph $/\$ $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
123	122	imp 429	. . . . . . . 8 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
124	57, 123	jca 532	. . . . . . 7 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
125	124	ex 434	. . . . . 6 FriendGrph $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
126	26, 125	sylbid 215	. . . . 5 FriendGrph $/\$ $/\$ $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
127	21, 126	sylbid 215	. . . 4 FriendGrph $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
128	127	imp 429	. . 3 FriendGrph $/\$ $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
129	1	anim2i 569	. . . . . . . 8 $/\$ $/\$
130	129	3adant1 1006	. . . . . . 7 FriendGrph $/\$ $/\$ $/\$
131	130	adantr 465	. . . . . 6 FriendGrph $/\$ $/\$ $/\$ $/\$
132	7, 8, 9, 10	numclwwlkovq 30718	. . . . . 6 $/\$ WWalksN $/\$ lastS
133	131, 132	syl 16	. . . . 5 FriendGrph $/\$ $/\$ $/\$ WWalksN $/\$ lastS
134	133	eleq2d 2510	. . . 4 FriendGrph $/\$ $/\$ $/\$ substr substr WWalksN $/\$ lastS
135		fveq1 5711	. . . . . . 7 substr substr
136	135	eqeq1d 2451	. . . . . 6 substr substr
137		fveq2 5712	. . . . . . 7 substr lastS lastS substr
138	137	neeq1d 2641	. . . . . 6 substr lastS lastS substr
139	136, 138	anbi12d 710	. . . . 5 substr $/\$ lastS substr $/\$ lastS substr
140	139	elrab 3138	. . . 4 substr WWalksN $/\$ lastS substr WWalksN $/\$ substr $/\$ lastS substr
141	134, 140	syl6bb 261	. . 3 FriendGrph $/\$ $/\$ $/\$ substr substr WWalksN $/\$ substr $/\$ lastS substr
142	128, 141	mpbird 232	. 2 FriendGrph $/\$ $/\$ $/\$ substr
143		numclwwlk.r	. 2 substr
144	142, 143	fmptd 5888	1 FriendGrph $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wne 2620

crab 2740

cvv 2993

cop 3904 class class class wbr 4313

cmpt 4371

wf 5435

cfv 5439 (class class class)co 6112

cmpt2 6114

cc 9301

cc0 9303

c1 9304

caddc 9306

cle 9440

cmin 9616

cn 10343

c2 10392

cn0 10600

cz 10667

cuz 10882

cfz 11458

chash 12124 Word cword 12242 lastS clsw 12243 substr csubstr 12246 WWalksN cwwlkn 30338 ClWWalksN cclwwlkn 30440 FriendGrph cfrgra 30606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4424 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393 ax-cnex 9359 ax-resscn 9360 ax-1cn 9361 ax-icn 9362 ax-addcl 9363 ax-addrcl 9364 ax-mulcl 9365 ax-mulrcl 9366 ax-mulcom 9367 ax-addass 9368 ax-mulass 9369 ax-distr 9370 ax-i2m1 9371 ax-1ne0 9372 ax-1rid 9373 ax-rnegex 9374 ax-rrecex 9375 ax-cnre 9376 ax-pre-lttri 9377 ax-pre-lttrn 9378 ax-pre-ltadd 9379 ax-pre-mulgt0 9380

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-pss 3365 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-tp 3903 df-op 3905 df-uni 4113 df-int 4150 df-iun 4194 df-br 4314 df-opab 4372 df-mpt 4373 df-tr 4407 df-eprel 4653 df-id 4657 df-po 4662 df-so 4663 df-fr 4700 df-we 4702 df-ord 4743 df-on 4744 df-lim 4745 df-suc 4746 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-riota 6073 df-ov 6115 df-oprab 6116 df-mpt2 6117 df-om 6498 df-1st 6598 df-2nd 6599 df-recs 6853 df-rdg 6887 df-1o 6941 df-oadd 6945 df-er 7122 df-map 7237 df-pm 7238 df-en 7332 df-dom 7333 df-sdom 7334 df-fin 7335 df-card 8130 df-pnf 9441 df-mnf 9442 df-xr 9443 df-ltxr 9444 df-le 9445 df-sub 9618 df-neg 9619 df-nn 10344 df-2 10401 df-n0 10601 df-z 10668 df-uz 10883 df-fz 11459 df-fzo 11570 df-hash 12125 df-word 12250 df-lsw 12251 df-substr 12254 df-wwlk 30339 df-wwlkn 30340 df-clwwlk 30442 df-clwwlkn 30443

This theorem is referenced by: numclwlk2lem2f1o 30724

W3C validator