Proof of Theorem subfacp1lem1
Step | Hyp | Ref
| Expression |
1 | | disj 3969 |
. . . 4
⊢ ((𝐾 ∩ {1, 𝑀}) = ∅ ↔ ∀𝑥 ∈ 𝐾 ¬ 𝑥 ∈ {1, 𝑀}) |
2 | | eldifi 3694 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → 𝑥 ∈ (2...(𝑁 + 1))) |
3 | | elfzle1 12215 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2...(𝑁 + 1)) → 2 ≤ 𝑥) |
4 | | 1lt2 11071 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
5 | | 1re 9918 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℝ |
6 | | 2re 10967 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
7 | 5, 6 | ltnlei 10037 |
. . . . . . . . . . . 12
⊢ (1 < 2
↔ ¬ 2 ≤ 1) |
8 | 4, 7 | mpbi 219 |
. . . . . . . . . . 11
⊢ ¬ 2
≤ 1 |
9 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (2 ≤ 𝑥 ↔ 2 ≤
1)) |
10 | 8, 9 | mtbiri 316 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → ¬ 2 ≤ 𝑥) |
11 | 10 | necon2ai 2811 |
. . . . . . . . 9
⊢ (2 ≤
𝑥 → 𝑥 ≠ 1) |
12 | 2, 3, 11 | 3syl 18 |
. . . . . . . 8
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → 𝑥 ≠ 1) |
13 | | eldifsni 4261 |
. . . . . . . 8
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → 𝑥 ≠ 𝑀) |
14 | 12, 13 | jca 553 |
. . . . . . 7
⊢ (𝑥 ∈ ((2...(𝑁 + 1)) ∖ {𝑀}) → (𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀)) |
15 | | subfacp1lem1.k |
. . . . . . 7
⊢ 𝐾 = ((2...(𝑁 + 1)) ∖ {𝑀}) |
16 | 14, 15 | eleq2s 2706 |
. . . . . 6
⊢ (𝑥 ∈ 𝐾 → (𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀)) |
17 | | neanior 2874 |
. . . . . 6
⊢ ((𝑥 ≠ 1 ∧ 𝑥 ≠ 𝑀) ↔ ¬ (𝑥 = 1 ∨ 𝑥 = 𝑀)) |
18 | 16, 17 | sylib 207 |
. . . . 5
⊢ (𝑥 ∈ 𝐾 → ¬ (𝑥 = 1 ∨ 𝑥 = 𝑀)) |
19 | | vex 3176 |
. . . . . 6
⊢ 𝑥 ∈ V |
20 | 19 | elpr 4146 |
. . . . 5
⊢ (𝑥 ∈ {1, 𝑀} ↔ (𝑥 = 1 ∨ 𝑥 = 𝑀)) |
21 | 18, 20 | sylnibr 318 |
. . . 4
⊢ (𝑥 ∈ 𝐾 → ¬ 𝑥 ∈ {1, 𝑀}) |
22 | 1, 21 | mprgbir 2911 |
. . 3
⊢ (𝐾 ∩ {1, 𝑀}) = ∅ |
23 | 22 | a1i 11 |
. 2
⊢ (𝜑 → (𝐾 ∩ {1, 𝑀}) = ∅) |
24 | | uncom 3719 |
. . . 4
⊢ ({1}
∪ (𝐾 ∪ {𝑀})) = ((𝐾 ∪ {𝑀}) ∪ {1}) |
25 | | 1z 11284 |
. . . . . 6
⊢ 1 ∈
ℤ |
26 | | fzsn 12254 |
. . . . . 6
⊢ (1 ∈
ℤ → (1...1) = {1}) |
27 | 25, 26 | ax-mp 5 |
. . . . 5
⊢ (1...1) =
{1} |
28 | 15 | uneq1i 3725 |
. . . . . 6
⊢ (𝐾 ∪ {𝑀}) = (((2...(𝑁 + 1)) ∖ {𝑀}) ∪ {𝑀}) |
29 | | undif1 3995 |
. . . . . 6
⊢
(((2...(𝑁 + 1))
∖ {𝑀}) ∪ {𝑀}) = ((2...(𝑁 + 1)) ∪ {𝑀}) |
30 | 28, 29 | eqtr2i 2633 |
. . . . 5
⊢
((2...(𝑁 + 1)) ∪
{𝑀}) = (𝐾 ∪ {𝑀}) |
31 | 27, 30 | uneq12i 3727 |
. . . 4
⊢ ((1...1)
∪ ((2...(𝑁 + 1)) ∪
{𝑀})) = ({1} ∪ (𝐾 ∪ {𝑀})) |
32 | | df-pr 4128 |
. . . . . . 7
⊢ {1, 𝑀} = ({1} ∪ {𝑀}) |
33 | 32 | equncomi 3721 |
. . . . . 6
⊢ {1, 𝑀} = ({𝑀} ∪ {1}) |
34 | 33 | uneq2i 3726 |
. . . . 5
⊢ (𝐾 ∪ {1, 𝑀}) = (𝐾 ∪ ({𝑀} ∪ {1})) |
35 | | unass 3732 |
. . . . 5
⊢ ((𝐾 ∪ {𝑀}) ∪ {1}) = (𝐾 ∪ ({𝑀} ∪ {1})) |
36 | 34, 35 | eqtr4i 2635 |
. . . 4
⊢ (𝐾 ∪ {1, 𝑀}) = ((𝐾 ∪ {𝑀}) ∪ {1}) |
37 | 24, 31, 36 | 3eqtr4i 2642 |
. . 3
⊢ ((1...1)
∪ ((2...(𝑁 + 1)) ∪
{𝑀})) = (𝐾 ∪ {1, 𝑀}) |
38 | | subfacp1lem1.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ (2...(𝑁 + 1))) |
39 | 38 | snssd 4281 |
. . . . . . 7
⊢ (𝜑 → {𝑀} ⊆ (2...(𝑁 + 1))) |
40 | | ssequn2 3748 |
. . . . . . 7
⊢ ({𝑀} ⊆ (2...(𝑁 + 1)) ↔ ((2...(𝑁 + 1)) ∪ {𝑀}) = (2...(𝑁 + 1))) |
41 | 39, 40 | sylib 207 |
. . . . . 6
⊢ (𝜑 → ((2...(𝑁 + 1)) ∪ {𝑀}) = (2...(𝑁 + 1))) |
42 | | df-2 10956 |
. . . . . . 7
⊢ 2 = (1 +
1) |
43 | 42 | oveq1i 6559 |
. . . . . 6
⊢
(2...(𝑁 + 1)) = ((1
+ 1)...(𝑁 +
1)) |
44 | 41, 43 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → ((2...(𝑁 + 1)) ∪ {𝑀}) = ((1 + 1)...(𝑁 + 1))) |
45 | 44 | uneq2d 3729 |
. . . 4
⊢ (𝜑 → ((1...1) ∪
((2...(𝑁 + 1)) ∪ {𝑀})) = ((1...1) ∪ ((1 +
1)...(𝑁 +
1)))) |
46 | | subfacp1lem1.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
47 | 46 | peano2nnd 10914 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈ ℕ) |
48 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
49 | 47, 48 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘1)) |
50 | | eluzfz1 12219 |
. . . . 5
⊢ ((𝑁 + 1) ∈
(ℤ≥‘1) → 1 ∈ (1...(𝑁 + 1))) |
51 | | fzsplit 12238 |
. . . . 5
⊢ (1 ∈
(1...(𝑁 + 1)) →
(1...(𝑁 + 1)) = ((1...1)
∪ ((1 + 1)...(𝑁 +
1)))) |
52 | 49, 50, 51 | 3syl 18 |
. . . 4
⊢ (𝜑 → (1...(𝑁 + 1)) = ((1...1) ∪ ((1 + 1)...(𝑁 + 1)))) |
53 | 45, 52 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → ((1...1) ∪
((2...(𝑁 + 1)) ∪ {𝑀})) = (1...(𝑁 + 1))) |
54 | 37, 53 | syl5eqr 2658 |
. 2
⊢ (𝜑 → (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1))) |
55 | 42 | oveq2i 6560 |
. . 3
⊢ ((𝑁 + 1) − 2) = ((𝑁 + 1) − (1 +
1)) |
56 | | fzfi 12633 |
. . . . . . . . 9
⊢
(2...(𝑁 + 1)) ∈
Fin |
57 | | diffi 8077 |
. . . . . . . . 9
⊢
((2...(𝑁 + 1))
∈ Fin → ((2...(𝑁
+ 1)) ∖ {𝑀}) ∈
Fin) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . 8
⊢
((2...(𝑁 + 1))
∖ {𝑀}) ∈
Fin |
59 | 15, 58 | eqeltri 2684 |
. . . . . . 7
⊢ 𝐾 ∈ Fin |
60 | | prfi 8120 |
. . . . . . 7
⊢ {1, 𝑀} ∈ Fin |
61 | | hashun 13032 |
. . . . . . 7
⊢ ((𝐾 ∈ Fin ∧ {1, 𝑀} ∈ Fin ∧ (𝐾 ∩ {1, 𝑀}) = ∅) → (#‘(𝐾 ∪ {1, 𝑀})) = ((#‘𝐾) + (#‘{1, 𝑀}))) |
62 | 59, 60, 22, 61 | mp3an 1416 |
. . . . . 6
⊢
(#‘(𝐾 ∪
{1, 𝑀})) = ((#‘𝐾) + (#‘{1, 𝑀})) |
63 | 54 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (#‘(𝐾 ∪ {1, 𝑀})) = (#‘(1...(𝑁 + 1)))) |
64 | | neeq1 2844 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑀 → (𝑥 ≠ 1 ↔ 𝑀 ≠ 1)) |
65 | 3, 11 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (2...(𝑁 + 1)) → 𝑥 ≠ 1) |
66 | 64, 65 | vtoclga 3245 |
. . . . . . . . . 10
⊢ (𝑀 ∈ (2...(𝑁 + 1)) → 𝑀 ≠ 1) |
67 | 38, 66 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ≠ 1) |
68 | 67 | necomd 2837 |
. . . . . . . 8
⊢ (𝜑 → 1 ≠ 𝑀) |
69 | | 1ex 9914 |
. . . . . . . . 9
⊢ 1 ∈
V |
70 | | subfacp1lem1.x |
. . . . . . . . 9
⊢ 𝑀 ∈ V |
71 | | hashprg 13043 |
. . . . . . . . 9
⊢ ((1
∈ V ∧ 𝑀 ∈ V)
→ (1 ≠ 𝑀 ↔
(#‘{1, 𝑀}) =
2)) |
72 | 69, 70, 71 | mp2an 704 |
. . . . . . . 8
⊢ (1 ≠
𝑀 ↔ (#‘{1, 𝑀}) = 2) |
73 | 68, 72 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → (#‘{1, 𝑀}) = 2) |
74 | 73 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → ((#‘𝐾) + (#‘{1, 𝑀})) = ((#‘𝐾) + 2)) |
75 | 62, 63, 74 | 3eqtr3a 2668 |
. . . . 5
⊢ (𝜑 → (#‘(1...(𝑁 + 1))) = ((#‘𝐾) + 2)) |
76 | 47 | nnnn0d 11228 |
. . . . . 6
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
77 | | hashfz1 12996 |
. . . . . 6
⊢ ((𝑁 + 1) ∈ ℕ0
→ (#‘(1...(𝑁 +
1))) = (𝑁 +
1)) |
78 | 76, 77 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘(1...(𝑁 + 1))) = (𝑁 + 1)) |
79 | 75, 78 | eqtr3d 2646 |
. . . 4
⊢ (𝜑 → ((#‘𝐾) + 2) = (𝑁 + 1)) |
80 | 47 | nncnd 10913 |
. . . . 5
⊢ (𝜑 → (𝑁 + 1) ∈ ℂ) |
81 | | 2cnd 10970 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℂ) |
82 | | hashcl 13009 |
. . . . . . . 8
⊢ (𝐾 ∈ Fin →
(#‘𝐾) ∈
ℕ0) |
83 | 59, 82 | ax-mp 5 |
. . . . . . 7
⊢
(#‘𝐾) ∈
ℕ0 |
84 | 83 | nn0cni 11181 |
. . . . . 6
⊢
(#‘𝐾) ∈
ℂ |
85 | 84 | a1i 11 |
. . . . 5
⊢ (𝜑 → (#‘𝐾) ∈ ℂ) |
86 | 80, 81, 85 | subadd2d 10290 |
. . . 4
⊢ (𝜑 → (((𝑁 + 1) − 2) = (#‘𝐾) ↔ ((#‘𝐾) + 2) = (𝑁 + 1))) |
87 | 79, 86 | mpbird 246 |
. . 3
⊢ (𝜑 → ((𝑁 + 1) − 2) = (#‘𝐾)) |
88 | 46 | nncnd 10913 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℂ) |
89 | | 1cnd 9935 |
. . . 4
⊢ (𝜑 → 1 ∈
ℂ) |
90 | 88, 89, 89 | pnpcan2d 10309 |
. . 3
⊢ (𝜑 → ((𝑁 + 1) − (1 + 1)) = (𝑁 − 1)) |
91 | 55, 87, 90 | 3eqtr3a 2668 |
. 2
⊢ (𝜑 → (#‘𝐾) = (𝑁 − 1)) |
92 | 23, 54, 91 | 3jca 1235 |
1
⊢ (𝜑 → ((𝐾 ∩ {1, 𝑀}) = ∅ ∧ (𝐾 ∪ {1, 𝑀}) = (1...(𝑁 + 1)) ∧ (#‘𝐾) = (𝑁 − 1))) |