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

Theorem clwlkfclwwlk1hash 25456
 Description: The size of the first component of a closed walk is an integer in the range between 0 and the size of the second component. (Contributed by Alexander van der Vekens, 25-Jun-2018.)
Hypotheses
Ref Expression
clwlkfclwwlk.1
clwlkfclwwlk.2
clwlkfclwwlk.c ClWalks
clwlkfclwwlk.f substr
Assertion
Ref Expression
clwlkfclwwlk1hash
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem clwlkfclwwlk1hash
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 clwlkfclwwlk.c . . 3 ClWalks
21rabeq2i 3075 . 2 ClWalks
3 clwlkfclwwlk.1 . . . . 5
4 clwlkfclwwlk.2 . . . . 5
53, 4clwlkcompim 25378 . . . 4 ClWalks Word ..^
6 lencl 12663 . . . . . 6 Word
7 ffn 5737 . . . . . 6
8 fz0hash 12597 . . . . . . 7
9 id 23 . . . . . . . . . 10
10 peano2nn0 10899 . . . . . . . . . 10
11 nn0re 10867 . . . . . . . . . . 11
1211lep1d 10527 . . . . . . . . . 10
13 elfz2nn0 11872 . . . . . . . . . 10
149, 10, 12, 13syl3anbrc 1189 . . . . . . . . 9
15 oveq2 6304 . . . . . . . . . 10
1615eleq2d 2490 . . . . . . . . 9
1714, 16syl5ibrcom 225 . . . . . . . 8
1817adantr 466 . . . . . . 7
198, 18mpd 15 . . . . . 6
206, 7, 19syl2an 479 . . . . 5 Word
2120adantr 466 . . . 4 Word ..^
225, 21syl 17 . . 3 ClWalks