Proof of Theorem crctcsh1wlkn0lem4
Step | Hyp | Ref
| Expression |
1 | | crctcsh1wlkn0lem.p |
. . . . 5
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) |
2 | | crctcsh1wlkn0lem.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) |
3 | | elfzoelz 12339 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → 𝑗 ∈ ℤ) |
4 | 3 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → 𝑗 ∈ ℂ) |
5 | 4 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 𝑗 ∈ ℂ) |
6 | | elfzoelz 12339 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℤ) |
7 | 6 | zcnd 11359 |
. . . . . . . . . 10
⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ ℂ) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 𝑆 ∈ ℂ) |
9 | | 1cnd 9935 |
. . . . . . . . 9
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 1 ∈
ℂ) |
10 | 5, 8, 9 | add32d 10142 |
. . . . . . . 8
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) |
11 | | elfzo1 12385 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (1..^𝑁) ↔ (𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) |
12 | | nnnn0 11176 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℕ0) |
13 | | elfzonn0 12380 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → 𝑗 ∈ ℕ0) |
14 | | nn0addcl 11205 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ0
∧ 𝑆 ∈
ℕ0) → (𝑗 + 𝑆) ∈
ℕ0) |
15 | 14 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ0
→ (𝑆 ∈
ℕ0 → (𝑗 + 𝑆) ∈
ℕ0)) |
16 | 13, 15 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → (𝑆 ∈ ℕ0 → (𝑗 + 𝑆) ∈
ℕ0)) |
17 | 12, 16 | syl5com 31 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ ℕ → (𝑗 ∈ (0..^(𝑁 − 𝑆)) → (𝑗 + 𝑆) ∈
ℕ0)) |
18 | 17 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 ∈ (0..^(𝑁 − 𝑆)) → (𝑗 + 𝑆) ∈
ℕ0)) |
19 | 11, 18 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → (𝑗 ∈ (0..^(𝑁 − 𝑆)) → (𝑗 + 𝑆) ∈
ℕ0)) |
20 | 19 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑗 + 𝑆) ∈
ℕ0) |
21 | | fzo0ss1 12367 |
. . . . . . . . . . . . . 14
⊢
(1..^𝑁) ⊆
(0..^𝑁) |
22 | 21 | sseli 3564 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (1..^𝑁) → 𝑆 ∈ (0..^𝑁)) |
23 | | elfzo0 12376 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ (0..^𝑁) ↔ (𝑆 ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁)) |
24 | 23 | simp2bi 1070 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ (0..^𝑁) → 𝑁 ∈ ℕ) |
25 | 22, 24 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ ℕ) |
26 | 25 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 𝑁 ∈ ℕ) |
27 | | elfzo0 12376 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) ↔ (𝑗 ∈ ℕ0 ∧ (𝑁 − 𝑆) ∈ ℕ ∧ 𝑗 < (𝑁 − 𝑆))) |
28 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℝ) |
29 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℝ) |
30 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
31 | 29, 30 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑆 ∈ ℝ ∧ 𝑁 ∈
ℝ)) |
32 | 31 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
33 | 11, 32 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ (1..^𝑁) → (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
34 | 28, 33 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ0
∧ 𝑆 ∈ (1..^𝑁)) → (𝑗 ∈ ℝ ∧ (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
35 | | 3anass 1035 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) ↔ (𝑗 ∈ ℝ ∧ (𝑆 ∈ ℝ ∧ 𝑁 ∈
ℝ))) |
36 | 34, 35 | sylibr 223 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℕ0
∧ 𝑆 ∈ (1..^𝑁)) → (𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
37 | | ltaddsub 10381 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑗 + 𝑆) < 𝑁 ↔ 𝑗 < (𝑁 − 𝑆))) |
38 | 37 | bicomd 212 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝑗 < (𝑁 − 𝑆) ↔ (𝑗 + 𝑆) < 𝑁)) |
39 | 36, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ0
∧ 𝑆 ∈ (1..^𝑁)) → (𝑗 < (𝑁 − 𝑆) ↔ (𝑗 + 𝑆) < 𝑁)) |
40 | 39 | biimpd 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ0
∧ 𝑆 ∈ (1..^𝑁)) → (𝑗 < (𝑁 − 𝑆) → (𝑗 + 𝑆) < 𝑁)) |
41 | 40 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ ℕ0
→ (𝑆 ∈ (1..^𝑁) → (𝑗 < (𝑁 − 𝑆) → (𝑗 + 𝑆) < 𝑁))) |
42 | 41 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ (𝑗 < (𝑁 − 𝑆) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁))) |
43 | 42 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
→ ((𝑁 − 𝑆) ∈ ℕ → (𝑗 < (𝑁 − 𝑆) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁)))) |
44 | 43 | 3imp 1249 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℕ0
∧ (𝑁 − 𝑆) ∈ ℕ ∧ 𝑗 < (𝑁 − 𝑆)) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁)) |
45 | 27, 44 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → (𝑆 ∈ (1..^𝑁) → (𝑗 + 𝑆) < 𝑁)) |
46 | 45 | impcom 445 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑗 + 𝑆) < 𝑁) |
47 | | elfzo0 12376 |
. . . . . . . . . . 11
⊢ ((𝑗 + 𝑆) ∈ (0..^𝑁) ↔ ((𝑗 + 𝑆) ∈ ℕ0 ∧ 𝑁 ∈ ℕ ∧ (𝑗 + 𝑆) < 𝑁)) |
48 | 20, 26, 46, 47 | syl3anbrc 1239 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑗 + 𝑆) ∈ (0..^𝑁)) |
49 | 48 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → (𝑗 + 𝑆) ∈ (0..^𝑁)) |
50 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 𝑆) → (𝑃‘𝑖) = (𝑃‘(𝑗 + 𝑆))) |
51 | 50 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (𝑃‘𝑖) = (𝑃‘(𝑗 + 𝑆))) |
52 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 𝑆) → (𝑖 + 1) = ((𝑗 + 𝑆) + 1)) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 𝑆) → (𝑃‘(𝑖 + 1)) = (𝑃‘((𝑗 + 𝑆) + 1))) |
54 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → (𝑃‘((𝑗 + 𝑆) + 1)) = (𝑃‘((𝑗 + 1) + 𝑆))) |
56 | 53, 55 | sylan9eqr 2666 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (𝑃‘(𝑖 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆))) |
57 | 51, 56 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → ((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)) ↔ (𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)))) |
58 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 𝑆) → (𝐹‘𝑖) = (𝐹‘(𝑗 + 𝑆))) |
59 | 58 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 𝑆) → (𝐼‘(𝐹‘𝑖)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) |
60 | 50 | sneqd 4137 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 𝑆) → {(𝑃‘𝑖)} = {(𝑃‘(𝑗 + 𝑆))}) |
61 | 59, 60 | eqeq12d 2625 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 + 𝑆) → ((𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)} ↔ (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))})) |
62 | 61 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → ((𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)} ↔ (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))})) |
63 | 51, 56 | preq12d 4220 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} = {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))}) |
64 | 59 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (𝐼‘(𝐹‘𝑖)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) |
65 | 63, 64 | sseq12d 3597 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → ({(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)) ↔ {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))) |
66 | 57, 62, 65 | ifpbi123d 1021 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) ∧ 𝑖 = (𝑗 + 𝑆)) → (if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) ↔ if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))) |
67 | 49, 66 | rspcdv 3285 |
. . . . . . . 8
⊢ (((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) ∧ ((𝑗 + 𝑆) + 1) = ((𝑗 + 1) + 𝑆)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))) |
68 | 10, 67 | mpdan 699 |
. . . . . . 7
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))) |
69 | 2, 68 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))) |
70 | 69 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑗 ∈ (0..^(𝑁 − 𝑆)) → (∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))))) |
71 | 1, 70 | mpid 43 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ (0..^(𝑁 − 𝑆)) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))) |
72 | 71 | imp 444 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))) |
73 | | elfzofz 12354 |
. . . . 5
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → 𝑗 ∈ (0...(𝑁 − 𝑆))) |
74 | | crctcsh1wlkn0lem.q |
. . . . . 6
⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) |
75 | 2, 74 | crctcsh1wlkn0lem2 41014 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 𝑆))) → (𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆))) |
76 | 73, 75 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆))) |
77 | | fzofzp1 12431 |
. . . . 5
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → (𝑗 + 1) ∈ (0...(𝑁 − 𝑆))) |
78 | 2, 74 | crctcsh1wlkn0lem2 41014 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁 − 𝑆))) → (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆))) |
79 | 77, 78 | sylan2 490 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆))) |
80 | | crctcsh1wlkn0lem.h |
. . . . . . 7
⊢ 𝐻 = (𝐹 cyclShift 𝑆) |
81 | 80 | fveq1i 6104 |
. . . . . 6
⊢ (𝐻‘𝑗) = ((𝐹 cyclShift 𝑆)‘𝑗) |
82 | | crctcsh1wlkn0lem.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ Word 𝐴) |
83 | 82 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 𝐹 ∈ Word 𝐴) |
84 | 2, 6 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ ℤ) |
85 | 84 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 𝑆 ∈ ℤ) |
86 | | nnz 11276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
87 | 86 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑁 ∈
ℤ) |
88 | | nnz 11276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ ℕ → 𝑆 ∈
ℤ) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 𝑆 ∈
ℤ) |
90 | 87, 89 | zsubcld 11363 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 − 𝑆) ∈ ℤ) |
91 | 12 | nn0ge0d 11231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑆 ∈ ℕ → 0 ≤
𝑆) |
92 | 91 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → 0 ≤
𝑆) |
93 | | subge02 10423 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (0 ≤
𝑆 ↔ (𝑁 − 𝑆) ≤ 𝑁)) |
94 | 30, 29, 93 | syl2anr 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (0 ≤
𝑆 ↔ (𝑁 − 𝑆) ≤ 𝑁)) |
95 | 92, 94 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑁 − 𝑆) ≤ 𝑁) |
96 | 90, 87, 95 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑁 − 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 𝑆) ≤ 𝑁)) |
97 | 96 | 3adant3 1074 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → ((𝑁 − 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 𝑆) ≤ 𝑁)) |
98 | 11, 97 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (1..^𝑁) → ((𝑁 − 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 𝑆) ≤ 𝑁)) |
99 | | eluz2 11569 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 𝑆)) ↔ ((𝑁 − 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 𝑆) ≤ 𝑁)) |
100 | 98, 99 | sylibr 223 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (1..^𝑁) → 𝑁 ∈ (ℤ≥‘(𝑁 − 𝑆))) |
101 | | fzoss2 12365 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘(𝑁 − 𝑆)) → (0..^(𝑁 − 𝑆)) ⊆ (0..^𝑁)) |
102 | 2, 100, 101 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (0..^(𝑁 − 𝑆)) ⊆ (0..^𝑁)) |
103 | 102 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 𝑗 ∈ (0..^𝑁)) |
104 | | crctcsh1wlkn0lem.n |
. . . . . . . . . 10
⊢ 𝑁 = (#‘𝐹) |
105 | 104 | oveq2i 6560 |
. . . . . . . . 9
⊢
(0..^𝑁) =
(0..^(#‘𝐹)) |
106 | 103, 105 | syl6eleq 2698 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → 𝑗 ∈ (0..^(#‘𝐹))) |
107 | | cshwidxmod 13400 |
. . . . . . . 8
⊢ ((𝐹 ∈ Word 𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝑗 ∈ (0..^(#‘𝐹))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))) |
108 | 83, 85, 106, 107 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹)))) |
109 | 104 | eqcomi 2619 |
. . . . . . . . . 10
⊢
(#‘𝐹) = 𝑁 |
110 | 109 | oveq2i 6560 |
. . . . . . . . 9
⊢ ((𝑗 + 𝑆) mod (#‘𝐹)) = ((𝑗 + 𝑆) mod 𝑁) |
111 | 18 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑗 + 𝑆) ∈
ℕ0) |
112 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |
113 | 112 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑁 − 1) ∈
ℕ0) |
114 | 113 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑁 − 1) ∈
ℕ0) |
115 | 28, 32 | anim12i 588 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → (𝑗 ∈ ℝ ∧ (𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ))) |
116 | 115, 35 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → (𝑗 ∈ ℝ ∧ 𝑆 ∈ ℝ ∧ 𝑁 ∈ ℝ)) |
117 | 116, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → (𝑗 < (𝑁 − 𝑆) ↔ (𝑗 + 𝑆) < 𝑁)) |
118 | 12 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑆 ∈
ℕ0) |
119 | 118, 14 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → (𝑗 + 𝑆) ∈
ℕ0) |
120 | 119 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → (𝑗 + 𝑆) ∈ ℤ) |
121 | 86 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → 𝑁 ∈ ℤ) |
122 | 121 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → 𝑁 ∈ ℤ) |
123 | | zltlem1 11307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑗 + 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑗 + 𝑆) < 𝑁 ↔ (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
124 | 120, 122,
123 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → ((𝑗 + 𝑆) < 𝑁 ↔ (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
125 | 124 | biimpd 218 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → ((𝑗 + 𝑆) < 𝑁 → (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
126 | 117, 125 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ ℕ0
∧ (𝑆 ∈ ℕ
∧ 𝑁 ∈ ℕ
∧ 𝑆 < 𝑁)) → (𝑗 < (𝑁 − 𝑆) → (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
127 | 126 | impancom 455 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑗 ∈ ℕ0
∧ 𝑗 < (𝑁 − 𝑆)) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
128 | 127 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ ℕ0
∧ (𝑁 − 𝑆) ∈ ℕ ∧ 𝑗 < (𝑁 − 𝑆)) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
129 | 27, 128 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ (0..^(𝑁 − 𝑆)) → ((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) → (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
130 | 129 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑗 + 𝑆) ≤ (𝑁 − 1)) |
131 | 111, 114,
130 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑆 < 𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝑗 + 𝑆) ∈ ℕ0 ∧ (𝑁 − 1) ∈
ℕ0 ∧ (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
132 | 11, 131 | sylanb 488 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝑗 + 𝑆) ∈ ℕ0 ∧ (𝑁 − 1) ∈
ℕ0 ∧ (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
133 | | elfz2nn0 12300 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 𝑆) ∈ (0...(𝑁 − 1)) ↔ ((𝑗 + 𝑆) ∈ ℕ0 ∧ (𝑁 − 1) ∈
ℕ0 ∧ (𝑗 + 𝑆) ≤ (𝑁 − 1))) |
134 | 132, 133 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑗 + 𝑆) ∈ (0...(𝑁 − 1))) |
135 | | zaddcl 11294 |
. . . . . . . . . . . . 13
⊢ ((𝑗 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑗 + 𝑆) ∈ ℤ) |
136 | 3, 6, 135 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝑗 + 𝑆) ∈ ℤ) |
137 | | zmodid2 12560 |
. . . . . . . . . . . 12
⊢ (((𝑗 + 𝑆) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆) ↔ (𝑗 + 𝑆) ∈ (0...(𝑁 − 1)))) |
138 | 136, 26, 137 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆) ↔ (𝑗 + 𝑆) ∈ (0...(𝑁 − 1)))) |
139 | 134, 138 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (1..^𝑁) ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆)) |
140 | 2, 139 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝑗 + 𝑆) mod 𝑁) = (𝑗 + 𝑆)) |
141 | 110, 140 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝑗 + 𝑆) mod (#‘𝐹)) = (𝑗 + 𝑆)) |
142 | 141 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝐹‘((𝑗 + 𝑆) mod (#‘𝐹))) = (𝐹‘(𝑗 + 𝑆))) |
143 | 108, 142 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → ((𝐹 cyclShift 𝑆)‘𝑗) = (𝐹‘(𝑗 + 𝑆))) |
144 | 81, 143 | syl5eq 2656 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝐻‘𝑗) = (𝐹‘(𝑗 + 𝑆))) |
145 | 144 | fveq2d 6107 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) |
146 | | simp1 1054 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆))) |
147 | | simp2 1055 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆))) |
148 | 146, 147 | eqeq12d 2625 |
. . . . 5
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → ((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)) ↔ (𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)))) |
149 | | simp3 1056 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) |
150 | 146 | sneqd 4137 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → {(𝑄‘𝑗)} = {(𝑃‘(𝑗 + 𝑆))}) |
151 | 149, 150 | eqeq12d 2625 |
. . . . 5
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → ((𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)} ↔ (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))})) |
152 | 146, 147 | preq12d 4220 |
. . . . . 6
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} = {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))}) |
153 | 152, 149 | sseq12d 3597 |
. . . . 5
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → ({(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)) ↔ {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆))))) |
154 | 148, 151,
153 | ifpbi123d 1021 |
. . . 4
⊢ (((𝑄‘𝑗) = (𝑃‘(𝑗 + 𝑆)) ∧ (𝑄‘(𝑗 + 1)) = (𝑃‘((𝑗 + 1) + 𝑆)) ∧ (𝐼‘(𝐻‘𝑗)) = (𝐼‘(𝐹‘(𝑗 + 𝑆)))) → (if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))) |
155 | 76, 79, 145, 154 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → (if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗))) ↔ if-((𝑃‘(𝑗 + 𝑆)) = (𝑃‘((𝑗 + 1) + 𝑆)), (𝐼‘(𝐹‘(𝑗 + 𝑆))) = {(𝑃‘(𝑗 + 𝑆))}, {(𝑃‘(𝑗 + 𝑆)), (𝑃‘((𝑗 + 1) + 𝑆))} ⊆ (𝐼‘(𝐹‘(𝑗 + 𝑆)))))) |
156 | 72, 155 | mpbird 246 |
. 2
⊢ ((𝜑 ∧ 𝑗 ∈ (0..^(𝑁 − 𝑆))) → if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
157 | 156 | ralrimiva 2949 |
1
⊢ (𝜑 → ∀𝑗 ∈ (0..^(𝑁 − 𝑆))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |