numclwlk2lem2f - Metamath Proof Explorer

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

Theorem numclwlk2lem2f 25880

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 10905	. . . . . . . . . 10
2		2nn0 10915	. . . . . . . . . . 11
3	2	a1i 11	. . . . . . . . . 10
4	1, 3	nn0addcld 10958	. . . . . . . . 9
5	4	anim2i 577	. . . . . . . 8 $/\$ $/\$
6	5	3adant1 1032	. . . . . . 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 25878	. . . . . . . 8 $/\$ $/\$
13	12	eleq2d 2525	. . . . . . 7 $/\$ $/\$
14	6, 13	syl 17	. . . . . 6 FriendGrph $/\$ $/\$ $/\$
15		fveq1 5887	. . . . . . . . 9
16	15	eqeq1d 2464	. . . . . . . 8
17		fveq1 5887	. . . . . . . . 9
18	17, 15	neeq12d 2697	. . . . . . . 8
19	16, 18	anbi12d 722	. . . . . . 7 $/\$ $/\$
20	19	elrab 3208	. . . . . 6 $/\$ $/\$ $/\$
21	14, 20	syl6bb 269	. . . . 5 FriendGrph $/\$ $/\$ $/\$ $/\$
22	4	3ad2ant3 1037	. . . . . . . 8 FriendGrph $/\$ $/\$
23	7	numclwwlkfvc 25854	. . . . . . . . 9 ClWWalksN
24	23	eleq2d 2525	. . . . . . . 8 ClWWalksN
25	22, 24	syl 17	. . . . . . 7 FriendGrph $/\$ $/\$ ClWWalksN
26	25	anbi1d 716	. . . . . 6 FriendGrph $/\$ $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$
27		peano2nn 10649	. . . . . . . . . . . . 13
28		nnz 10988	. . . . . . . . . . . . . . . 16
29		2z 10998	. . . . . . . . . . . . . . . . 17
30	29	a1i 11	. . . . . . . . . . . . . . . 16
31	28, 30	zaddcld 11073	. . . . . . . . . . . . . . 15
32		uzid 11202	. . . . . . . . . . . . . . 15
33	31, 32	syl 17	. . . . . . . . . . . . . 14
34		nncn 10645	. . . . . . . . . . . . . . . . 17
35		1cnd 9685	. . . . . . . . . . . . . . . . 17
36	34, 35, 35	addassd 9691	. . . . . . . . . . . . . . . 16
37		1p1e2 10751	. . . . . . . . . . . . . . . . . 18
38	37	a1i 11	. . . . . . . . . . . . . . . . 17
39	38	oveq2d 6331	. . . . . . . . . . . . . . . 16
40	36, 39	eqtrd 2496	. . . . . . . . . . . . . . 15
41	40	fveq2d 5892	. . . . . . . . . . . . . 14
42	33, 41	eleqtrrd 2543	. . . . . . . . . . . . 13
43	27, 42	jca 539	. . . . . . . . . . . 12 $/\$
44	43	3ad2ant3 1037	. . . . . . . . . . 11 FriendGrph $/\$ $/\$ $/\$
45	44	adantr 471	. . . . . . . . . 10 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ $/\$
46		simprl 769	. . . . . . . . . 10 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ ClWWalksN
47		wwlksubclwwlk 25581	. . . . . . . . . 10 $/\$ ClWWalksN substr WWalksN
48	45, 46, 47	sylc 62	. . . . . . . . 9 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN
49		pncan1 10071	. . . . . . . . . . . . . . 15
50	49	eqcomd 2468	. . . . . . . . . . . . . 14
51	34, 50	syl 17	. . . . . . . . . . . . 13
52	51	fveq2d 5892	. . . . . . . . . . . 12 WWalksN WWalksN
53	52	eleq2d 2525	. . . . . . . . . . 11 substr WWalksN substr WWalksN
54	53	3ad2ant3 1037	. . . . . . . . . 10 FriendGrph $/\$ $/\$ substr WWalksN substr WWalksN
55	54	adantr 471	. . . . . . . . 9 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN substr WWalksN
56	48, 55	mpbird 240	. . . . . . . 8 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN
57		clwwlknprop 25549	. . . . . . . . . . . . 13 ClWWalksN $/\$ $/\$ Word $/\$ $/\$
58		simprl 769	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word $/\$ $/\$ $/\$ $/\$
59		simprr 771	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ Word Word
60		peano2nn0 10939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
61	1, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
62		nnre 10644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
63	62	lep1d 10566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
64		elfz2nn0 11914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
65	1, 61, 63, 64	syl3anbrc 1198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
66		2cnd 10710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
67		addsubass 9911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
68		2m1e1 10752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
69	68	oveq2i 6326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	67, 69	syl6eq 2512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
71	34, 66, 35, 70	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
72	71	oveq2d 6331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
73	65, 72	eleqtrrd 2543	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
74		elfzp1b 11900	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
75	28, 31, 74	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76	73, 75	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	76	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word
78		oveq2 6323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
79	78	eleq2d 2525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
80	79	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word
81	77, 80	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ Word
82		swrd0fv0 12833	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ substr
83	59, 81, 82	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ Word substr
84	83	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word substr
85	84	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ Word substr
86	85	impcom 436	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ $/\$ substr
87	86	ad2antrl 739	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
88		simpl 463	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$
89	87, 88	eqtrd 2496	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr
90		swrd0fvlsw 12836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Word $/\$ lastS substr
91	59, 81, 90	syl2anc 671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ Word lastS substr
92	34, 49	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
93	34, 66	pncand 10013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
94	92, 93	eqtr4d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
95	94	fveq2d 5892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
96	95	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ Word
97	91, 96	eqtr2d 2497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ Word lastS substr
98	97	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ Word lastS substr
99	98	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ Word lastS substr
100	99	impcom 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ Word $/\$ $/\$ lastS substr
101	100	neeq1d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ Word $/\$ $/\$ lastS substr
102	101	biimpcd 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ Word $/\$ $/\$ lastS substr
103	102	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ Word $/\$ $/\$ lastS substr
104	103	impcom 436	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
105	104	adantl 472	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
106		neeq2 2699	. . . . . . . . . . . . . . . . . . . . . . . 24 lastS substr lastS substr
107	106	eqcoms 2470	. . . . . . . . . . . . . . . . . . . . . . 23 lastS substr lastS substr
108	107	adantr 471	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr lastS substr
109	105, 108	mpbird 240	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ lastS substr
110	89, 109	jca 539	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
111	58, 110	mpancom 680	. . . . . . . . . . . . . . . . . . 19 $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
112	111	exp31 613	. . . . . . . . . . . . . . . . . 18 $/\$ Word $/\$ $/\$ substr $/\$ lastS substr
113	112	com23 81	. . . . . . . . . . . . . . . . 17 $/\$ Word $/\$ $/\$ substr $/\$ lastS substr
114	113	ex 440	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ substr $/\$ lastS substr
115	114	adantl 472	. . . . . . . . . . . . . . 15 $/\$ Word $/\$ $/\$ substr $/\$ lastS substr
116	115	impcom 436	. . . . . . . . . . . . . 14 Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
117	116	3adant1 1032	. . . . . . . . . . . . 13 $/\$ $/\$ Word $/\$ $/\$ $/\$ $/\$ substr $/\$ lastS substr
118	57, 117	syl 17	. . . . . . . . . . . 12 ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
119	118	imp 435	. . . . . . . . . . 11 ClWWalksN $/\$ $/\$ $/\$ substr $/\$ lastS substr
120	119	com12 32	. . . . . . . . . 10 $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
121	120	3adant1 1032	. . . . . . . . 9 FriendGrph $/\$ $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
122	121	imp 435	. . . . . . . 8 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr $/\$ lastS substr
123	56, 122	jca 539	. . . . . . 7 FriendGrph $/\$ $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
124	123	ex 440	. . . . . 6 FriendGrph $/\$ $/\$ ClWWalksN $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
125	26, 124	sylbid 223	. . . . 5 FriendGrph $/\$ $/\$ $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
126	21, 125	sylbid 223	. . . 4 FriendGrph $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
127	126	imp 435	. . 3 FriendGrph $/\$ $/\$ $/\$ substr WWalksN $/\$ substr $/\$ lastS substr
128	1	anim2i 577	. . . . . . . 8 $/\$ $/\$
129	128	3adant1 1032	. . . . . . 7 FriendGrph $/\$ $/\$ $/\$
130	129	adantr 471	. . . . . 6 FriendGrph $/\$ $/\$ $/\$ $/\$
131	7, 8, 9, 10	numclwwlkovq 25876	. . . . . 6 $/\$ WWalksN $/\$ lastS
132	130, 131	syl 17	. . . . 5 FriendGrph $/\$ $/\$ $/\$ WWalksN $/\$ lastS
133	132	eleq2d 2525	. . . 4 FriendGrph $/\$ $/\$ $/\$ substr substr WWalksN $/\$ lastS
134		fveq1 5887	. . . . . . 7 substr substr
135	134	eqeq1d 2464	. . . . . 6 substr substr
136		fveq2 5888	. . . . . . 7 substr lastS lastS substr
137	136	neeq1d 2695	. . . . . 6 substr lastS lastS substr
138	135, 137	anbi12d 722	. . . . 5 substr $/\$ lastS substr $/\$ lastS substr
139	138	elrab 3208	. . . 4 substr WWalksN $/\$ lastS substr WWalksN $/\$ substr $/\$ lastS substr
140	133, 139	syl6bb 269	. . 3 FriendGrph $/\$ $/\$ $/\$ substr substr WWalksN $/\$ substr $/\$ lastS substr
141	127, 140	mpbird 240	. 2 FriendGrph $/\$ $/\$ $/\$ substr
142		numclwwlk.r	. 2 substr
143	141, 142	fmptd 6069	1 FriendGrph $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

wne 2633

crab 2753

cvv 3057

cop 3986 class class class wbr 4416

cmpt 4475

wf 5597

cfv 5601 (class class class)co 6315

cmpt2 6317

cc 9563

cc0 9565

c1 9566

caddc 9568

cle 9702

cmin 9886

cn 10637

c2 10687

cn0 10898

cz 10966

cuz 11188

cfz 11813

chash 12547 Word cword 12689 lastS clsw 12690 substr csubstr 12693 WWalksN cwwlkn 25455 ClWWalksN cclwwlkn 25526 FriendGrph cfrgra 25765

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4529 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-cnex 9621 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 ax-pre-mulgt0 9642

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-om 6720 df-1st 6820 df-2nd 6821 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-1o 7208 df-oadd 7212 df-er 7389 df-map 7500 df-pm 7501 df-en 7596 df-dom 7597 df-sdom 7598 df-fin 7599 df-card 8399 df-cda 8624 df-pnf 9703 df-mnf 9704 df-xr 9705 df-ltxr 9706 df-le 9707 df-sub 9888 df-neg 9889 df-nn 10638 df-2 10696 df-n0 10899 df-z 10967 df-uz 11189 df-fz 11814 df-fzo 11947 df-hash 12548 df-word 12697 df-lsw 12698 df-substr 12701 df-wwlk 25456 df-wwlkn 25457 df-clwwlk 25528 df-clwwlkn 25529

This theorem is referenced by: numclwlk2lem2f1o 25882

W3C validator