Proof of Theorem swrdswrdlem
Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → 𝑊 ∈ Word 𝑉) |
2 | | elfz2 12204 |
. . . . . 6
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) ↔ ((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)))) |
3 | | elfz2nn0 12300 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 − 𝑀) ∈ ℕ0 ∧ 𝐾 ≤ (𝑁 − 𝑀))) |
4 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑀 ≤ 𝑁)) |
5 | | nn0addcl 11205 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑀 + 𝐾) ∈
ℕ0) |
6 | 5 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝑀
+ 𝐾) ∈
ℕ0) |
7 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ 𝐾
≤ 𝐿) → (𝑀 + 𝐾) ∈
ℕ0) |
8 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ∈ ℕ0
↔ (𝐾 ∈ ℤ
∧ 0 ≤ 𝐾)) |
9 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 0 ∈
ℝ) |
10 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℝ) |
11 | 10 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐾 ∈
ℝ) |
12 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
ℝ) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → 𝐿 ∈
ℝ) |
14 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((0
∈ ℝ ∧ 𝐾
∈ ℝ ∧ 𝐿
∈ ℝ) → ((0 ≤ 𝐾 ∧ 𝐾 ≤ 𝐿) → 0 ≤ 𝐿)) |
15 | 9, 11, 13, 14 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤
𝐾 ∧ 𝐾 ≤ 𝐿) → 0 ≤ 𝐿)) |
16 | | elnn0z 11267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐿 ∈ ℕ0
↔ (𝐿 ∈ ℤ
∧ 0 ≤ 𝐿)) |
17 | | nn0addcl 11205 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑀 ∈ ℕ0
∧ 𝐿 ∈
ℕ0) → (𝑀 + 𝐿) ∈
ℕ0) |
18 | 17 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐿 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (𝑀 + 𝐿) ∈
ℕ0)) |
19 | 16, 18 | sylbir 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐿 ∈ ℤ ∧ 0 ≤
𝐿) → (𝑀 ∈ ℕ0
→ (𝑀 + 𝐿) ∈
ℕ0)) |
20 | 19 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐿 ∈ ℤ → (0 ≤
𝐿 → (𝑀 ∈ ℕ0 → (𝑀 + 𝐿) ∈
ℕ0))) |
21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐿 → (𝑀 ∈ ℕ0 → (𝑀 + 𝐿) ∈
ℕ0))) |
22 | 15, 21 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤
𝐾 ∧ 𝐾 ≤ 𝐿) → (𝑀 ∈ ℕ0 → (𝑀 + 𝐿) ∈
ℕ0))) |
23 | 22 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐾 → (𝐾 ≤ 𝐿 → (𝑀 ∈ ℕ0 → (𝑀 + 𝐿) ∈
ℕ0)))) |
24 | 23 | com34 89 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐾 → (𝑀 ∈ ℕ0 → (𝐾 ≤ 𝐿 → (𝑀 + 𝐿) ∈
ℕ0)))) |
25 | 24 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) → (𝐿 ∈ ℤ → (𝑀 ∈ ℕ0
→ (𝐾 ≤ 𝐿 → (𝑀 + 𝐿) ∈
ℕ0)))) |
26 | 8, 25 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐾 ∈ ℕ0
→ (𝐿 ∈ ℤ
→ (𝑀 ∈
ℕ0 → (𝐾 ≤ 𝐿 → (𝑀 + 𝐿) ∈
ℕ0)))) |
27 | 26 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝑀 ∈
ℕ0 → (𝐾 ≤ 𝐿 → (𝑀 + 𝐿) ∈
ℕ0))) |
28 | 27 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝐾
≤ 𝐿 → (𝑀 + 𝐿) ∈
ℕ0)) |
29 | 28 | imp 444 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ 𝐾
≤ 𝐿) → (𝑀 + 𝐿) ∈
ℕ0) |
30 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℝ) |
31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ 𝐾 ∈
ℝ) |
32 | 31 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝐾
∈ ℝ) |
33 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ 𝐿 ∈
ℝ) |
34 | 33 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝐿
∈ ℝ) |
35 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 ∈ ℕ0
→ 𝑀 ∈
ℝ) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → 𝑀
∈ ℝ) |
37 | 32, 34, 36 | leadd2d 10501 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → (𝐾
≤ 𝐿 ↔ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))) |
38 | 37 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ 𝐾
≤ 𝐿) → (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)) |
39 | 7, 29, 38 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ 𝐾
≤ 𝐿) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))) |
40 | 39 | exp31 628 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ0
→ ((𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ) → (𝐾
≤ 𝐿 → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
41 | 40 | com23 84 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ ℕ0
→ (𝐾 ≤ 𝐿 → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
42 | 41 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) → (𝐾 ≤ 𝐿 → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
43 | 4, 42 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ (0...𝑁) → (𝐾 ≤ 𝐿 → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
44 | 43 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → (𝐾 ≤ 𝐿 → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
45 | 44 | com13 86 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝐾 ≤ 𝐿 → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
46 | 45 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℕ0
→ (𝐿 ∈ ℤ
→ (𝐾 ≤ 𝐿 → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))))) |
47 | 46 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0
∧ 𝐾 ≤ (𝑁 − 𝑀)) → (𝐿 ∈ ℤ → (𝐾 ≤ 𝐿 → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))))) |
48 | 3, 47 | sylbi 206 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → (𝐿 ∈ ℤ → (𝐾 ≤ 𝐿 → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))))) |
49 | 48 | com13 86 |
. . . . . . . . . 10
⊢ (𝐾 ≤ 𝐿 → (𝐿 ∈ ℤ → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))))) |
50 | 49 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝐿 ∈ ℤ → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))))) |
51 | 50 | com12 32 |
. . . . . . . 8
⊢ (𝐿 ∈ ℤ → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))))) |
52 | 51 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))))) |
53 | 52 | imp 444 |
. . . . . 6
⊢ (((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
54 | 2, 53 | sylbi 206 |
. . . . 5
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))))) |
55 | 54 | impcom 445 |
. . . 4
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿)))) |
56 | 55 | impcom 445 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))) |
57 | | elfz2nn0 12300 |
. . 3
⊢ ((𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ↔ ((𝑀 + 𝐾) ∈ ℕ0 ∧ (𝑀 + 𝐿) ∈ ℕ0 ∧ (𝑀 + 𝐾) ≤ (𝑀 + 𝐿))) |
58 | 56, 57 | sylibr 223 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿))) |
59 | | elfz2nn0 12300 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ (0...(#‘𝑊)) ↔ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊))) |
60 | 28 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐾 ≤ 𝐿 → ((𝑀 ∈ ℕ0 ∧ (𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ (𝑀 + 𝐿) ∈
ℕ0)) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑀 ∈ ℕ0 ∧ (𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ))
→ (𝑀 + 𝐿) ∈
ℕ0)) |
62 | 61 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) → (𝑀 + 𝐿) ∈
ℕ0) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊))) →
(𝑀 + 𝐿) ∈
ℕ0) |
64 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊))) →
(#‘𝑊) ∈
ℕ0) |
65 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
66 | 65, 35 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ)) |
67 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℝ) |
68 | 66, 67 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ (#‘𝑊) ∈ ℕ0) → ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈
ℝ)) |
69 | | simpllr 795 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ 𝑀 ∈
ℝ) |
70 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ 𝐿 ∈
ℝ) |
71 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ 𝑁 ∈
ℝ) |
72 | 69, 70, 71 | leaddsub2d 10508 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ ((𝑀 + 𝐿) ≤ 𝑁 ↔ 𝐿 ≤ (𝑁 − 𝑀))) |
73 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
⊢ ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑀 + 𝐿) ∈ ℝ) |
74 | 73 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
⊢ (𝑀 ∈ ℝ → (𝐿 ∈ ℝ → (𝑀 + 𝐿) ∈ ℝ)) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (𝐿 ∈ ℝ → (𝑀 + 𝐿) ∈ ℝ)) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
→ (𝐿 ∈ ℝ
→ (𝑀 + 𝐿) ∈
ℝ)) |
77 | 76 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ (𝑀 + 𝐿) ∈
ℝ) |
78 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
→ (#‘𝑊) ∈
ℝ) |
79 | 78 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ (#‘𝑊) ∈
ℝ) |
80 | | letr 10010 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
⊢ (((𝑀 + 𝐿) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) →
(((𝑀 + 𝐿) ≤ 𝑁 ∧ 𝑁 ≤ (#‘𝑊)) → (𝑀 + 𝐿) ≤ (#‘𝑊))) |
81 | 80 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
⊢ (((𝑀 + 𝐿) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((𝑀 + 𝐿) ≤ 𝑁 → (𝑁 ≤ (#‘𝑊) → (𝑀 + 𝐿) ≤ (#‘𝑊)))) |
82 | 77, 71, 79, 81 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ ((𝑀 + 𝐿) ≤ 𝑁 → (𝑁 ≤ (#‘𝑊) → (𝑀 + 𝐿) ≤ (#‘𝑊)))) |
83 | 82 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
⊢
(((((𝑁 ∈
ℝ ∧ 𝑀 ∈
ℝ) ∧ (#‘𝑊)
∈ ℝ) ∧ 𝐿
∈ ℝ) ∧ (𝑀 +
𝐿) ≤ 𝑁) → (𝑁 ≤ (#‘𝑊) → (𝑀 + 𝐿) ≤ (#‘𝑊))) |
84 | 83 | a1dd 48 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢
(((((𝑁 ∈
ℝ ∧ 𝑀 ∈
ℝ) ∧ (#‘𝑊)
∈ ℝ) ∧ 𝐿
∈ ℝ) ∧ (𝑀 +
𝐿) ≤ 𝑁) → (𝑁 ≤ (#‘𝑊) → (0 ≤ 𝐿 → (𝑀 + 𝐿) ≤ (#‘𝑊)))) |
85 | 84 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ ((𝑀 + 𝐿) ≤ 𝑁 → (𝑁 ≤ (#‘𝑊) → (0 ≤ 𝐿 → (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
86 | 72, 85 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ (𝐿 ≤ (𝑁 − 𝑀) → (𝑁 ≤ (#‘𝑊) → (0 ≤ 𝐿 → (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
87 | 86 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ ((((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ) ∧
(#‘𝑊) ∈ ℝ)
∧ 𝐿 ∈ ℝ)
→ (𝑁 ≤
(#‘𝑊) → (𝐿 ≤ (𝑁 − 𝑀) → (0 ≤ 𝐿 → (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
88 | 68, 12, 87 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ ((((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ (#‘𝑊) ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑁 ≤ (#‘𝑊) → (𝐿 ≤ (𝑁 − 𝑀) → (0 ≤ 𝐿 → (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
89 | 88 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ (#‘𝑊) ∈ ℕ0) → (𝐿 ∈ ℤ → (𝑁 ≤ (#‘𝑊) → (𝐿 ≤ (𝑁 − 𝑀) → (0 ≤ 𝐿 → (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
90 | 89 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) ∧ (#‘𝑊) ∈ ℕ0) → (0 ≤
𝐿 → (𝑁 ≤ (#‘𝑊) → (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
91 | 90 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → ((#‘𝑊) ∈ ℕ0 → (0 ≤
𝐿 → (𝑁 ≤ (#‘𝑊) → (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → (𝑀 + 𝐿) ≤ (#‘𝑊))))))) |
92 | 91 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
ℕ0) → (𝑁 ≤ (#‘𝑊) → (0 ≤ 𝐿 → ((#‘𝑊) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → (𝑀 + 𝐿) ≤ (#‘𝑊))))))) |
93 | 92 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑁 ∈ ℕ0
→ (𝑀 ∈
ℕ0 → (𝑁 ≤ (#‘𝑊) → (0 ≤ 𝐿 → ((#‘𝑊) ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → (𝑀 + 𝐿) ≤ (#‘𝑊)))))))) |
94 | 93 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑁 ∈ ℕ0
→ ((#‘𝑊) ∈
ℕ0 → (𝑁 ≤ (#‘𝑊) → (0 ≤ 𝐿 → (𝑀 ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → (𝑀 + 𝐿) ≤ (#‘𝑊)))))))) |
95 | 94 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) → (0
≤ 𝐿 → (𝑀 ∈ ℕ0
→ (𝐿 ≤ (𝑁 − 𝑀) → (𝐿 ∈ ℤ → (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
96 | 95 | com15 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝐿 ∈ ℤ → (0 ≤
𝐿 → (𝑀 ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
97 | 96 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐿 → (𝑀 ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
98 | 15, 97 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((0 ≤
𝐾 ∧ 𝐾 ≤ 𝐿) → (𝑀 ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
99 | 98 | expd 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐾 → (𝐾 ≤ 𝐿 → (𝑀 ∈ ℕ0 → (𝐿 ≤ (𝑁 − 𝑀) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊))))))) |
100 | 99 | com35 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐾 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑀 ∈ ℕ0 → (𝐾 ≤ 𝐿 → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊))))))) |
101 | 100 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐾 ≤ 𝐿 → (𝐿 ≤ (𝑁 − 𝑀) → (𝑀 ∈ ℕ0 → (0 ≤
𝐾 → ((𝑁 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊))))))) |
102 | 101 | impd 446 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝑀 ∈ ℕ0 → (0 ≤
𝐾 → ((𝑁 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
103 | 102 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (0 ≤
𝐾 → (𝑀 ∈ ℕ0 → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
104 | 103 | impancom 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐾 ∈ ℤ ∧ 0 ≤
𝐾) → (𝐿 ∈ ℤ → (𝑀 ∈ ℕ0
→ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
105 | 8, 104 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐾 ∈ ℕ0
→ (𝐿 ∈ ℤ
→ (𝑀 ∈
ℕ0 → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
106 | 105 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ (𝑀 ∈
ℕ0 → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊))))) |
107 | 106 | impcom 445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) → ((𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊)))) |
108 | 107 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 + 𝐿) ≤ (#‘𝑊))) |
109 | 108 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊))) →
(𝑀 + 𝐿) ≤ (#‘𝑊)) |
110 | 63, 64, 109 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑀 ∈ ℕ0
∧ (𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ)) ∧ (𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) ∧ (𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊))) →
((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))) |
111 | 110 | exp41 636 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 ∈ ℕ0
→ ((𝐾 ∈
ℕ0 ∧ 𝐿
∈ ℤ) → ((𝐾
≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
112 | 111 | com24 93 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑀 ∈ ℕ0
→ ((𝑁 ∈
ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 𝑁 ≤ (#‘𝑊)) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
113 | 112 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝑀
≤ 𝑁) → ((𝑁 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
114 | 4, 113 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ (0...𝑁) → ((𝑁 ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
115 | 114 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ0 ∧ 𝑁
≤ (#‘𝑊)) →
(𝑀 ∈ (0...𝑁) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
116 | 59, 115 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (0...(#‘𝑊)) → (𝑀 ∈ (0...𝑁) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
117 | 116 | imp 444 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
118 | 117 | 3adant1 1072 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
119 | 118 | com13 86 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℕ0
∧ 𝐿 ∈ ℤ)
→ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
120 | 119 | ex 449 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ (𝐿 ∈ ℤ
→ ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
121 | 120 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 − 𝑀) ∈ ℕ0
∧ 𝐾 ≤ (𝑁 − 𝑀)) → (𝐿 ∈ ℤ → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
122 | 3, 121 | sylbi 206 |
. . . . . . . . 9
⊢ (𝐾 ∈ (0...(𝑁 − 𝑀)) → (𝐿 ∈ ℤ → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
123 | 122 | com3l 87 |
. . . . . . . 8
⊢ (𝐿 ∈ ℤ → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
124 | 123 | 3ad2ant3 1077 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀)) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))))) |
125 | 124 | imp 444 |
. . . . . 6
⊢ (((𝐾 ∈ ℤ ∧ (𝑁 − 𝑀) ∈ ℤ ∧ 𝐿 ∈ ℤ) ∧ (𝐾 ≤ 𝐿 ∧ 𝐿 ≤ (𝑁 − 𝑀))) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
126 | 2, 125 | sylbi 206 |
. . . . 5
⊢ (𝐿 ∈ (𝐾...(𝑁 − 𝑀)) → (𝐾 ∈ (0...(𝑁 − 𝑀)) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))))) |
127 | 126 | impcom 445 |
. . . 4
⊢ ((𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀))) → ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊)))) |
128 | 127 | impcom 445 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))) |
129 | | elfz2nn0 12300 |
. . 3
⊢ ((𝑀 + 𝐿) ∈ (0...(#‘𝑊)) ↔ ((𝑀 + 𝐿) ∈ ℕ0 ∧
(#‘𝑊) ∈
ℕ0 ∧ (𝑀 + 𝐿) ≤ (#‘𝑊))) |
130 | 128, 129 | sylibr 223 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑀 + 𝐿) ∈ (0...(#‘𝑊))) |
131 | 1, 58, 130 | 3jca 1235 |
1
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊)) ∧ 𝑀 ∈ (0...𝑁)) ∧ (𝐾 ∈ (0...(𝑁 − 𝑀)) ∧ 𝐿 ∈ (𝐾...(𝑁 − 𝑀)))) → (𝑊 ∈ Word 𝑉 ∧ (𝑀 + 𝐾) ∈ (0...(𝑀 + 𝐿)) ∧ (𝑀 + 𝐿) ∈ (0...(#‘𝑊)))) |