Metamath Proof Explorer

Theorem cshwcsh2id

Description: A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr and erclwwlkntr . (Contributed by AV, 9-Apr-2018) (Revised by AV, 11-Jun-2018) (Proof shortened by AV, 3-Nov-2018)

Ref Expression
Hypotheses cshwcsh2id.1 ⊢ ( 𝜑 → 𝑧 ∈ Word 𝑉 )
cshwcsh2id.2 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
Assertion cshwcsh2id ( 𝜑 → ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )

Proof

Step Hyp Ref Expression
1 cshwcsh2id.1 ⊢ ( 𝜑 → 𝑧 ∈ Word 𝑉 )
2 cshwcsh2id.2 ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
3 oveq1 ⊢ ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ( 𝑦 cyclShift 𝑚 ) = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) )
4 3 eqeq2d ⊢ ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) ↔ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) )
5 4 anbi2d ⊢ ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ↔ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) ) )
6 5 adantr ⊢ ( ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ↔ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) ) )
7 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → 𝑘 ∈ ℕ0 )
8 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → 𝑚 ∈ ℕ0 )
9 nn0addcl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑘 + 𝑚 ) ∈ ℕ0 )
10 7 8 9 syl2anr ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( 𝑘 + 𝑚 ) ∈ ℕ0 )
11 10 adantr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( 𝑘 + 𝑚 ) ∈ ℕ0 )
12 elfz3nn0 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
13 12 ad2antlr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
14 simprl ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) )
15 elfz2nn0 ⊢ ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ↔ ( ( 𝑘 + 𝑚 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ) )
16 11 13 14 15 syl3anbrc ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) )
17 16 adantr ⊢ ( ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) )
18 1 adantl ⊢ ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → 𝑧 ∈ Word 𝑉 )
19 18 adantl ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → 𝑧 ∈ Word 𝑉 )
20 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → 𝑘 ∈ ℤ )
21 20 ad2antlr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → 𝑘 ∈ ℤ )
22 elfzelz ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → 𝑚 ∈ ℤ )
23 22 adantr ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → 𝑚 ∈ ℤ )
24 23 adantr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → 𝑚 ∈ ℤ )
25 2cshw ⊢ ( ( 𝑧 ∈ Word 𝑉 ∧ 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) )
26 19 21 24 25 syl3anc ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) )
27 26 eqeq2d ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ↔ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) )
28 27 biimpa ⊢ ( ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) )
29 17 28 jca ⊢ ( ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) )
30 29 exp41 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) ) )
31 30 com23 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) ) )
32 31 com24 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) ) )
33 32 imp ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) )
34 33 com12 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) )
35 34 adantl ⊢ ( ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) )
36 6 35 sylbid ⊢ ( ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) )
37 36 ancoms ⊢ ( ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) ) )
38 37 impcom ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) ) )
39 oveq2 ⊢ ( 𝑛 = ( 𝑘 + 𝑚 ) → ( 𝑧 cyclShift 𝑛 ) = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) )
40 39 rspceeqv ⊢ ( ( ( 𝑘 + 𝑚 ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) )
41 38 40 syl6com ⊢ ( ( ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
42 elfz2 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ↔ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 0 ≤ 𝑘 ∧ 𝑘 ≤ ( ♯ ‘ 𝑧 ) ) ) )
43 nn0z ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℤ )
44 zaddcl ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑘 + 𝑚 ) ∈ ℤ )
45 44 ex ⊢ ( 𝑘 ∈ ℤ → ( 𝑚 ∈ ℤ → ( 𝑘 + 𝑚 ) ∈ ℤ ) )
46 45 adantl ⊢ ( ( ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑚 ∈ ℤ → ( 𝑘 + 𝑚 ) ∈ ℤ ) )
47 46 impcom ⊢ ( ( 𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 + 𝑚 ) ∈ ℤ )
48 simprl ⊢ ( ( 𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( ♯ ‘ 𝑧 ) ∈ ℤ )
49 47 48 zsubcld ⊢ ( ( 𝑚 ∈ ℤ ∧ ( ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ )
50 49 ex ⊢ ( 𝑚 ∈ ℤ → ( ( ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ ) )
51 43 50 syl ⊢ ( 𝑚 ∈ ℕ0 → ( ( ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ ) )
52 51 com12 ⊢ ( ( ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑚 ∈ ℕ0 → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ ) )
53 52 3adant1 ⊢ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑚 ∈ ℕ0 → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ ) )
54 53 adantr ⊢ ( ( ( 0 ∈ ℤ ∧ ( ♯ ‘ 𝑧 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) ∧ ( 0 ≤ 𝑘 ∧ 𝑘 ≤ ( ♯ ‘ 𝑧 ) ) ) → ( 𝑚 ∈ ℕ0 → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ ) )
55 42 54 sylbi ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( 𝑚 ∈ ℕ0 → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ ) )
56 8 55 mpan9 ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ )
57 56 adantr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ )
58 elfz2nn0 ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ↔ ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ 𝑘 ≤ ( ♯ ‘ 𝑧 ) ) )
59 nn0re ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ )
60 nn0re ⊢ ( ( ♯ ‘ 𝑧 ) ∈ ℕ0 → ( ♯ ‘ 𝑧 ) ∈ ℝ )
61 59 60 anim12i ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) → ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) )
62 nn0re ⊢ ( 𝑚 ∈ ℕ0 → 𝑚 ∈ ℝ )
63 61 62 anim12i ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) )
64 simplr ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ♯ ‘ 𝑧 ) ∈ ℝ )
65 readdcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → ( 𝑘 + 𝑚 ) ∈ ℝ )
66 65 adantlr ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( 𝑘 + 𝑚 ) ∈ ℝ )
67 64 66 ltnled ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( ♯ ‘ 𝑧 ) < ( 𝑘 + 𝑚 ) ↔ ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ) )
68 64 66 posdifd ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( ♯ ‘ 𝑧 ) < ( 𝑘 + 𝑚 ) ↔ 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
69 68 biimpd ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ( ♯ ‘ 𝑧 ) < ( 𝑘 + 𝑚 ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
70 67 69 sylbird ⊢ ( ( ( 𝑘 ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ∧ 𝑚 ∈ ℝ ) → ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
71 63 70 syl ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
72 71 ex ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) → ( 𝑚 ∈ ℕ0 → ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) )
73 72 3adant3 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ 𝑘 ≤ ( ♯ ‘ 𝑧 ) ) → ( 𝑚 ∈ ℕ0 → ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) )
74 58 73 sylbi ⊢ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( 𝑚 ∈ ℕ0 → ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) )
75 8 74 mpan9 ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
76 75 com12 ⊢ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
77 76 adantr ⊢ ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
78 77 impcom ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) )
79 elnnz ⊢ ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℕ ↔ ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℤ ∧ 0 < ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
80 57 78 79 sylanbrc ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℕ )
81 80 nnnn0d ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℕ0 )
82 12 ad2antlr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ♯ ‘ 𝑧 ) ∈ ℕ0 )
83 oveq2 ⊢ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( 0 ... ( ♯ ‘ 𝑦 ) ) = ( 0 ... ( ♯ ‘ 𝑧 ) ) )
84 83 eleq2d ⊢ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ↔ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) )
85 84 anbi1d ⊢ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ↔ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ) )
86 elfz2nn0 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ↔ ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ 𝑚 ≤ ( ♯ ‘ 𝑧 ) ) )
87 59 adantr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) → 𝑘 ∈ ℝ )
88 87 62 anim12i ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ ) )
89 60 60 jca ⊢ ( ( ♯ ‘ 𝑧 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑧 ) ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) )
90 89 ad2antlr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑧 ) ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) )
91 le2add ⊢ ( ( ( 𝑘 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ∧ ( ( ♯ ‘ 𝑧 ) ∈ ℝ ∧ ( ♯ ‘ 𝑧 ) ∈ ℝ ) ) → ( ( 𝑘 ≤ ( ♯ ‘ 𝑧 ) ∧ 𝑚 ≤ ( ♯ ‘ 𝑧 ) ) → ( 𝑘 + 𝑚 ) ≤ ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑧 ) ) ) )
92 88 90 91 syl2anc ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( ♯ ‘ 𝑧 ) ∧ 𝑚 ≤ ( ♯ ‘ 𝑧 ) ) → ( 𝑘 + 𝑚 ) ≤ ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑧 ) ) ) )
93 nn0readdcl ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑚 ∈ ℕ0 ) → ( 𝑘 + 𝑚 ) ∈ ℝ )
94 93 adantlr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑘 + 𝑚 ) ∈ ℝ )
95 60 ad2antlr ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( ♯ ‘ 𝑧 ) ∈ ℝ )
96 94 95 95 lesubadd2d ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ↔ ( 𝑘 + 𝑚 ) ≤ ( ( ♯ ‘ 𝑧 ) + ( ♯ ‘ 𝑧 ) ) ) )
97 92 96 sylibrd ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( ( 𝑘 ≤ ( ♯ ‘ 𝑧 ) ∧ 𝑚 ≤ ( ♯ ‘ 𝑧 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
98 97 expcomd ⊢ ( ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) ∧ 𝑚 ∈ ℕ0 ) → ( 𝑚 ≤ ( ♯ ‘ 𝑧 ) → ( 𝑘 ≤ ( ♯ ‘ 𝑧 ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) ) )
99 98 ex ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) → ( 𝑚 ∈ ℕ0 → ( 𝑚 ≤ ( ♯ ‘ 𝑧 ) → ( 𝑘 ≤ ( ♯ ‘ 𝑧 ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) ) ) )
100 99 com24 ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ) → ( 𝑘 ≤ ( ♯ ‘ 𝑧 ) → ( 𝑚 ≤ ( ♯ ‘ 𝑧 ) → ( 𝑚 ∈ ℕ0 → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) ) ) )
101 100 3impia ⊢ ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ 𝑘 ≤ ( ♯ ‘ 𝑧 ) ) → ( 𝑚 ≤ ( ♯ ‘ 𝑧 ) → ( 𝑚 ∈ ℕ0 → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) ) )
102 101 com13 ⊢ ( 𝑚 ∈ ℕ0 → ( 𝑚 ≤ ( ♯ ‘ 𝑧 ) → ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ 𝑘 ≤ ( ♯ ‘ 𝑧 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) ) )
103 102 imp ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( ♯ ‘ 𝑧 ) ) → ( ( 𝑘 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ 𝑘 ≤ ( ♯ ‘ 𝑧 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
104 58 103 biimtrid ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝑚 ≤ ( ♯ ‘ 𝑧 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
105 104 3adant2 ⊢ ( ( 𝑚 ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ 𝑚 ≤ ( ♯ ‘ 𝑧 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
106 86 105 sylbi ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
107 106 imp ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) )
108 85 107 biimtrdi ⊢ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
109 108 adantr ⊢ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
110 2 109 syl ⊢ ( 𝜑 → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
111 110 adantl ⊢ ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
112 111 impcom ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) )
113 elfz2nn0 ⊢ ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ↔ ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑧 ) ∈ ℕ0 ∧ ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ≤ ( ♯ ‘ 𝑧 ) ) )
114 81 82 112 113 syl3anbrc ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) )
115 114 adantr ⊢ ( ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) )
116 1 adantl ⊢ ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → 𝑧 ∈ Word 𝑉 )
117 116 adantl ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → 𝑧 ∈ Word 𝑉 )
118 20 ad2antlr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → 𝑘 ∈ ℤ )
119 23 adantr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → 𝑚 ∈ ℤ )
120 117 118 119 25 syl3anc ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) = ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) )
121 20 22 44 syl2anr ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( 𝑘 + 𝑚 ) ∈ ℤ )
122 cshwsublen ⊢ ( ( 𝑧 ∈ Word 𝑉 ∧ ( 𝑘 + 𝑚 ) ∈ ℤ ) → ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
123 116 121 122 syl2anr ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( 𝑧 cyclShift ( 𝑘 + 𝑚 ) ) = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
124 120 123 eqtrd ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
125 124 eqeq2d ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ↔ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) )
126 125 biimpa ⊢ ( ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
127 115 126 jca ⊢ ( ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) ∧ ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) )
128 127 exp41 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) ) ) )
129 128 com23 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) ) ) )
130 129 com24 ⊢ ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) ) ) )
131 130 imp ⊢ ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( ( 𝑧 cyclShift 𝑘 ) cyclShift 𝑚 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) ) )
132 5 131 biimtrdi ⊢ ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) ) ) )
133 132 com23 ⊢ ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) ) ) )
134 133 impcom ⊢ ( ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) → ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) ) )
135 134 impcom ⊢ ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) ) )
136 oveq2 ⊢ ( 𝑛 = ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) → ( 𝑧 cyclShift 𝑛 ) = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) )
137 136 rspceeqv ⊢ ( ( ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑥 = ( 𝑧 cyclShift ( ( 𝑘 + 𝑚 ) − ( ♯ ‘ 𝑧 ) ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) )
138 135 137 syl6com ⊢ ( ( ¬ ( 𝑘 + 𝑚 ) ≤ ( ♯ ‘ 𝑧 ) ∧ 𝜑 ) → ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
139 41 138 pm2.61ian ⊢ ( 𝜑 → ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )