clwlkisclwwlklem1 - Metamath Proof Explorer

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

Theorem clwlkisclwwlklem1 24451

Description: Lemma for clwlkisclwwlk 24453. (Contributed by Alexander van der Vekens, 22-Jun-2018.)

**Assertion**
Ref	Expression
clwlkisclwwlklem1	USGrph $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$

Distinct variable groups:

**Proof of Theorem clwlkisclwwlklem1**
Step	Hyp	Ref	Expression
1		usgraf1 24025	. . . 4 USGrph
2		f1f 5774	. . . 4
3	1, 2	syl 16	. . 3 USGrph
4		lencl 12517	. . . . . . . . . . 11 Word
5		ffn 5724	. . . . . . . . . . 11
6		fz0hash 12454	. . . . . . . . . . 11 $/\$
7	4, 5, 6	syl2an 477	. . . . . . . . . 10 Word $/\$
8		ffz0iswrd 12523	. . . . . . . . . . . . . 14 Word
9		lsw 12539	. . . . . . . . . . . . . . . . . . 19 Word lastS
10	9	ad6antr 735	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
11		oveq1 6284	. . . . . . . . . . . . . . . . . . . 20
12	11	fveq2d 5863	. . . . . . . . . . . . . . . . . . 19
13	12	ad4antlr 732	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
14		eqcom 2471	. . . . . . . . . . . . . . . . . . . . 21
15		nn0cn 10796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
16		1cnd 9603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
17	15, 16	pncand 9922	. . . . . . . . . . . . . . . . . . . . . . . . . 26
18	17	eqcomd 2470	. . . . . . . . . . . . . . . . . . . . . . . . 25
19	18	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20	19	fveq2d 5863	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
21	20	eqeq1d 2464	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
22	21	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
23	14, 22	syl5bi 217	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
24	23	adantld 467	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ $/\$
25	24	imp 429	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
26	10, 13, 25	3eqtrd 2507	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
27		nn0z 10878	. . . . . . . . . . . . . . . . . . . . . . . . 25
28		peano2zm 10897	. . . . . . . . . . . . . . . . . . . . . . . . 25
29	27, 28	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24
30		nn0re 10795	. . . . . . . . . . . . . . . . . . . . . . . . 25
31	30	lem1d 10470	. . . . . . . . . . . . . . . . . . . . . . . 24
32		eluz2 11079	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
33	29, 27, 31, 32	syl3anbrc 1175	. . . . . . . . . . . . . . . . . . . . . . 23
34	33	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
35		fzoss2 11812	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
36		ssralv 3559	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^ ..^ ..^
37	34, 35, 36	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
38		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
39	38	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
40		wrdf 12508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word ..^
41		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
42		fzossrbm1 11813	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
43	27, 42	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
44	43	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$ ..^ ..^
45	44	sselda 3499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
46	41, 45	ffvelrnd 6015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ $/\$ $/\$ ..^
47	46	exp31 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
48	40, 47	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^
49	48	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word ..^
50	49	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ ..^
51	50	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
52	51	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
53	39, 52	ffvelrnd 6015	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
54		eqcom 2471	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	eleq1d 2531	. . . . . . . . . . . . . . . . . . . . . . 23
57	53, 56	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
58	57	ralimdva 2867	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
59	37, 58	syld 44	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
60	59	com12 31	. . . . . . . . . . . . . . . . . . 19 ..^ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
61	60	adantr 465	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
62	61	impcom 430	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ ..^
63		breq2 4446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
65		2re 10596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
67		1red 9602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	66, 67, 30	lesubaddd 10140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
69		2m1e1 10641	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	breq1i 4449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		elnnnn0c 10832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
72	71	simplbi2 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74	68, 73	sylbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	74	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$
76	75	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
77	64, 76	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$
78	77	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
79	78	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
80		lbfzo0 11821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
81	79, 80	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
82		fzoend 11862	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
83	81, 82	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
84		fveq2 5859	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	84	fveq2d 5863	. . . . . . . . . . . . . . . . . . . . . . . . 25
86		fveq2 5859	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	87	fveq2d 5863	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	86, 88	preq12d 4109	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	85, 89	eqeq12d 2484	. . . . . . . . . . . . . . . . . . . . . . . 24
91	90	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
92	83, 91	rspcdv 3212	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
93	15, 16	npcand 9925	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94	93	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
95	94	fveq2d 5863	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
96	95	preq2d 4108	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
97	96	eqeq2d 2476	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
98	40	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
99	74	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100	63, 99	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
101	100	com3r 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102	101	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word $/\$ Word $/\$
103	102	imp31 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$ $/\$ $/\$
104	103, 80	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$ $/\$ ..^
105	104, 82	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
106	98, 105	ffvelrnd 6015	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
107	106	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
108	38, 107	ffvelrnd 6015	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
109		eqcom 2471	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	109	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	110	eleq1d 2531	. . . . . . . . . . . . . . . . . . . . . . . 24
112	108, 111	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
113	97, 112	sylbid 215	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
114	92, 113	syld 44	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
115	114	com12 31	. . . . . . . . . . . . . . . . . . . 20 ..^ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
116	115	adantr 465	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
117	116	impcom 430	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
118		preq2 4102	. . . . . . . . . . . . . . . . . . . . 21
119	118	eleq1d 2531	. . . . . . . . . . . . . . . . . . . 20
120	119	adantl 466	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
121	120	adantl 466	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
122	117, 121	mpbird 232	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
123	26, 62, 122	3jca 1171	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
124	123	exp41 610	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
125	124	exp41 610	. . . . . . . . . . . . . 14 Word Word ..^ $/\$ lastS $/\$ ..^ $/\$
126	8, 125	syl 16	. . . . . . . . . . . . 13 Word ..^ $/\$ lastS $/\$ ..^ $/\$
127	126	com13 80	. . . . . . . . . . . 12 Word ..^ $/\$ lastS $/\$ ..^ $/\$
128	4, 127	mpcom 36	. . . . . . . . . . 11 Word ..^ $/\$ lastS $/\$ ..^ $/\$
129	128	imp 429	. . . . . . . . . 10 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
130	7, 129	mpd 15	. . . . . . . . 9 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
131	130	expcom 435	. . . . . . . 8 Word ..^ $/\$ lastS $/\$ ..^ $/\$
132	131	com14 88	. . . . . . 7 Word ..^ $/\$ lastS $/\$ ..^ $/\$
133	132	imp 429	. . . . . 6 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
134	133	com13 80	. . . . 5 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
135	134	imp 429	. . . 4 $/\$ $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
136	135	com12 31	. . 3 $/\$ Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
137	3, 136	sylan 471	. 2 USGrph $/\$ Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
138	137	3imp 1185	1 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1374

wcel 1762

wral 2809

wss 3471

cpr 4024 class class class wbr 4442

cdm 4994

crn 4995

wfn 5576

wf 5577

wf1 5578

cfv 5581 (class class class)co 6277

cr 9482

cc0 9483

c1 9484

caddc 9486

cle 9620

cmin 9796

cn 10527

c2 10576

cn0 10786

cz 10855

cuz 11073

cfz 11663 ..^cfzo 11783

chash 12362 Word cword 12489 lastS clsw 12490 USGrph cusg 23995

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 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1963 ax-ext 2440 ax-rep 4553 ax-sep 4563 ax-nul 4571 ax-pow 4620 ax-pr 4681 ax-un 6569 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2274 df-mo 2275 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2612 df-ne 2659 df-nel 2660 df-ral 2814 df-rex 2815 df-reu 2816 df-rab 2818 df-v 3110 df-sbc 3327 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3781 df-if 3935 df-pw 4007 df-sn 4023 df-pr 4025 df-tp 4027 df-op 4029 df-uni 4241 df-int 4278 df-iun 4322 df-br 4443 df-opab 4501 df-mpt 4502 df-tr 4536 df-eprel 4786 df-id 4790 df-po 4795 df-so 4796 df-fr 4833 df-we 4835 df-ord 4876 df-on 4877 df-lim 4878 df-suc 4879 df-xp 5000 df-rel 5001 df-cnv 5002 df-co 5003 df-dm 5004 df-rn 5005 df-res 5006 df-ima 5007 df-iota 5544 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6674 df-1st 6776 df-2nd 6777 df-recs 7034 df-rdg 7068 df-1o 7122 df-oadd 7126 df-er 7303 df-en 7509 df-dom 7510 df-sdom 7511 df-fin 7512 df-card 8311 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9798 df-neg 9799 df-nn 10528 df-2 10585 df-n0 10787 df-z 10856 df-uz 11074 df-fz 11664 df-fzo 11784 df-hash 12363 df-word 12497 df-lsw 12498 df-usgra 23998

This theorem is referenced by: clwlkisclwwlklem0 24452 clwlkfclwwlk 24508

W3C validator