clwlkisclwwlklem1 - Metamath Proof Explorer

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

Theorem clwlkisclwwlklem1 25191

Description: Lemma for clwlkisclwwlk 25193. (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 24764	. . . 4 USGrph
2		f1f 5763	. . . 4
3	1, 2	syl 17	. . 3 USGrph
4		lencl 12612	. . . . . . . . . . 11 Word
5		ffn 5713	. . . . . . . . . . 11
6		fz0hash 12546	. . . . . . . . . . 11 $/\$
7	4, 5, 6	syl2an 475	. . . . . . . . . 10 Word $/\$
8		ffz0iswrd 12619	. . . . . . . . . . . . . 14 Word
9		lsw 12636	. . . . . . . . . . . . . . . . . . 19 Word lastS
10	9	ad6antr 734	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
11		oveq1 6284	. . . . . . . . . . . . . . . . . . . 20
12	11	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19
13	12	ad4antlr 731	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
14		eqcom 2411	. . . . . . . . . . . . . . . . . . . . 21
15		nn0cn 10845	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
16		1cnd 9641	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
17	15, 16	pncand 9967	. . . . . . . . . . . . . . . . . . . . . . . . . 26
18	17	eqcomd 2410	. . . . . . . . . . . . . . . . . . . . . . . . 25
19	18	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
20	19	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
21	20	eqeq1d 2404	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
22	21	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
23	14, 22	syl5bi 217	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
24	23	adantld 465	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ $/\$
25	24	imp 427	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
26	10, 13, 25	3eqtrd 2447	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
27		nn0z 10927	. . . . . . . . . . . . . . . . . . . . . . . . 25
28		peano2zm 10947	. . . . . . . . . . . . . . . . . . . . . . . . 25
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
30		nn0re 10844	. . . . . . . . . . . . . . . . . . . . . . . . 25
31	30	lem1d 10518	. . . . . . . . . . . . . . . . . . . . . . . 24
32		eluz2 11132	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
33	29, 27, 31, 32	syl3anbrc 1181	. . . . . . . . . . . . . . . . . . . . . . 23
34	33	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
35		fzoss2 11883	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
36		ssralv 3502	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^ ..^ ..^
37	34, 35, 36	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
38		simpr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
39	38	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
40		wrdf 12601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word ..^
41		simpll 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
42		fzossrbm1 11884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ..^ ..^
43	27, 42	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
44	43	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$ ..^ ..^
45	44	sselda 3441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
46	41, 45	ffvelrnd 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ $/\$ $/\$ ..^
47	46	exp31 602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
48	40, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word ..^
49	48	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word ..^
50	49	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ ..^
51	50	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
52	51	imp 427	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
53	39, 52	ffvelrnd 6009	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
54		eqcom 2411	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	eleq1d 2471	. . . . . . . . . . . . . . . . . . . . . . 23
57	53, 56	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
58	57	ralimdva 2811	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
59	37, 58	syld 42	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
60	59	com12 29	. . . . . . . . . . . . . . . . . . 19 ..^ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
61	60	adantr 463	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
62	61	impcom 428	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ ..^
63		breq2 4398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
65		2re 10645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
67		1red 9640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	66, 67, 30	lesubaddd 10188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
69		2m1e1 10690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
70	69	breq1i 4401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
71		elnnnn0c 10881	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
72	71	simplbi2 623	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
73	70, 72	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
74	68, 73	sylbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
75	74	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$
76	75	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
77	64, 76	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$
78	77	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
79	78	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
80		lbfzo0 11892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
81	79, 80	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
82		fzoend 11938	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
83	81, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
84		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . 26
85	84	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . 25
86		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . 26
87		oveq1 6284	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
88	87	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . 26
89	86, 88	preq12d 4058	. . . . . . . . . . . . . . . . . . . . . . . . 25
90	85, 89	eqeq12d 2424	. . . . . . . . . . . . . . . . . . . . . . . 24
91	90	adantl 464	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
92	83, 91	rspcdv 3162	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
93	15, 16	npcand 9970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
94	93	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
95	94	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
96	95	preq2d 4057	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
97	96	eqeq2d 2416	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
98	40	ad4antlr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
99	74	com12 29	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
100	63, 99	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
101	100	com3r 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
102	101	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word $/\$ Word $/\$
103	102	imp31 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$ $/\$ $/\$
104	103, 80	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$ $/\$ ..^
105	104, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
106	98, 105	ffvelrnd 6009	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
107	106	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
108	38, 107	ffvelrnd 6009	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
109		eqcom 2411	. . . . . . . . . . . . . . . . . . . . . . . . . 26
110	109	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25
111	110	eleq1d 2471	. . . . . . . . . . . . . . . . . . . . . . . 24
112	108, 111	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
113	97, 112	sylbid 215	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
114	92, 113	syld 42	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
115	114	com12 29	. . . . . . . . . . . . . . . . . . . 20 ..^ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
116	115	adantr 463	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
117	116	impcom 428	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
118		preq2 4051	. . . . . . . . . . . . . . . . . . . . 21
119	118	eleq1d 2471	. . . . . . . . . . . . . . . . . . . 20
120	119	adantl 464	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
121	120	adantl 464	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
122	117, 121	mpbird 232	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
123	26, 62, 122	3jca 1177	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
124	123	exp41 608	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
125	124	exp41 608	. . . . . . . . . . . . . 14 Word Word ..^ $/\$ lastS $/\$ ..^ $/\$
126	8, 125	syl 17	. . . . . . . . . . . . 13 Word ..^ $/\$ lastS $/\$ ..^ $/\$
127	126	com13 80	. . . . . . . . . . . 12 Word ..^ $/\$ lastS $/\$ ..^ $/\$
128	4, 127	mpcom 34	. . . . . . . . . . 11 Word ..^ $/\$ lastS $/\$ ..^ $/\$
129	128	imp 427	. . . . . . . . . 10 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
130	7, 129	mpd 15	. . . . . . . . 9 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
131	130	expcom 433	. . . . . . . 8 Word ..^ $/\$ lastS $/\$ ..^ $/\$
132	131	com14 88	. . . . . . 7 Word ..^ $/\$ lastS $/\$ ..^ $/\$
133	132	imp 427	. . . . . 6 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
134	133	com13 80	. . . . 5 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
135	134	imp 427	. . . 4 $/\$ $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
136	135	com12 29	. . 3 $/\$ Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
137	3, 136	sylan 469	. 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 367 $/\$ w3a 974

wceq 1405

wcel 1842

wral 2753

wss 3413

cpr 3973 class class class wbr 4394

cdm 4822

crn 4823

wfn 5563

wf 5564

wf1 5565

cfv 5568 (class class class)co 6277

cr 9520

cc0 9521

c1 9522

caddc 9524

cle 9658

cmin 9840

cn 10575

c2 10625

cn0 10835

cz 10904

cuz 11126

cfz 11724 ..^cfzo 11852

chash 12450 Word cword 12581 lastS clsw 12582 USGrph cusg 24734

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6573 ax-cnex 9577 ax-resscn 9578 ax-1cn 9579 ax-icn 9580 ax-addcl 9581 ax-addrcl 9582 ax-mulcl 9583 ax-mulrcl 9584 ax-mulcom 9585 ax-addass 9586 ax-mulass 9587 ax-distr 9588 ax-i2m1 9589 ax-1ne0 9590 ax-1rid 9591 ax-rnegex 9592 ax-rrecex 9593 ax-cnre 9594 ax-pre-lttri 9595 ax-pre-lttrn 9596 ax-pre-ltadd 9597 ax-pre-mulgt0 9598

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 975 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-nel 2601 df-ral 2758 df-rex 2759 df-reu 2760 df-rmo 2761 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-pss 3429 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-tp 3976 df-op 3978 df-uni 4191 df-int 4227 df-iun 4272 df-br 4395 df-opab 4453 df-mpt 4454 df-tr 4489 df-eprel 4733 df-id 4737 df-po 4743 df-so 4744 df-fr 4781 df-we 4783 df-xp 4828 df-rel 4829 df-cnv 4830 df-co 4831 df-dm 4832 df-rn 4833 df-res 4834 df-ima 4835 df-pred 5366 df-ord 5412 df-on 5413 df-lim 5414 df-suc 5415 df-iota 5532 df-fun 5570 df-fn 5571 df-f 5572 df-f1 5573 df-fo 5574 df-f1o 5575 df-fv 5576 df-riota 6239 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6683 df-1st 6783 df-2nd 6784 df-wrecs 7012 df-recs 7074 df-rdg 7112 df-1o 7166 df-oadd 7170 df-er 7347 df-en 7554 df-dom 7555 df-sdom 7556 df-fin 7557 df-card 8351 df-cda 8579 df-pnf 9659 df-mnf 9660 df-xr 9661 df-ltxr 9662 df-le 9663 df-sub 9842 df-neg 9843 df-nn 10576 df-2 10634 df-n0 10836 df-z 10905 df-uz 11127 df-fz 11725 df-fzo 11853 df-hash 12451 df-word 12589 df-lsw 12590 df-usgra 24737

This theorem is referenced by: clwlkisclwwlklem0 25192 clwlkfclwwlk 25248

W3C validator