Metamath Proof Explorer

Theorem crctcshwlkn0lem7

Description: Lemma for crctcshwlkn0 . (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypotheses crctcshwlkn0lem.s ⊢φ→S∈1..^N
crctcshwlkn0lem.q ⊢Q=x∈0…N⟼ifx≤N−SP⁡x+SP⁡x+S-N
crctcshwlkn0lem.h ⊢H=FcyclShiftS
crctcshwlkn0lem.n ⊢N=F
crctcshwlkn0lem.f ⊢φ→F∈WordA
crctcshwlkn0lem.p ⊢φ→∀i∈0..^Nif-P⁡i=P⁡i+1I⁡F⁡i=P⁡iP⁡iP⁡i+1⊆I⁡F⁡i
crctcshwlkn0lem.e ⊢φ→P⁡N=P⁡0
Assertion crctcshwlkn0lem7 ⊢φ→∀j∈0..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j

Proof

Step Hyp Ref Expression
1 crctcshwlkn0lem.s ⊢φ→S∈1..^N
2 crctcshwlkn0lem.q ⊢Q=x∈0…N⟼ifx≤N−SP⁡x+SP⁡x+S-N
3 crctcshwlkn0lem.h ⊢H=FcyclShiftS
4 crctcshwlkn0lem.n ⊢N=F
5 crctcshwlkn0lem.f ⊢φ→F∈WordA
6 crctcshwlkn0lem.p ⊢φ→∀i∈0..^Nif-P⁡i=P⁡i+1I⁡F⁡i=P⁡iP⁡iP⁡i+1⊆I⁡F⁡i
7 crctcshwlkn0lem.e ⊢φ→P⁡N=P⁡0
8 1 2 3 4 5 6 crctcshwlkn0lem4 ⊢φ→∀j∈0..^N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
9 eqidd ⊢φ→N−S=N−S
10 1 2 3 4 5 6 7 crctcshwlkn0lem6 ⊢φ∧N−S=N−S→if-Q⁡N−S=Q⁡N-S+1I⁡H⁡N−S=Q⁡N−SQ⁡N−SQ⁡N-S+1⊆I⁡H⁡N−S
11 9 10 mpdan ⊢φ→if-Q⁡N−S=Q⁡N-S+1I⁡H⁡N−S=Q⁡N−SQ⁡N−SQ⁡N-S+1⊆I⁡H⁡N−S
12 ovex ⊢N−S∈V
13 wkslem1 ⊢j=N−S→if-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j↔if-Q⁡N−S=Q⁡N-S+1I⁡H⁡N−S=Q⁡N−SQ⁡N−SQ⁡N-S+1⊆I⁡H⁡N−S
14 12 13 ralsn ⊢∀j∈N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j↔if-Q⁡N−S=Q⁡N-S+1I⁡H⁡N−S=Q⁡N−SQ⁡N−SQ⁡N-S+1⊆I⁡H⁡N−S
15 11 14 sylibr ⊢φ→∀j∈N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
16 ralunb ⊢∀j∈0..^N−S∪N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j↔∀j∈0..^N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j∧∀j∈N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
17 8 15 16 sylanbrc ⊢φ→∀j∈0..^N−S∪N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
18 elfzo1 ⊢S∈1..^N↔S∈ℕ∧N∈ℕ∧S<N
19 nnz ⊢N∈ℕ→N∈ℤ
20 nnz ⊢S∈ℕ→S∈ℤ
21 zsubcl ⊢N∈ℤ∧S∈ℤ→N−S∈ℤ
22 19 20 21 syl2anr ⊢S∈ℕ∧N∈ℕ→N−S∈ℤ
23 22 3adant3 ⊢S∈ℕ∧N∈ℕ∧S<N→N−S∈ℤ
24 nnre ⊢S∈ℕ→S∈ℝ
25 nnre ⊢N∈ℕ→N∈ℝ
26 posdif ⊢S∈ℝ∧N∈ℝ→S<N↔0<N−S
27 0re ⊢0∈ℝ
28 resubcl ⊢N∈ℝ∧S∈ℝ→N−S∈ℝ
29 28 ancoms ⊢S∈ℝ∧N∈ℝ→N−S∈ℝ
30 ltle ⊢0∈ℝ∧N−S∈ℝ→0<N−S→0≤N−S
31 27 29 30 sylancr ⊢S∈ℝ∧N∈ℝ→0<N−S→0≤N−S
32 26 31 sylbid ⊢S∈ℝ∧N∈ℝ→S<N→0≤N−S
33 24 25 32 syl2an ⊢S∈ℕ∧N∈ℕ→S<N→0≤N−S
34 33 3impia ⊢S∈ℕ∧N∈ℕ∧S<N→0≤N−S
35 elnn0z ⊢N−S∈ℕ0↔N−S∈ℤ∧0≤N−S
36 23 34 35 sylanbrc ⊢S∈ℕ∧N∈ℕ∧S<N→N−S∈ℕ0
37 elnn0uz ⊢N−S∈ℕ0↔N−S∈ℤ≥0
38 36 37 sylib ⊢S∈ℕ∧N∈ℕ∧S<N→N−S∈ℤ≥0
39 fzosplitsn ⊢N−S∈ℤ≥0→0..^N-S+1=0..^N−S∪N−S
40 38 39 syl ⊢S∈ℕ∧N∈ℕ∧S<N→0..^N-S+1=0..^N−S∪N−S
41 18 40 sylbi ⊢S∈1..^N→0..^N-S+1=0..^N−S∪N−S
42 1 41 syl ⊢φ→0..^N-S+1=0..^N−S∪N−S
43 42 raleqdv ⊢φ→∀j∈0..^N-S+1if-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j↔∀j∈0..^N−S∪N−Sif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
44 17 43 mpbird ⊢φ→∀j∈0..^N-S+1if-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
45 1 2 3 4 5 6 crctcshwlkn0lem5 ⊢φ→∀j∈N-S+1..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
46 ralunb ⊢∀j∈0..^N-S+1∪N-S+1..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j↔∀j∈0..^N-S+1if-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j∧∀j∈N-S+1..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
47 44 45 46 sylanbrc ⊢φ→∀j∈0..^N-S+1∪N-S+1..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
48 nnsub ⊢S∈ℕ∧N∈ℕ→S<N↔N−S∈ℕ
49 48 biimp3a ⊢S∈ℕ∧N∈ℕ∧S<N→N−S∈ℕ
50 nnnn0 ⊢N−S∈ℕ→N−S∈ℕ0
51 peano2nn0 ⊢N−S∈ℕ0→N-S+1∈ℕ0
52 49 50 51 3syl ⊢S∈ℕ∧N∈ℕ∧S<N→N-S+1∈ℕ0
53 nnnn0 ⊢N∈ℕ→N∈ℕ0
54 53 3ad2ant2 ⊢S∈ℕ∧N∈ℕ∧S<N→N∈ℕ0
55 25 anim1i ⊢N∈ℕ∧S∈ℕ→N∈ℝ∧S∈ℕ
56 55 ancoms ⊢S∈ℕ∧N∈ℕ→N∈ℝ∧S∈ℕ
57 crctcshwlkn0lem1 ⊢N∈ℝ∧S∈ℕ→N-S+1≤N
58 56 57 syl ⊢S∈ℕ∧N∈ℕ→N-S+1≤N
59 58 3adant3 ⊢S∈ℕ∧N∈ℕ∧S<N→N-S+1≤N
60 elfz2nn0 ⊢N-S+1∈0…N↔N-S+1∈ℕ0∧N∈ℕ0∧N-S+1≤N
61 52 54 59 60 syl3anbrc ⊢S∈ℕ∧N∈ℕ∧S<N→N-S+1∈0…N
62 18 61 sylbi ⊢S∈1..^N→N-S+1∈0…N
63 fzosplit ⊢N-S+1∈0…N→0..^N=0..^N-S+1∪N-S+1..^N
64 1 62 63 3syl ⊢φ→0..^N=0..^N-S+1∪N-S+1..^N
65 64 raleqdv ⊢φ→∀j∈0..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j↔∀j∈0..^N-S+1∪N-S+1..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j
66 47 65 mpbird ⊢φ→∀j∈0..^Nif-Q⁡j=Q⁡j+1I⁡H⁡j=Q⁡jQ⁡jQ⁡j+1⊆I⁡H⁡j