Proof of Theorem crctcshwlkn0lem5
Step | Hyp | Ref
| Expression |
1 | | crctcshwlkn0lem.p |
. . . . 5
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
2 | | crctcshwlkn0lem.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) |
3 | | elfzoelz 13384 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → 𝑗 ∈ ℤ) |
4 | 3 | zcnd 12424 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → 𝑗 ∈ ℂ) |
5 | 4 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑗 ∈ ℂ) |
6 | | 1cnd 10969 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 1 ∈ ℂ) |
7 | | elfzoelz 13384 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ) |
8 | 7 | zcnd 12424 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℂ) |
9 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑆 ∈ ℂ) |
10 | | elfzoel2 13383 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℤ) |
11 | 10 | zcnd 12424 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℂ) |
12 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑁 ∈ ℂ) |
13 | 5, 6, 9, 12 | 2addsubd 11380 |
. . . . . . . . 9
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (((𝑗 + 1) + 𝑆) − 𝑁) = (((𝑗 + 𝑆) − 𝑁) + 1)) |
14 | 13 | eqcomd 2746 |
. . . . . . . 8
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) |
15 | | elfzo1 13433 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) |
16 | | nnz 12340 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
17 | 16 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℤ) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑁 ∈ ℤ) |
19 | 3 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑗 ∈ ℤ) |
20 | | nnz 12340 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℤ) |
21 | 20 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℤ) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑆 ∈ ℤ) |
23 | 19, 22 | zaddcld 12427 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (𝑗 + 𝑆) ∈ ℤ) |
24 | | elfzo2 13387 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) ↔ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) |
25 | | eluz2 12585 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) ↔ (((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑗)) |
26 | | zre 12321 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
ℝ) |
27 | | nnre 11978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℝ) |
28 | | nnre 11978 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
29 | 27, 28 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
30 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → 𝑁 ∈
ℝ) |
31 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → 𝑆 ∈
ℝ) |
32 | 30, 31 | resubcld 11401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → (𝑁 − 𝑆) ∈ ℝ) |
33 | 32 | lep1d 11904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → (𝑁 − 𝑆) ≤ ((𝑁 − 𝑆) + 1)) |
34 | | 1red 10975 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → 1 ∈
ℝ) |
35 | 32, 34 | readdcld 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → ((𝑁 − 𝑆) + 1) ∈ ℝ) |
36 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → 𝑗 ∈
ℝ) |
37 | | letr 11067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑁 − 𝑆) ∈ ℝ ∧ ((𝑁 − 𝑆) + 1) ∈ ℝ ∧ 𝑗 ∈ ℝ) → (((𝑁 − 𝑆) ≤ ((𝑁 − 𝑆) + 1) ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑗) → (𝑁 − 𝑆) ≤ 𝑗)) |
38 | 32, 35, 36, 37 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → (((𝑁 − 𝑆) ≤ ((𝑁 − 𝑆) + 1) ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑗) → (𝑁 − 𝑆) ≤ 𝑗)) |
39 | 33, 38 | mpand 692 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → (((𝑁 − 𝑆) + 1) ≤ 𝑗 → (𝑁 − 𝑆) ≤ 𝑗)) |
40 | 30, 31, 36 | lesubaddd 11570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → ((𝑁 − 𝑆) ≤ 𝑗 ↔ 𝑁 ≤ (𝑗 + 𝑆))) |
41 | 39, 40 | sylibd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℝ) → (((𝑁 − 𝑆) + 1) ≤ 𝑗 → 𝑁 ≤ (𝑗 + 𝑆))) |
42 | 41 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑗 ∈ ℝ → (((𝑁 − 𝑆) + 1) ≤ 𝑗 → 𝑁 ≤ (𝑗 + 𝑆)))) |
43 | 29, 42 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑗 ∈ ℝ → (((𝑁 − 𝑆) + 1) ≤ 𝑗 → 𝑁 ≤ (𝑗 + 𝑆)))) |
44 | 43 | 3adant3 1131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 ∈ ℝ → (((𝑁 − 𝑆) + 1) ≤ 𝑗 → 𝑁 ≤ (𝑗 + 𝑆)))) |
45 | 26, 44 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ ℤ → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (((𝑁 − 𝑆) + 1) ≤ 𝑗 → 𝑁 ≤ (𝑗 + 𝑆)))) |
46 | 45 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ ℤ → (((𝑁 − 𝑆) + 1) ≤ 𝑗 → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ≤ (𝑗 + 𝑆)))) |
47 | 46 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑗) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ≤ (𝑗 + 𝑆))) |
48 | 47 | 3adant1 1129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑗) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ≤ (𝑗 + 𝑆))) |
49 | 25, 48 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ≤ (𝑗 + 𝑆))) |
50 | 49 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ≤ (𝑗 + 𝑆))) |
51 | 50 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁) → 𝑁 ≤ (𝑗 + 𝑆))) |
52 | 24, 51 | syl5bi 241 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → 𝑁 ≤ (𝑗 + 𝑆))) |
53 | 52 | imp 407 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑁 ≤ (𝑗 + 𝑆)) |
54 | | eluz2 12585 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 + 𝑆) ∈ (ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (𝑗 + 𝑆) ∈ ℤ ∧ 𝑁 ≤ (𝑗 + 𝑆))) |
55 | 18, 23, 53, 54 | syl3anbrc 1342 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (𝑗 + 𝑆) ∈ (ℤ≥‘𝑁)) |
56 | | uznn0sub 12614 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 + 𝑆) ∈ (ℤ≥‘𝑁) → ((𝑗 + 𝑆) − 𝑁) ∈
ℕ0) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → ((𝑗 + 𝑆) − 𝑁) ∈
ℕ0) |
58 | | simpl2 1191 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑁 ∈ ℕ) |
59 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → 𝑗 ∈
ℝ) |
60 | | simpll 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → 𝑆 ∈
ℝ) |
61 | | ax-1 6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑁 ∈ ℝ → (𝑆 ∈ ℝ → 𝑁 ∈
ℝ)) |
62 | 61 | imdistanri 570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑁 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → (𝑁 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
64 | | lt2add 11458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ) ∧ (𝑁 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → ((𝑗 < 𝑁 ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) < (𝑁 + 𝑁))) |
65 | 59, 60, 63, 64 | syl21anc 835 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → ((𝑗 < 𝑁 ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) < (𝑁 + 𝑁))) |
66 | 59, 60 | readdcld 11003 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → (𝑗 + 𝑆) ∈ ℝ) |
67 | | simplr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → 𝑁 ∈
ℝ) |
68 | 66, 67, 67 | ltsubaddd 11569 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → (((𝑗 + 𝑆) − 𝑁) < 𝑁 ↔ (𝑗 + 𝑆) < (𝑁 + 𝑁))) |
69 | 65, 68 | sylibrd 258 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝑗 ∈ ℤ) → ((𝑗 < 𝑁 ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁)) |
70 | 69 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑗 ∈ ℤ → ((𝑗 < 𝑁 ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁))) |
71 | 70 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑗 < 𝑁 ∧ 𝑆 < 𝑁) → (𝑗 ∈ ℤ → ((𝑗 + 𝑆) − 𝑁) < 𝑁))) |
72 | 71 | expcomd 417 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → (𝑗 < 𝑁 → (𝑗 ∈ ℤ → ((𝑗 + 𝑆) − 𝑁) < 𝑁)))) |
73 | 29, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → (𝑗 < 𝑁 → (𝑗 ∈ ℤ → ((𝑗 + 𝑆) − 𝑁) < 𝑁)))) |
74 | 73 | 3impia 1116 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 < 𝑁 → (𝑗 ∈ ℤ → ((𝑗 + 𝑆) − 𝑁) < 𝑁))) |
75 | 74 | com13 88 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ ℤ → (𝑗 < 𝑁 → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁))) |
76 | 75 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 − 𝑆) + 1) ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ ((𝑁 − 𝑆) + 1) ≤ 𝑗) → (𝑗 < 𝑁 → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁))) |
77 | 25, 76 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) → (𝑗 < 𝑁 → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁))) |
78 | 77 | imp 407 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑗 < 𝑁) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁)) |
79 | 78 | 3adant2 1130 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁)) |
80 | 24, 79 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 + 𝑆) − 𝑁) < 𝑁)) |
81 | 80 | impcom 408 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → ((𝑗 + 𝑆) − 𝑁) < 𝑁) |
82 | 57, 58, 81 | 3jca 1127 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (((𝑗 + 𝑆) − 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ((𝑗 + 𝑆) − 𝑁) < 𝑁)) |
83 | 15, 82 | sylanb 581 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (((𝑗 + 𝑆) − 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ((𝑗 + 𝑆) − 𝑁) < 𝑁)) |
84 | | elfzo0 13424 |
. . . . . . . . . . 11
⊢ (((𝑗 + 𝑆) − 𝑁) ∈ (0..^𝑁) ↔ (((𝑗 + 𝑆) − 𝑁) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ ((𝑗 + 𝑆) − 𝑁) < 𝑁)) |
85 | 83, 84 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → ((𝑗 + 𝑆) − 𝑁) ∈ (0..^𝑁)) |
86 | 85 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) → ((𝑗 + 𝑆) − 𝑁) ∈ (0..^𝑁)) |
87 | | fveq2 6769 |
. . . . . . . . . . . 12
⊢ (𝑖 = ((𝑗 + 𝑆) − 𝑁) → (𝑃‘𝑖) = (𝑃‘((𝑗 + 𝑆) − 𝑁))) |
88 | 87 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → (𝑃‘𝑖) = (𝑃‘((𝑗 + 𝑆) − 𝑁))) |
89 | | fvoveq1 7292 |
. . . . . . . . . . . 12
⊢ (𝑖 = ((𝑗 + 𝑆) − 𝑁) → (𝑃‘(𝑖 + 1)) = (𝑃‘(((𝑗 + 𝑆) − 𝑁) + 1))) |
90 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) → (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) |
91 | 90 | fveq2d 6773 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) → (𝑃‘(((𝑗 + 𝑆) − 𝑁) + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))) |
92 | 89, 91 | sylan9eqr 2802 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → (𝑃‘(𝑖 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))) |
93 | 88, 92 | eqeq12d 2756 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → ((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) ↔ (𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)))) |
94 | | 2fveq3 6774 |
. . . . . . . . . . . 12
⊢ (𝑖 = ((𝑗 + 𝑆) − 𝑁) → (𝐼‘(𝐹‘𝑖)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) |
95 | 87 | sneqd 4579 |
. . . . . . . . . . . 12
⊢ (𝑖 = ((𝑗 + 𝑆) − 𝑁) → {(𝑃‘𝑖)} = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}) |
96 | 94, 95 | eqeq12d 2756 |
. . . . . . . . . . 11
⊢ (𝑖 = ((𝑗 + 𝑆) − 𝑁) → ((𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)} ↔ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))})) |
97 | 96 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → ((𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)} ↔ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))})) |
98 | 88, 92 | preq12d 4683 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))}) |
99 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → 𝑖 = ((𝑗 + 𝑆) − 𝑁)) |
100 | 99 | fveq2d 6773 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → (𝐹‘𝑖) = (𝐹‘((𝑗 + 𝑆) − 𝑁))) |
101 | 100 | fveq2d 6773 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → (𝐼‘(𝐹‘𝑖)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) |
102 | 98, 101 | sseq12d 3959 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) ↔ {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))))) |
103 | 93, 97, 102 | ifpbi123d 1077 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) ∧ 𝑖 = ((𝑗 + 𝑆) − 𝑁)) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))))) |
104 | 86, 103 | rspcdv 3552 |
. . . . . . . 8
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) ∧ (((𝑗 + 𝑆) − 𝑁) + 1) = (((𝑗 + 1) + 𝑆) − 𝑁)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))))) |
105 | 14, 104 | mpdan 684 |
. . . . . . 7
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))))) |
106 | 2, 105 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))))) |
107 | 106 | ex 413 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))))))) |
108 | 1, 107 | mpid 44 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))))) |
109 | 108 | imp 407 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))))) |
110 | | elfzofz 13399 |
. . . . 5
⊢ (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → 𝑗 ∈ (((𝑁 − 𝑆) + 1)...𝑁)) |
111 | | crctcshwlkn0lem.q |
. . . . . 6
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
112 | 2, 111 | crctcshwlkn0lem3 28171 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁))) |
113 | 110, 112 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁))) |
114 | | fzofzp1 13480 |
. . . . 5
⊢ (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → (𝑗 + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) |
115 | 2, 111 | crctcshwlkn0lem3 28171 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 + 1) ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))) |
116 | 114, 115 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))) |
117 | | crctcshwlkn0lem.h |
. . . . . . 7
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
118 | 117 | fveq1i 6770 |
. . . . . 6
⊢ (𝐻‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗) |
119 | | crctcshwlkn0lem.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ Word 𝐴) |
120 | 119 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝐹 ∈ Word 𝐴) |
121 | 2, 7 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℤ) |
122 | 121 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑆 ∈ ℤ) |
123 | | ltle 11062 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁)) |
124 | 29, 123 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 < 𝑁 → 𝑆 ≤ 𝑁)) |
125 | 124 | 3impia 1116 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ≤ 𝑁) |
126 | | nnnn0 12238 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℕ0) |
127 | | nnnn0 12238 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
128 | 126, 127 | anim12i 613 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 ∈ ℕ0
∧ 𝑁 ∈
ℕ0)) |
129 | 128 | 3adant3 1131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑆 ∈ ℕ0 ∧ 𝑁 ∈
ℕ0)) |
130 | | nn0sub 12281 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑆 ≤ 𝑁 ↔ (𝑁 − 𝑆) ∈
ℕ0)) |
131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑆 ≤ 𝑁 ↔ (𝑁 − 𝑆) ∈
ℕ0)) |
132 | 125, 131 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 𝑆) ∈
ℕ0) |
133 | 15, 132 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (1..^𝑁) → (𝑁 − 𝑆) ∈
ℕ0) |
134 | | 1nn0 12247 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℕ0 |
135 | 134 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (1..^𝑁) → 1 ∈
ℕ0) |
136 | 133, 135 | nn0addcld 12295 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈
ℕ0) |
137 | | elnn0uz 12620 |
. . . . . . . . . . . 12
⊢ (((𝑁 − 𝑆) + 1) ∈ ℕ0 ↔
((𝑁 − 𝑆) + 1) ∈
(ℤ≥‘0)) |
138 | 136, 137 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) + 1) ∈
(ℤ≥‘0)) |
139 | | fzoss1 13410 |
. . . . . . . . . . 11
⊢ (((𝑁 − 𝑆) + 1) ∈
(ℤ≥‘0) → (((𝑁 − 𝑆) + 1)..^𝑁) ⊆ (0..^𝑁)) |
140 | 2, 138, 139 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑁 − 𝑆) + 1)..^𝑁) ⊆ (0..^𝑁)) |
141 | 140 | sselda 3926 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑗 ∈ (0..^𝑁)) |
142 | | crctcshwlkn0lem.n |
. . . . . . . . . 10
⊢ 𝑁 = (♯‘𝐹) |
143 | 142 | oveq2i 7280 |
. . . . . . . . 9
⊢
(0..^𝑁) =
(0..^(♯‘𝐹)) |
144 | 141, 143 | eleqtrdi 2851 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → 𝑗 ∈ (0..^(♯‘𝐹))) |
145 | | cshwidxmod 14512 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(♯‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
146 | 120, 122,
144, 145 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹)))) |
147 | 142 | eqcomi 2749 |
. . . . . . . . . 10
⊢
(♯‘𝐹) =
𝑁 |
148 | 147 | oveq2i 7280 |
. . . . . . . . 9
⊢ ((𝑗 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) mod 𝑁) |
149 | | eluzelre 12590 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) → 𝑗 ∈ ℝ) |
150 | 149 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈
(ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁) → 𝑗 ∈ ℝ) |
151 | 150 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → 𝑗 ∈ ℝ) |
152 | 27 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈ ℝ) |
153 | 152 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → 𝑆 ∈ ℝ) |
154 | 151, 153 | readdcld 11003 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → (𝑗 + 𝑆) ∈ ℝ) |
155 | | nnrp 12738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ+) |
156 | 155 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈
ℝ+) |
157 | 156 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → 𝑁 ∈
ℝ+) |
158 | 50 | impcom 408 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → 𝑁 ≤ (𝑗 + 𝑆)) |
159 | 157 | rpred 12769 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → 𝑁 ∈ ℝ) |
160 | | simpr3 1195 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → 𝑗 < 𝑁) |
161 | | simpl3 1192 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → 𝑆 < 𝑁) |
162 | 151, 153,
159, 160, 161 | lt2addmuld 12221 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → (𝑗 + 𝑆) < (2 · 𝑁)) |
163 | 158, 162 | jca 512 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁))) |
164 | 154, 157,
163 | jca31 515 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ (𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁)) → (((𝑗 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁)))) |
165 | 164 | ex 413 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑗 ∈ (ℤ≥‘((𝑁 − 𝑆) + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑗 < 𝑁) → (((𝑗 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁))))) |
166 | 24, 165 | syl5bi 241 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → (((𝑗 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁))))) |
167 | 15, 166 | sylbi 216 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → (((𝑗 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁))))) |
168 | 2, 167 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁) → (((𝑗 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁))))) |
169 | 168 | imp 407 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (((𝑗 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁)))) |
170 | | 2submod 13648 |
. . . . . . . . . 10
⊢ ((((𝑗 + 𝑆) ∈ ℝ ∧ 𝑁 ∈ ℝ+) ∧ (𝑁 ≤ (𝑗 + 𝑆) ∧ (𝑗 + 𝑆) < (2 · 𝑁))) → ((𝑗 + 𝑆) mod 𝑁) = ((𝑗 + 𝑆) − 𝑁)) |
171 | 169, 170 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → ((𝑗 + 𝑆) mod 𝑁) = ((𝑗 + 𝑆) − 𝑁)) |
172 | 148, 171 | eqtrid 2792 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → ((𝑗 + 𝑆) mod (♯‘𝐹)) = ((𝑗 + 𝑆) − 𝑁)) |
173 | 172 | fveq2d 6773 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (𝐹‘((𝑗 + 𝑆) mod (♯‘𝐹))) = (𝐹‘((𝑗 + 𝑆) − 𝑁))) |
174 | 146, 173 | eqtrd 2780 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) − 𝑁))) |
175 | 118, 174 | eqtrid 2792 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (𝐻‘𝑗) = (𝐹‘((𝑗 + 𝑆) − 𝑁))) |
176 | 175 | fveq2d 6773 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) |
177 | | simp1 1135 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → (𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁))) |
178 | | simp2 1136 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))) |
179 | 177, 178 | eqeq12d 2756 |
. . . . 5
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → ((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)) ↔ (𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)))) |
180 | | simp3 1137 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) |
181 | 177 | sneqd 4579 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → {(𝑄‘𝑗)} = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}) |
182 | 180, 181 | eqeq12d 2756 |
. . . . 5
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → ((𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)} ↔ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))})) |
183 | 177, 178 | preq12d 4683 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} = {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))}) |
184 | 183, 180 | sseq12d 3959 |
. . . . 5
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → ({(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)) ↔ {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))))) |
185 | 179, 182,
184 | ifpbi123d 1077 |
. . . 4
⊢ (((𝑄‘𝑗) = (𝑃‘((𝑗 + 𝑆) − 𝑁)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))) → (if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))))) |
186 | 113, 116,
176, 185 | syl3anc 1370 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → (if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ if-((𝑃‘((𝑗 + 𝑆) − 𝑁)) = (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁)), (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁))) = {(𝑃‘((𝑗 + 𝑆) − 𝑁))}, {(𝑃‘((𝑗 + 𝑆) − 𝑁)), (𝑃‘(((𝑗 + 1) + 𝑆) − 𝑁))} ⊆ (𝐼‘(𝐹‘((𝑗 + 𝑆) − 𝑁)))))) |
187 | 109, 186 | mpbird 256 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)) → if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
188 | 187 | ralrimiva 3110 |
1
⊢ (𝜑 → ∀𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |