clwlkisclwwlklem1 - Metamath Proof Explorer

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

Theorem clwlkisclwwlklem1 24765

Description: Lemma for clwlkisclwwlk 24767. (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 24338	. . . 4 USGrph
2		f1f 5771	. . . 4
3	1, 2	syl 16	. . 3 USGrph
4		lencl 12544	. . . . . . . . . . 11 Word
5		ffn 5721	. . . . . . . . . . 11
6		fz0hash 12481	. . . . . . . . . . 11 $/\$
7	4, 5, 6	syl2an 477	. . . . . . . . . 10 Word $/\$
8		ffz0iswrd 12550	. . . . . . . . . . . . . 14 Word
9		lsw 12567	. . . . . . . . . . . . . . . . . . 19 Word lastS
10	9	ad6antr 735	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
11		oveq1 6288	. . . . . . . . . . . . . . . . . . . 20
12	11	fveq2d 5860	. . . . . . . . . . . . . . . . . . 19
13	12	ad4antlr 732	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
14		eqcom 2452	. . . . . . . . . . . . . . . . . . . . 21
15		nn0cn 10812	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
16		1cnd 9615	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
17	15, 16	pncand 9937	. . . . . . . . . . . . . . . . . . . . . . . . . 26
18	17	eqcomd 2451	. . . . . . . . . . . . . . . . . . . . . . . . 25
19	18	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20	19	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
21	20	eqeq1d 2445	. . . . . . . . . . . . . . . . . . . . . 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 2488	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
27		nn0z 10894	. . . . . . . . . . . . . . . . . . . . . . . . 25
28		peano2zm 10914	. . . . . . . . . . . . . . . . . . . . . . . . 25
29	27, 28	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24
30		nn0re 10811	. . . . . . . . . . . . . . . . . . . . . . . . 25
31	30	lem1d 10486	. . . . . . . . . . . . . . . . . . . . . . . 24
32		eluz2 11098	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
33	29, 27, 31, 32	syl3anbrc 1181	. . . . . . . . . . . . . . . . . . . . . . 23
34	33	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
35		fzoss2 11835	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
36		ssralv 3549	. . . . . . . . . . . . . . . . . . . . . 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 12535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word ..^
41		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
42		fzossrbm1 11836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
43	27, 42	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
44	43	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$ ..^ ..^
45	44	sselda 3489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
46	41, 45	ffvelrnd 6017	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6017	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
54		eqcom 2452	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . . . 23
57	53, 56	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
58	57	ralimdva 2851	. . . . . . . . . . . . . . . . . . . . 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 4441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
65		2re 10612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
67		1red 9614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	66, 67, 30	lesubaddd 10156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
69		2m1e1 10657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	breq1i 4444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		elnnnn0c 10848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
81	79, 80	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
82		fzoend 11885	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
83	81, 82	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
84		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	84	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . . . . 25
86		fveq2 5856	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87		oveq1 6288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	87	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	86, 88	preq12d 4102	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	85, 89	eqeq12d 2465	. . . . . . . . . . . . . . . . . . . . . . . 24
91	90	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
92	83, 91	rspcdv 3199	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
93	15, 16	npcand 9940	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94	93	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
95	94	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
96	95	preq2d 4101	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
97	96	eqeq2d 2457	. . . . . . . . . . . . . . . . . . . . . . 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 6017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
107	106	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
108	38, 107	ffvelrnd 6017	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
109		eqcom 2452	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	109	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	110	eleq1d 2512	. . . . . . . . . . . . . . . . . . . . . . . 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 4095	. . . . . . . . . . . . . . . . . . . . 21
119	118	eleq1d 2512	. . . . . . . . . . . . . . . . . . . 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 1177	. . . . . . . . . . . . . . . 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 1191	1 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1383

wcel 1804

wral 2793

wss 3461

cpr 4016 class class class wbr 4437

cdm 4989

crn 4990

wfn 5573

wf 5574

wf1 5575

cfv 5578 (class class class)co 6281

cr 9494

cc0 9495

c1 9496

caddc 9498

cle 9632

cmin 9810

cn 10543

c2 10592

cn0 10802

cz 10871

cuz 11092

cfz 11683 ..^cfzo 11806

chash 12387 Word cword 12516 lastS clsw 12517 USGrph cusg 24308

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-oadd 7136 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-card 8323 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-nn 10544 df-2 10601 df-n0 10803 df-z 10872 df-uz 11093 df-fz 11684 df-fzo 11807 df-hash 12388 df-word 12524 df-lsw 12525 df-usgra 24311

This theorem is referenced by: clwlkisclwwlklem0 24766 clwlkfclwwlk 24822

W3C validator