Proof of Theorem clwlkisclwwlklem2fv1
Step | Hyp | Ref
| Expression |
1 | | clwlkisclwwlklem2.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) |
2 | 1 | a1i 11 |
. 2
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝐼
∈ (0..^((#‘𝑃)
− 2))) → 𝐹 =
(𝑥 ∈
(0..^((#‘𝑃) −
1)) ↦ if(𝑥 <
((#‘𝑃) − 2),
(◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})))) |
3 | | breq1 4586 |
. . . 4
⊢ (𝑥 = 𝐼 → (𝑥 < ((#‘𝑃) − 2) ↔ 𝐼 < ((#‘𝑃) − 2))) |
4 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝐼 → (𝑃‘𝑥) = (𝑃‘𝐼)) |
5 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = 𝐼 → (𝑥 + 1) = (𝐼 + 1)) |
6 | 5 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = 𝐼 → (𝑃‘(𝑥 + 1)) = (𝑃‘(𝐼 + 1))) |
7 | 4, 6 | preq12d 4220 |
. . . . 5
⊢ (𝑥 = 𝐼 → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) |
8 | 7 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = 𝐼 → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |
9 | 4 | preq1d 4218 |
. . . . 5
⊢ (𝑥 = 𝐼 → {(𝑃‘𝑥), (𝑃‘0)} = {(𝑃‘𝐼), (𝑃‘0)}) |
10 | 9 | fveq2d 6107 |
. . . 4
⊢ (𝑥 = 𝐼 → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘0)})) |
11 | 3, 8, 10 | ifbieq12d 4063 |
. . 3
⊢ (𝑥 = 𝐼 → if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})) = if(𝐼 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}), (◡𝐸‘{(𝑃‘𝐼), (𝑃‘0)}))) |
12 | | elfzolt2 12348 |
. . . . 5
⊢ (𝐼 ∈ (0..^((#‘𝑃) − 2)) → 𝐼 < ((#‘𝑃) − 2)) |
13 | 12 | adantl 481 |
. . . 4
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝐼
∈ (0..^((#‘𝑃)
− 2))) → 𝐼 <
((#‘𝑃) −
2)) |
14 | 13 | iftrued 4044 |
. . 3
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝐼
∈ (0..^((#‘𝑃)
− 2))) → if(𝐼
< ((#‘𝑃) −
2), (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}), (◡𝐸‘{(𝑃‘𝐼), (𝑃‘0)})) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |
15 | 11, 14 | sylan9eqr 2666 |
. 2
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 𝐼 ∈ (0..^((#‘𝑃) − 2))) ∧ 𝑥 = 𝐼) → if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |
16 | | nn0z 11277 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℤ) |
17 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
18 | 17 | a1i 11 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℤ) |
19 | 16, 18 | zsubcld 11363 |
. . . . 5
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 2) ∈
ℤ) |
20 | | peano2zm 11297 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℤ → ((#‘𝑃)
− 1) ∈ ℤ) |
21 | 16, 20 | syl 17 |
. . . . 5
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) ∈
ℤ) |
22 | | 1red 9934 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ0 → 1 ∈ ℝ) |
23 | | 2re 10967 |
. . . . . . 7
⊢ 2 ∈
ℝ |
24 | 23 | a1i 11 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℝ) |
25 | | nn0re 11178 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℝ) |
26 | | 1le2 11118 |
. . . . . . 7
⊢ 1 ≤
2 |
27 | 26 | a1i 11 |
. . . . . 6
⊢
((#‘𝑃) ∈
ℕ0 → 1 ≤ 2) |
28 | 22, 24, 25, 27 | lesub2dd 10523 |
. . . . 5
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 2) ≤ ((#‘𝑃) − 1)) |
29 | | eluz2 11569 |
. . . . 5
⊢
(((#‘𝑃)
− 1) ∈ (ℤ≥‘((#‘𝑃) − 2)) ↔ (((#‘𝑃) − 2) ∈ ℤ
∧ ((#‘𝑃) −
1) ∈ ℤ ∧ ((#‘𝑃) − 2) ≤ ((#‘𝑃) − 1))) |
30 | 19, 21, 28, 29 | syl3anbrc 1239 |
. . . 4
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 1) ∈
(ℤ≥‘((#‘𝑃) − 2))) |
31 | | fzoss2 12365 |
. . . 4
⊢
(((#‘𝑃)
− 1) ∈ (ℤ≥‘((#‘𝑃) − 2)) → (0..^((#‘𝑃) − 2)) ⊆
(0..^((#‘𝑃) −
1))) |
32 | 30, 31 | syl 17 |
. . 3
⊢
((#‘𝑃) ∈
ℕ0 → (0..^((#‘𝑃) − 2)) ⊆ (0..^((#‘𝑃) − 1))) |
33 | 32 | sselda 3568 |
. 2
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝐼
∈ (0..^((#‘𝑃)
− 2))) → 𝐼
∈ (0..^((#‘𝑃)
− 1))) |
34 | | fvex 6113 |
. . 3
⊢ (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) ∈ V |
35 | 34 | a1i 11 |
. 2
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝐼
∈ (0..^((#‘𝑃)
− 2))) → (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}) ∈ V) |
36 | 2, 15, 33, 35 | fvmptd 6197 |
1
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 𝐼
∈ (0..^((#‘𝑃)
− 2))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) |