clwlkisclwwlklem1 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > clwlkisclwwlklem1		Structured version Unicode version

Theorem clwlkisclwwlklem1 30447

Description: Lemma for clwlkisclwwlk 30449. (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 23281	. . . 4 USGrph
2		f1f 5605	. . . 4
3	1, 2	syl 16	. . 3 USGrph
4		lencl 12248	. . . . . . . . . . 11 Word
5		ffn 5558	. . . . . . . . . . 11
6		fz0hash 12202	. . . . . . . . . . 11 $/\$
7	4, 5, 6	syl2an 477	. . . . . . . . . 10 Word $/\$
8		ffz0iswrd 12254	. . . . . . . . . . . . . 14 Word
9		lsw 12265	. . . . . . . . . . . . . . . . . . 19 Word lastS
10	9	ad6antr 735	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
11		oveq1 6097	. . . . . . . . . . . . . . . . . . . 20
12	11	fveq2d 5694	. . . . . . . . . . . . . . . . . . 19
13	12	ad4antlr 732	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
14		eqcom 2444	. . . . . . . . . . . . . . . . . . . . 21
15		nn0cn 10588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
16		ax-1cn 9339	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
17	16	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
18	15, 17	pncand 9719	. . . . . . . . . . . . . . . . . . . . . . . . . 26
19	18	eqcomd 2447	. . . . . . . . . . . . . . . . . . . . . . . . 25
20	19	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
21	20	fveq2d 5694	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
22	21	eqeq1d 2450	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
23	22	biimpd 207	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
24	14, 23	syl5bi 217	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
25	24	adantld 467	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ $/\$
26	25	imp 429	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
27	10, 13, 26	3eqtrd 2478	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS
28		nn0z 10668	. . . . . . . . . . . . . . . . . . . . . . . . 25
29		peano2zm 10687	. . . . . . . . . . . . . . . . . . . . . . . . 25
30	28, 29	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24
31		nn0re 10587	. . . . . . . . . . . . . . . . . . . . . . . . 25
32	31	lem1d 10265	. . . . . . . . . . . . . . . . . . . . . . . 24
33		eluz2 10866	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
34	30, 28, 32, 33	syl3anbrc 1172	. . . . . . . . . . . . . . . . . . . . . . 23
35	34	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
36		fzoss2 11576	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^
37		ssralv 3415	. . . . . . . . . . . . . . . . . . . . . 22 ..^ ..^ ..^ ..^
38	35, 36, 37	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
39		simpr 461	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
40	39	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
41		wrdf 12239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word ..^
42		simpll 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
43		fzossrbm1 11577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ ..^
44	43	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^ $/\$ ..^ ..^
45	44	sselda 3355	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^ $/\$ $/\$ ..^ ..^
46	42, 45	ffvelrnd 5843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^ $/\$ $/\$ ..^
47	46	exp31 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ..^ ..^
48	41, 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	40, 52	ffvelrnd 5843	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
54		eqcom 2444	. . . . . . . . . . . . . . . . . . . . . . . . 25
55	54	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . 24
56	55	eleq1d 2508	. . . . . . . . . . . . . . . . . . . . . . 23
57	53, 56	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^
58	57	ralimdva 2793	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^ ..^
59	38, 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 4295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
64	63	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
65		2re 10390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
66	65	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
67		1re 9384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
69	66, 68, 31	lesubaddd 9935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
70		2m1e1 10435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
71	70	breq1i 4298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
72		elnnnn0c 10624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
73	72	simplbi2 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
74	71, 73	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
75	69, 74	sylbird 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
76	75	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$
77	76	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$
78	64, 77	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$
79	78	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
80	79	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
81		lbfzo0 11585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ..^
82	80, 81	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
83		fzoend 11617	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ ..^
84	82, 83	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
85		fveq2 5690	. . . . . . . . . . . . . . . . . . . . . . . . . 26
86	85	fveq2d 5694	. . . . . . . . . . . . . . . . . . . . . . . . 25
87		fveq2 5690	. . . . . . . . . . . . . . . . . . . . . . . . . 26
88		oveq1 6097	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
89	88	fveq2d 5694	. . . . . . . . . . . . . . . . . . . . . . . . . 26
90	87, 89	preq12d 3961	. . . . . . . . . . . . . . . . . . . . . . . . 25
91	86, 90	eqeq12d 2456	. . . . . . . . . . . . . . . . . . . . . . . 24
92	91	adantl 466	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$
93	84, 92	rspcdv 3075	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
94	15, 17	npcand 9722	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
95	94	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
96	95	fveq2d 5694	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
97	96	preq2d 3960	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
98	97	eqeq2d 2453	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
99	41	ad4antlr 732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
100	75	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
101	63, 100	syl6bi 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
102	101	com3r 79	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
103	102	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Word $/\$ Word $/\$
104	103	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word $/\$ Word $/\$ $/\$
105	104	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word $/\$ Word $/\$ $/\$ $/\$
106	105, 81	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word $/\$ Word $/\$ $/\$ $/\$ ..^
107	106, 83	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word $/\$ Word $/\$ $/\$ $/\$ ..^
108	99, 107	ffvelrnd 5843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Word $/\$ Word $/\$ $/\$ $/\$
109	108	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
110	39, 109	ffvelrnd 5843	. . . . . . . . . . . . . . . . . . . . . . . 24 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
111		eqcom 2444	. . . . . . . . . . . . . . . . . . . . . . . . . 26
112	111	biimpi 194	. . . . . . . . . . . . . . . . . . . . . . . . 25
113	112	eleq1d 2508	. . . . . . . . . . . . . . . . . . . . . . . 24
114	110, 113	syl5ibrcom 222	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
115	98, 114	sylbid 215	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ Word $/\$ $/\$ $/\$ $/\$
116	93, 115	syld 44	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ ..^
117	116	com12 31	. . . . . . . . . . . . . . . . . . . 20 ..^ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
118	117	adantr 465	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$ Word $/\$ Word $/\$ $/\$ $/\$ $/\$
119	118	impcom 430	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
120		preq2 3954	. . . . . . . . . . . . . . . . . . . . 21
121	120	eleq1d 2508	. . . . . . . . . . . . . . . . . . . 20
122	121	adantl 466	. . . . . . . . . . . . . . . . . . 19 ..^ $/\$
123	122	adantl 466	. . . . . . . . . . . . . . . . . 18 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
124	119, 123	mpbird 232	. . . . . . . . . . . . . . . . 17 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$
125	27, 62, 124	3jca 1168	. . . . . . . . . . . . . . . 16 Word $/\$ Word $/\$ $/\$ $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
126	125	exp41 610	. . . . . . . . . . . . . . 15 Word $/\$ Word $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
127	126	exp41 610	. . . . . . . . . . . . . 14 Word Word ..^ $/\$ lastS $/\$ ..^ $/\$
128	8, 127	syl 16	. . . . . . . . . . . . 13 Word ..^ $/\$ lastS $/\$ ..^ $/\$
129	128	com13 80	. . . . . . . . . . . 12 Word ..^ $/\$ lastS $/\$ ..^ $/\$
130	4, 129	mpcom 36	. . . . . . . . . . 11 Word ..^ $/\$ lastS $/\$ ..^ $/\$
131	130	imp 429	. . . . . . . . . 10 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
132	7, 131	mpd 15	. . . . . . . . 9 Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
133	132	expcom 435	. . . . . . . 8 Word ..^ $/\$ lastS $/\$ ..^ $/\$
134	133	com14 88	. . . . . . 7 Word ..^ $/\$ lastS $/\$ ..^ $/\$
135	134	imp 429	. . . . . 6 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
136	135	com13 80	. . . . 5 $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
137	136	imp 429	. . . 4 $/\$ $/\$ Word ..^ $/\$ lastS $/\$ ..^ $/\$
138	137	com12 31	. . 3 $/\$ Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
139	3, 138	sylan 471	. 2 USGrph $/\$ Word $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$
140	139	3imp 1181	1 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^ $/\$ lastS $/\$ ..^ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1369

wcel 1756

wral 2714

wss 3327

cpr 3878 class class class wbr 4291

cdm 4839

crn 4840

wfn 5412

wf 5413

wf1 5414

cfv 5417 (class class class)co 6090

cc 9279

cr 9280

cc0 9281

c1 9282

caddc 9284

cle 9418

cmin 9594

cn 10321

c2 10370

cn0 10578

cz 10645

cuz 10860

cfz 11436 ..^cfzo 11547

chash 12102 Word cword 12220 lastS clsw 12221 USGrph cusg 23263

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4402 ax-sep 4412 ax-nul 4420 ax-pow 4469 ax-pr 4530 ax-un 6371 ax-cnex 9337 ax-resscn 9338 ax-1cn 9339 ax-icn 9340 ax-addcl 9341 ax-addrcl 9342 ax-mulcl 9343 ax-mulrcl 9344 ax-mulcom 9345 ax-addass 9346 ax-mulass 9347 ax-distr 9348 ax-i2m1 9349 ax-1ne0 9350 ax-1rid 9351 ax-rnegex 9352 ax-rrecex 9353 ax-cnre 9354 ax-pre-lttri 9355 ax-pre-lttrn 9356 ax-pre-ltadd 9357 ax-pre-mulgt0 9358

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2567 df-ne 2607 df-nel 2608 df-ral 2719 df-rex 2720 df-reu 2721 df-rab 2723 df-v 2973 df-sbc 3186 df-csb 3288 df-dif 3330 df-un 3332 df-in 3334 df-ss 3341 df-pss 3343 df-nul 3637 df-if 3791 df-pw 3861 df-sn 3877 df-pr 3879 df-tp 3881 df-op 3883 df-uni 4091 df-int 4128 df-iun 4172 df-br 4292 df-opab 4350 df-mpt 4351 df-tr 4385 df-eprel 4631 df-id 4635 df-po 4640 df-so 4641 df-fr 4678 df-we 4680 df-ord 4721 df-on 4722 df-lim 4723 df-suc 4724 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5380 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-riota 6051 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6831 df-rdg 6865 df-1o 6919 df-oadd 6923 df-er 7100 df-en 7310 df-dom 7311 df-sdom 7312 df-fin 7313 df-card 8108 df-pnf 9419 df-mnf 9420 df-xr 9421 df-ltxr 9422 df-le 9423 df-sub 9596 df-neg 9597 df-nn 10322 df-2 10379 df-n0 10579 df-z 10646 df-uz 10861 df-fz 11437 df-fzo 11548 df-hash 12103 df-word 12228 df-lsw 12229 df-usgra 23265

This theorem is referenced by: clwlkisclwwlklem0 30448 clwlkfclwwlk 30515

W3C validator