clwlkisclwwlklem1 - Metamath Proof Explorer

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

Theorem clwlkisclwwlklem1 25515

Description: Lemma for clwlkisclwwlk 25517. (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 25087	. . . 4 USGrph
2		f1f 5779	. . . 4
3	1, 2	syl 17	. . 3 USGrph
4		lencl 12687	. . . . . . . . . . 11 Word
5		ffn 5728	. . . . . . . . . . 11
6		fz0hash 12613	. . . . . . . . . . 11 $/\$
7	4, 5, 6	syl2an 480	. . . . . . . . . 10 Word $/\$
8		ffz0iswrd 12694	. . . . . . . . . . . . . 14 Word
9		lsw 12711	. . . . . . . . . . . . . . . . . . 19 Word lastS
10	9	ad6antr 742	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
11		oveq1 6297	. . . . . . . . . . . . . . . . . . . 20
12	11	fveq2d 5869	. . . . . . . . . . . . . . . . . . 19
13	12	ad4antlr 739	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
14		eqcom 2458	. . . . . . . . . . . . . . . . . . . . 21
15		nn0cn 10879	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
16		1cnd 9659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
17	15, 16	pncand 9987	. . . . . . . . . . . . . . . . . . . . . . . . . 26
18	17	eqcomd 2457	. . . . . . . . . . . . . . . . . . . . . . . . 25
19	18	ad4antlr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20	19	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
21	20	eqeq1d 2453	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
22	21	biimpd 211	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
23	14, 22	syl5bi 221	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
24	23	adantld 469	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ $/\$
25	24	imp 431	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
26	10, 13, 25	3eqtrd 2489	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
27		nn0z 10960	. . . . . . . . . . . . . . . . . . . . . . . . 25
28		peano2zm 10980	. . . . . . . . . . . . . . . . . . . . . . . . 25
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
30		nn0re 10878	. . . . . . . . . . . . . . . . . . . . . . . . 25
31	30	lem1d 10540	. . . . . . . . . . . . . . . . . . . . . . . 24
32		eluz2 11165	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
33	29, 27, 31, 32	syl3anbrc 1192	. . . . . . . . . . . . . . . . . . . . . . 23
34	33	ad4antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
35		fzoss2 11946	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
36		ssralv 3493	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^ ..^ ..^
37	34, 35, 36	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
38		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
39	38	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
40		wrdf 12676	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word ..^
41		simpll 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
42		fzossrbm1 11947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
43	27, 42	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
44	43	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$ ..^ ..^
45	44	sselda 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
46	41, 45	ffvelrnd 6023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ $/\$ $/\$ ..^
47	46	exp31 609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
48	40, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^
49	48	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word ..^
50	49	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ ..^
51	50	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
52	51	imp 431	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
53	39, 52	ffvelrnd 6023	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
54		eqcom 2458	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . 23
57	53, 56	syl5ibrcom 226	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
58	57	ralimdva 2796	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
59	37, 58	syld 45	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
60	59	com12 32	. . . . . . . . . . . . . . . . . . 19 ..^ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
61	60	adantr 467	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
62	61	impcom 432	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ ..^
63		breq2 4406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
65		2re 10679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
67		1red 9658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	66, 67, 30	lesubaddd 10210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
69		2m1e1 10724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	breq1i 4409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		elnnnn0c 10915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
72	71	simplbi2 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	syl5bi 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74	68, 73	sylbird 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	74	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$
76	75	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
77	64, 76	sylbid 219	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$
78	77	imp 431	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
79	78	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
80		lbfzo0 11955	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
81	79, 80	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
82		fzoend 12002	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
84		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	84	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . . . 25
86		fveq2 5865	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87		oveq1 6297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	87	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	86, 88	preq12d 4059	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	85, 89	eqeq12d 2466	. . . . . . . . . . . . . . . . . . . . . . . 24
91	90	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
92	83, 91	rspcdv 3153	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
93	15, 16	npcand 9990	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94	93	ad4antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
95	94	fveq2d 5869	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
96	95	preq2d 4058	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
97	96	eqeq2d 2461	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
98	40	ad4antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
99	74	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100	63, 99	syl6bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
101	100	com3r 82	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102	101	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word $/\$ Word $/\$
103	102	imp31 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$ $/\$ $/\$
104	103, 80	sylibr 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$ $/\$ ..^
105	104, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
106	98, 105	ffvelrnd 6023	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
107	106	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
108	38, 107	ffvelrnd 6023	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
109		eqcom 2458	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	109	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	110	eleq1d 2513	. . . . . . . . . . . . . . . . . . . . . . . 24
112	108, 111	syl5ibrcom 226	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
113	97, 112	sylbid 219	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
114	92, 113	syld 45	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
115	114	com12 32	. . . . . . . . . . . . . . . . . . . 20 ..^ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
116	115	adantr 467	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
117	116	impcom 432	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
118		preq2 4052	. . . . . . . . . . . . . . . . . . . . 21
119	118	eleq1d 2513	. . . . . . . . . . . . . . . . . . . 20
120	119	adantl 468	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
121	120	adantl 468	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
122	117, 121	mpbird 236	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
123	26, 62, 122	3jca 1188	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
124	123	exp41 615	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
125	124	exp41 615	. . . . . . . . . . . . . 14 Word Word ..^ $/\$ lastS $/\$ ..^ $/\$
126	8, 125	syl 17	. . . . . . . . . . . . 13 Word ..^ $/\$ lastS $/\$ ..^ $/\$
127	126	com13 83	. . . . . . . . . . . 12 Word ..^ $/\$ lastS $/\$ ..^ $/\$
128	4, 127	mpcom 37	. . . . . . . . . . 11 Word ..^ $/\$ lastS $/\$ ..^ $/\$
129	128	imp 431	. . . . . . . . . 10 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
130	7, 129	mpd 15	. . . . . . . . 9 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
131	130	expcom 437	. . . . . . . 8 Word ..^ $/\$ lastS $/\$ ..^ $/\$
132	131	com14 91	. . . . . . 7 Word ..^ $/\$ lastS $/\$ ..^ $/\$
133	132	imp 431	. . . . . 6 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
134	133	com13 83	. . . . 5 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
135	134	imp 431	. . . 4 $/\$ $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
136	135	com12 32	. . 3 $/\$ Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
137	3, 136	sylan 474	. 2 USGrph $/\$ Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
138	137	3imp 1202	1 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $/\$ wa 371 $/\$ w3a 985

wceq 1444

wcel 1887

wral 2737

wss 3404

cpr 3970 class class class wbr 4402

cdm 4834

crn 4835

wfn 5577

wf 5578

wf1 5579

cfv 5582 (class class class)co 6290

cr 9538

cc0 9539

c1 9540

caddc 9542

cle 9676

cmin 9860

cn 10609

c2 10659

cn0 10869

cz 10937

cuz 11159

cfz 11784 ..^cfzo 11915

chash 12515 Word cword 12656 lastS clsw 12657 USGrph cusg 25057

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-card 8373 df-cda 8598 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-2 10668 df-n0 10870 df-z 10938 df-uz 11160 df-fz 11785 df-fzo 11916 df-hash 12516 df-word 12664 df-lsw 12665 df-usgra 25060

This theorem is referenced by: clwlkisclwwlklem0 25516 clwlkfclwwlk 25572

W3C validator