This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem swrdswrdlem

Description: Lemma for swrdswrd . (Contributed by Alexander van der Vekens, 4-Apr-2018)

Ref Expression
Assertion swrdswrdlem ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 + 𝐾 ) ∈ ( 0 ... ( 𝑀 + 𝐿 ) ) ∧ ( 𝑀 + 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) ) → 𝑊 ∈ Word 𝑉 )
2 elfz2 ⊢ ( 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ↔ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) )
3 elfz2nn0 ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ↔ ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝐾 ≤ ( 𝑁 − 𝑀 ) ) )
4 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
5 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝑀 + 𝐾 ) ∈ ℕ0 )
6 5 adantrr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( 𝑀 + 𝐾 ) ∈ ℕ0 )
7 6 adantr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 + 𝐾 ) ∈ ℕ0 )
8 elnn0z ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
9 0red ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 0 ∈ ℝ )
10 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
11 10 adantr ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐾 ∈ ℝ )
12 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
13 12 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → 𝐿 ∈ ℝ )
14 letr ⊢ ( ( 0 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → 0 ≤ 𝐿 ) )
15 9 11 13 14 syl3anc ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → 0 ≤ 𝐿 ) )
16 elnn0z ⊢ ( 𝐿 ∈ ℕ0 ↔ ( 𝐿 ∈ ℤ ∧ 0 ≤ 𝐿 ) )
17 nn0addcl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑀 + 𝐿 ) ∈ ℕ0 )
18 17 expcom ⊢ ( 𝐿 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) )
19 16 18 sylbir ⊢ ( ( 𝐿 ∈ ℤ ∧ 0 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) )
20 19 ex ⊢ ( 𝐿 ∈ ℤ → ( 0 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) )
21 20 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) )
22 15 21 syld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) )
23 22 expd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐾 → ( 𝐾 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) ) )
24 23 com34 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐾 → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) ) )
25 24 impancom ⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) → ( 𝐿 ∈ ℤ → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) ) )
26 8 25 sylbi ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐿 ∈ ℤ → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) ) )
27 26 imp ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) ) )
28 27 impcom ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) )
29 28 imp ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 + 𝐿 ) ∈ ℕ0 )
30 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
31 30 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → 𝐾 ∈ ℝ )
32 31 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → 𝐾 ∈ ℝ )
33 12 adantl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → 𝐿 ∈ ℝ )
34 33 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → 𝐿 ∈ ℝ )
35 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
36 35 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → 𝑀 ∈ ℝ )
37 32 34 36 leadd2d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( 𝐾 ≤ 𝐿 ↔ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) )
38 37 biimpa ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) )
39 7 29 38 3jca ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ 𝐾 ≤ 𝐿 ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) )
40 39 exp31 ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 𝐾 ≤ 𝐿 → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
41 40 com23 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝐿 → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
42 41 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( 𝐾 ≤ 𝐿 → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
43 4 42 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ≤ 𝐿 → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
44 43 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( 𝐾 ≤ 𝐿 → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
45 44 com13 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 𝐾 ≤ 𝐿 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
46 45 ex ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐿 ∈ ℤ → ( 𝐾 ≤ 𝐿 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) ) )
47 46 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝐾 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝐿 ∈ ℤ → ( 𝐾 ≤ 𝐿 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) ) )
48 3 47 sylbi ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( 𝐿 ∈ ℤ → ( 𝐾 ≤ 𝐿 → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) ) )
49 48 com13 ⊢ ( 𝐾 ≤ 𝐿 → ( 𝐿 ∈ ℤ → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) ) )
50 49 adantr ⊢ ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝐿 ∈ ℤ → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) ) )
51 50 com12 ⊢ ( 𝐿 ∈ ℤ → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) ) )
52 51 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) ) )
53 52 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
54 2 53 sylbi ⊢ ( 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) ) )
55 54 impcom ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) ) )
56 55 impcom ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) )
57 elfz2nn0 ⊢ ( ( 𝑀 + 𝐾 ) ∈ ( 0 ... ( 𝑀 + 𝐿 ) ) ↔ ( ( 𝑀 + 𝐾 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐾 ) ≤ ( 𝑀 + 𝐿 ) ) )
58 56 57 sylibr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑀 + 𝐾 ) ∈ ( 0 ... ( 𝑀 + 𝐿 ) ) )
59 elfz2nn0 ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) )
60 28 com12 ⊢ ( 𝐾 ≤ 𝐿 → ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) )
61 60 adantr ⊢ ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( 𝑀 + 𝐿 ) ∈ ℕ0 ) )
62 61 impcom ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) → ( 𝑀 + 𝐿 ) ∈ ℕ0 )
63 62 adantr ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑀 + 𝐿 ) ∈ ℕ0 )
64 simpr2 ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
65 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
66 65 35 anim12i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
67 nn0re ⊢ ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
68 66 67 anim12i ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) )
69 simpllr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → 𝑀 ∈ ℝ )
70 simpr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → 𝐿 ∈ ℝ )
71 simplll ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → 𝑁 ∈ ℝ )
72 69 70 71 leaddsub2d ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( ( 𝑀 + 𝐿 ) ≤ 𝑁 ↔ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) )
73 readdcl ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑀 + 𝐿 ) ∈ ℝ )
74 73 ad4ant24 ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( 𝑀 + 𝐿 ) ∈ ℝ )
75 simpr ⊢ ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
76 75 adantr ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
77 letr ⊢ ( ( ( 𝑀 + 𝐿 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( ( 𝑀 + 𝐿 ) ≤ 𝑁 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) )
78 77 expd ⊢ ( ( ( 𝑀 + 𝐿 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) → ( ( 𝑀 + 𝐿 ) ≤ 𝑁 → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
79 74 71 76 78 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( ( 𝑀 + 𝐿 ) ≤ 𝑁 → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
80 79 a1ddd ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( ( 𝑀 + 𝐿 ) ≤ 𝑁 → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 0 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
81 72 80 sylbird ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 0 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
82 81 com23 ⊢ ( ( ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 0 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
83 68 12 82 syl2an ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) ∧ 𝐿 ∈ ℤ ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 0 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
84 83 ex ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( 𝐿 ∈ ℤ → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 0 ≤ 𝐿 → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
85 84 com25 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) → ( 0 ≤ 𝐿 → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝐿 ∈ ℤ → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
86 85 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 0 ≤ 𝐿 → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝐿 ∈ ℤ → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
87 86 com24 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 0 ≤ 𝐿 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝐿 ∈ ℤ → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
88 87 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 0 ≤ 𝐿 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝐿 ∈ ℤ → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) ) ) )
89 88 com25 ⊢ ( 𝑁 ∈ ℕ0 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 → ( 𝑁 ≤ ( ♯ ‘ 𝑊 ) → ( 0 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝐿 ∈ ℤ → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) ) ) )
90 89 3imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 0 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝐿 ∈ ℤ → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
91 90 com15 ⊢ ( 𝐿 ∈ ℤ → ( 0 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
92 91 adantl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
93 15 92 syld ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿 ) → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
94 93 expd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐾 → ( 𝐾 ≤ 𝐿 → ( 𝑀 ∈ ℕ0 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
95 94 com35 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐾 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 ≤ 𝐿 → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
96 95 com25 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐾 ≤ 𝐿 → ( 𝐿 ≤ ( 𝑁 − 𝑀 ) → ( 𝑀 ∈ ℕ0 → ( 0 ≤ 𝐾 → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )
97 96 impd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝑀 ∈ ℕ0 → ( 0 ≤ 𝐾 → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
98 97 com24 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 0 ≤ 𝐾 → ( 𝑀 ∈ ℕ0 → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
99 98 impancom ⊢ ( ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) → ( 𝐿 ∈ ℤ → ( 𝑀 ∈ ℕ0 → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
100 8 99 sylbi ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐿 ∈ ℤ → ( 𝑀 ∈ ℕ0 → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
101 100 imp ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( 𝑀 ∈ ℕ0 → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
102 101 impcom ⊢ ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
103 102 imp ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) )
104 103 imp ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) )
105 63 64 104 3jca ⊢ ( ( ( ( 𝑀 ∈ ℕ0 ∧ ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) ∧ ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) )
106 105 exp41 ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
107 106 com24 ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
108 107 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
109 4 108 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
110 109 com12 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝑁 ≤ ( ♯ ‘ 𝑊 ) ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
111 59 110 sylbi ⊢ ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
112 111 imp ⊢ ( ( 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
113 112 3adant1 ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
114 113 com13 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
115 114 ex ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐿 ∈ ℤ → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
116 115 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑁 − 𝑀 ) ∈ ℕ0 ∧ 𝐾 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝐿 ∈ ℤ → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
117 3 116 sylbi ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( 𝐿 ∈ ℤ → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
118 117 com3l ⊢ ( 𝐿 ∈ ℤ → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
119 118 3ad2ant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) ) )
120 119 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 − 𝑀 ) ∈ ℤ ∧ 𝐿 ∈ ℤ ) ∧ ( 𝐾 ≤ 𝐿 ∧ 𝐿 ≤ ( 𝑁 − 𝑀 ) ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
121 2 120 sylbi ⊢ ( 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) ) )
122 121 impcom ⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) ) )
123 122 impcom ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) ) → ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) )
124 elfz2nn0 ⊢ ( ( 𝑀 + 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ↔ ( ( 𝑀 + 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ ( 𝑀 + 𝐿 ) ≤ ( ♯ ‘ 𝑊 ) ) )
125 123 124 sylibr ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑀 + 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) )
126 1 58 125 3jca ⊢ ( ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) ∧ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) ) → ( 𝑊 ∈ Word 𝑉 ∧ ( 𝑀 + 𝐾 ) ∈ ( 0 ... ( 𝑀 + 𝐿 ) ) ∧ ( 𝑀 + 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) )