Proof of Theorem clwlkisclwwlklem2fv2
Step | Hyp | Ref
| Expression |
1 | | clwlkisclwwlklem2.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) |
2 | 1 | a1i 11 |
. 2
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})))) |
3 | | simpr 476 |
. . . . . . . . . 10
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → 𝑥 = ((#‘𝑃) − 2)) |
4 | | nn0z 11277 |
. . . . . . . . . . . . . 14
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℤ) |
5 | | 2z 11286 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℤ |
6 | 4, 5 | jctir 559 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) ∈ ℤ ∧ 2 ∈
ℤ)) |
7 | | zsubcl 11296 |
. . . . . . . . . . . . 13
⊢
(((#‘𝑃) ∈
ℤ ∧ 2 ∈ ℤ) → ((#‘𝑃) − 2) ∈
ℤ) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 2) ∈
ℤ) |
9 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) ∈
ℤ) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → ((#‘𝑃) − 2) ∈
ℤ) |
11 | 3, 10 | eqeltrd 2688 |
. . . . . . . . 9
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → 𝑥 ∈ ℤ) |
12 | 11 | ex 449 |
. . . . . . . 8
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (𝑥 = ((#‘𝑃) − 2) → 𝑥 ∈ ℤ)) |
13 | | zre 11258 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℝ) |
14 | | nn0re 11178 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℕ0 → (#‘𝑃) ∈ ℝ) |
15 | | 2re 10967 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
16 | 15 | a1i 11 |
. . . . . . . . . . . . 13
⊢
((#‘𝑃) ∈
ℕ0 → 2 ∈ ℝ) |
17 | 14, 16 | resubcld 10337 |
. . . . . . . . . . . 12
⊢
((#‘𝑃) ∈
ℕ0 → ((#‘𝑃) − 2) ∈
ℝ) |
18 | 17 | adantr 480 |
. . . . . . . . . . 11
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) ∈
ℝ) |
19 | | lttri3 10000 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧
((#‘𝑃) − 2)
∈ ℝ) → (𝑥 =
((#‘𝑃) − 2)
↔ (¬ 𝑥 <
((#‘𝑃) − 2)
∧ ¬ ((#‘𝑃)
− 2) < 𝑥))) |
20 | 13, 18, 19 | syl2anr 494 |
. . . . . . . . . 10
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 ∈ ℤ) → (𝑥 = ((#‘𝑃) − 2) ↔ (¬ 𝑥 < ((#‘𝑃) − 2) ∧ ¬
((#‘𝑃) − 2)
< 𝑥))) |
21 | | simpl 472 |
. . . . . . . . . 10
⊢ ((¬
𝑥 < ((#‘𝑃) − 2) ∧ ¬
((#‘𝑃) − 2)
< 𝑥) → ¬ 𝑥 < ((#‘𝑃) − 2)) |
22 | 20, 21 | syl6bi 242 |
. . . . . . . . 9
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 ∈ ℤ) → (𝑥 = ((#‘𝑃) − 2) → ¬ 𝑥 < ((#‘𝑃) − 2))) |
23 | 22 | ex 449 |
. . . . . . . 8
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (𝑥 ∈ ℤ → (𝑥 = ((#‘𝑃) − 2) → ¬ 𝑥 < ((#‘𝑃) − 2)))) |
24 | 12, 23 | syld 46 |
. . . . . . 7
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (𝑥 = ((#‘𝑃) − 2) → (𝑥 = ((#‘𝑃) − 2) → ¬ 𝑥 < ((#‘𝑃) − 2)))) |
25 | 24 | com13 86 |
. . . . . 6
⊢ (𝑥 = ((#‘𝑃) − 2) → (𝑥 = ((#‘𝑃) − 2) → (((#‘𝑃) ∈ ℕ0
∧ 2 ≤ (#‘𝑃))
→ ¬ 𝑥 <
((#‘𝑃) −
2)))) |
26 | 25 | pm2.43i 50 |
. . . . 5
⊢ (𝑥 = ((#‘𝑃) − 2) → (((#‘𝑃) ∈ ℕ0
∧ 2 ≤ (#‘𝑃))
→ ¬ 𝑥 <
((#‘𝑃) −
2))) |
27 | 26 | impcom 445 |
. . . 4
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → ¬ 𝑥 < ((#‘𝑃) − 2)) |
28 | 27 | iffalsed 4047 |
. . 3
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})) = (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})) |
29 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = ((#‘𝑃) − 2) → (𝑃‘𝑥) = (𝑃‘((#‘𝑃) − 2))) |
30 | 29 | adantl 481 |
. . . . 5
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → (𝑃‘𝑥) = (𝑃‘((#‘𝑃) − 2))) |
31 | 30 | preq1d 4218 |
. . . 4
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → {(𝑃‘𝑥), (𝑃‘0)} = {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) |
32 | 31 | fveq2d 6107 |
. . 3
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
33 | 28, 32 | eqtrd 2644 |
. 2
⊢
((((#‘𝑃)
∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) ∧ 𝑥 = ((#‘𝑃) − 2)) → if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)})) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |
34 | 6 | adantr 480 |
. . . . 5
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) ∈ ℤ ∧ 2 ∈
ℤ)) |
35 | 34, 7 | syl 17 |
. . . 4
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) ∈
ℤ) |
36 | 14, 16 | subge0d 10496 |
. . . . 5
⊢
((#‘𝑃) ∈
ℕ0 → (0 ≤ ((#‘𝑃) − 2) ↔ 2 ≤ (#‘𝑃))) |
37 | 36 | biimpar 501 |
. . . 4
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → 0 ≤ ((#‘𝑃) − 2)) |
38 | | elnn0z 11267 |
. . . 4
⊢
(((#‘𝑃)
− 2) ∈ ℕ0 ↔ (((#‘𝑃) − 2) ∈ ℤ ∧ 0 ≤
((#‘𝑃) −
2))) |
39 | 35, 37, 38 | sylanbrc 695 |
. . 3
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) ∈
ℕ0) |
40 | | nn0ge2m1nn 11237 |
. . 3
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 1) ∈
ℕ) |
41 | | 1red 9934 |
. . . 4
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → 1 ∈ ℝ) |
42 | 15 | a1i 11 |
. . . 4
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → 2 ∈ ℝ) |
43 | 14 | adantr 480 |
. . . 4
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (#‘𝑃) ∈ ℝ) |
44 | | 1lt2 11071 |
. . . . 5
⊢ 1 <
2 |
45 | 44 | a1i 11 |
. . . 4
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → 1 < 2) |
46 | 41, 42, 43, 45 | ltsub2dd 10519 |
. . 3
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) < ((#‘𝑃) − 1)) |
47 | | elfzo0 12376 |
. . 3
⊢
(((#‘𝑃)
− 2) ∈ (0..^((#‘𝑃) − 1)) ↔ (((#‘𝑃) − 2) ∈
ℕ0 ∧ ((#‘𝑃) − 1) ∈ ℕ ∧
((#‘𝑃) − 2)
< ((#‘𝑃) −
1))) |
48 | 39, 40, 46, 47 | syl3anbrc 1239 |
. 2
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → ((#‘𝑃) − 2) ∈ (0..^((#‘𝑃) − 1))) |
49 | | fvex 6113 |
. . 3
⊢ (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) ∈ V |
50 | 49 | a1i 11 |
. 2
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)}) ∈ V) |
51 | 2, 33, 48, 50 | fvmptd 6197 |
1
⊢
(((#‘𝑃) ∈
ℕ0 ∧ 2 ≤ (#‘𝑃)) → (𝐹‘((#‘𝑃) − 2)) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) |