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 30621

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 10582	. . . . . . . . . 10
2		2nn0 10592	. . . . . . . . . . 11
3	2	a1i 11	. . . . . . . . . 10
4	1, 3	nn0addcld 10636	. . . . . . . . 9
5	4	anim2i 566	. . . . . . . 8 $/\$ $/\$
6	5	3adant1 1001	. . . . . . 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 30619	. . . . . . . 8 $/\$ $/\$
13	12	eleq2d 2508	. . . . . . 7 $/\$ $/\$
14	6, 13	syl 16	. . . . . 6 FriendGrph $/\$ $/\$ $/\$
15		fveq1 5687	. . . . . . . . 9
16	15	eqeq1d 2449	. . . . . . . 8
17		fveq1 5687	. . . . . . . . 9
18	17, 15	neeq12d 2621	. . . . . . . 8
19	16, 18	anbi12d 705	. . . . . . 7 $/\$ $/\$
20	19	elrab 3114	. . . . . 6 $/\$ $/\$ $/\$
21	14, 20	syl6bb 261	. . . . 5 FriendGrph $/\$ $/\$ $/\$ $/\$
22	4	3ad2ant3 1006	. . . . . . . 8 FriendGrph $/\$ $/\$
23	7	numclwwlkfvc 30595	. . . . . . . . 9 ClWWalksN
24	23	eleq2d 2508	. . . . . . . 8 ClWWalksN
25	22, 24	syl 16	. . . . . . 7 FriendGrph $/\$ $/\$ ClWWalksN
26	25	anbi1d 699	. . . . . 6 FriendGrph $/\$ $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$
27		peano2nn 10330	. . . . . . . . . . . . 13
28		nnz 10664	. . . . . . . . . . . . . . . 16
29		2z 10674	. . . . . . . . . . . . . . . . 17
30	29	a1i 11	. . . . . . . . . . . . . . . 16
31	28, 30	zaddcld 10747	. . . . . . . . . . . . . . 15
32		uzid 10871	. . . . . . . . . . . . . . 15
33	31, 32	syl 16	. . . . . . . . . . . . . 14
34		nncn 10326	. . . . . . . . . . . . . . . . 17
35		ax-1cn 9336	. . . . . . . . . . . . . . . . . 18
36	35	a1i 11	. . . . . . . . . . . . . . . . 17
37	34, 36, 36	addassd 9404	. . . . . . . . . . . . . . . 16
38		1p1e2 10431	. . . . . . . . . . . . . . . . . 18
39	38	a1i 11	. . . . . . . . . . . . . . . . 17
40	39	oveq2d 6106	. . . . . . . . . . . . . . . 16
41	37, 40	eqtrd 2473	. . . . . . . . . . . . . . 15
42	41	fveq2d 5692	. . . . . . . . . . . . . 14
43	33, 42	eleqtrrd 2518	. . . . . . . . . . . . 13
44	27, 43	jca 529	. . . . . . . . . . . 12 $/\$
45	44	3ad2ant3 1006	. . . . . . . . . . 11 FriendGrph $/\$ $/\$ $/\$
46	45	adantr 462	. . . . . . . . . 10 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ $/\$
47		simprl 750	. . . . . . . . . 10 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ ClWWalksN
48		wwlksubclwwlk 30391	. . . . . . . . . 10 $/\$ ClWWalksN substr WWalksN
49	46, 47, 48	sylc 60	. . . . . . . . 9 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN
50		pncan1 9768	. . . . . . . . . . . . . . 15
51	50	eqcomd 2446	. . . . . . . . . . . . . 14
52	34, 51	syl 16	. . . . . . . . . . . . 13
53	52	fveq2d 5692	. . . . . . . . . . . 12 WWalksN WWalksN
54	53	eleq2d 2508	. . . . . . . . . . 11 substr WWalksN substr WWalksN
55	54	3ad2ant3 1006	. . . . . . . . . 10 FriendGrph $/\$ $/\$ substr WWalksN substr WWalksN
56	55	adantr 462	. . . . . . . . 9 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN substr WWalksN
57	49, 56	mpbird 232	. . . . . . . 8 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN
58		clwwlknprop 30360	. . . . . . . . . . . . 13 ClWWalksN $/\$ $/\$ Word $/\$ $/\$
59		simprl 750	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ $/\$ $/\$ $/\$
60		simprr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ Word Word
61		peano2nn0 10616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
62	1, 61	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
63		nnre 10325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
64	63	lep1d 10260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
65		elfz2nn0 11476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
66	1, 62, 64, 65	syl3anbrc 1167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
67		2cnd 10390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
68		addsubass 9616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
69		2m1e1 10432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
70	69	oveq2i 6101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
71	68, 70	syl6eq 2489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
72	34, 67, 36, 71	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	72	oveq2d 6106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74	66, 73	eleqtrrd 2518	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75		elfzp1b 11533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
76	28, 31, 75	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
77	74, 76	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
78	77	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word
79		oveq2 6098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
80	79	eleq2d 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
81	80	ad2antrl 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word
82	78, 81	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ Word
83		swrd0fv0 12332	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ substr
84	60, 82, 83	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ Word substr
85	84	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word substr
86	85	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ Word substr
87	86	impcom 430	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ $/\$ substr
88	87	ad2antrl 722	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
89		simpl 454	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
90	88, 89	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
91		swrd0fvlsw 12335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word $/\$ lastS substr
92	60, 82, 91	syl2anc 656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ Word lastS substr
93	34, 50	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
94	34, 67	pncand 9716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
95	93, 94	eqtr4d 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
96	95	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
97	96	adantr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ Word
98	92, 97	eqtr2d 2474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ Word lastS substr
99	98	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word lastS substr
100	99	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word lastS substr
101	100	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ lastS substr
102	101	neeq1d 2619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Word $/\$ $/\$ lastS substr
103	102	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word $/\$ $/\$ lastS substr
104	103	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ Word $/\$ $/\$ lastS substr
105	104	impcom 430	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
106	105	adantl 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
107		neeq2 2615	. . . . . . . . . . . . . . . . . . . . . . . 24 lastS substr lastS substr
108	107	eqcoms 2444	. . . . . . . . . . . . . . . . . . . . . . 23 lastS substr lastS substr
109	108	adantr 462	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr lastS substr
110	106, 109	mpbird 232	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
111	90, 110	jca 529	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
112	59, 111	mpancom 664	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
113	112	exp31 601	. . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ $/\$ substr $/\$ lastS substr
117	116	impcom 430	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
118	117	3adant1 1001	. . . . . . . . . . . . 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 1001	. . . . . . . . 9 FriendGrph $/\$ $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
123	122	imp 429	. . . . . . . 8 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
124	57, 123	jca 529	. . . . . . 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 566	. . . . . . . 8 $/\$ $/\$
130	129	3adant1 1001	. . . . . . 7 FriendGrph $/\$ $/\$ $/\$
131	130	adantr 462	. . . . . 6 FriendGrph $/\$ $/\$ $/\$ $/\$
132	7, 8, 9, 10	numclwwlkovq 30617	. . . . . 6 $/\$ WWalksN $/\$ lastS
133	131, 132	syl 16	. . . . 5 FriendGrph $/\$ $/\$ $/\$ WWalksN $/\$ lastS
134	133	eleq2d 2508	. . . 4 FriendGrph $/\$ $/\$ $/\$ substr substr WWalksN $/\$ lastS
135		fveq1 5687	. . . . . . 7 substr substr
136	135	eqeq1d 2449	. . . . . 6 substr substr
137		fveq2 5688	. . . . . . 7 substr lastS lastS substr
138	137	neeq1d 2619	. . . . . 6 substr lastS lastS substr
139	136, 138	anbi12d 705	. . . . 5 substr $/\$ lastS substr $/\$ lastS substr
140	139	elrab 3114	. . . 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 5864	1 FriendGrph $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1364

wcel 1761

wne 2604

crab 2717

cvv 2970

cop 3880 class class class wbr 4289

cmpt 4347

wf 5411

cfv 5415 (class class class)co 6090

cmpt2 6092

cc 9276

cc0 9278

c1 9279

caddc 9281

cle 9415

cmin 9591

cn 10318

c2 10367

cn0 10575

cz 10642

cuz 10857

cfz 11433

chash 12099 Word cword 12217 lastS clsw 12218 substr csubstr 12221 WWalksN cwwlkn 30237 ClWWalksN cclwwlkn 30339 FriendGrph cfrgra 30505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-oadd 6920 df-er 7097 df-map 7212 df-pm 7213 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-card 8105 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-nn 10319 df-2 10376 df-n0 10576 df-z 10643 df-uz 10858 df-fz 11434 df-fzo 11545 df-hash 12100 df-word 12225 df-lsw 12226 df-substr 12229 df-wwlk 30238 df-wwlkn 30239 df-clwwlk 30341 df-clwwlkn 30342

This theorem is referenced by: numclwlk2lem2f1o 30623

W3C validator