Proof of Theorem metakunt22
Step | Hyp | Ref
| Expression |
1 | | metakunt22.4 |
. . . 4
⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))) |
3 | | eqeq1 2763 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 = 𝑀 ↔ 𝑋 = 𝑀)) |
4 | | breq1 5028 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
5 | | oveq1 7150 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) |
6 | | oveq1 7150 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 + (1 − 𝐼)) = (𝑋 + (1 − 𝐼))) |
7 | 4, 5, 6 | ifbieq12d 4441 |
. . . . . 6
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) |
8 | 3, 7 | ifbieq2d 4439 |
. . . . 5
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) |
9 | 8 | adantl 486 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) |
10 | | metakunt22.8 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑋 = 𝑀) |
11 | | iffalse 4422 |
. . . . . . 7
⊢ (¬
𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) |
13 | | metakunt22.9 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑋 < 𝐼) |
14 | | iffalse 4422 |
. . . . . . 7
⊢ (¬
𝑋 < 𝐼 → if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))) = (𝑋 + (1 − 𝐼))) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))) = (𝑋 + (1 − 𝐼))) |
16 | 12, 15 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (1 − 𝐼))) |
17 | 16 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (1 − 𝐼))) |
18 | 9, 17 | eqtrd 2794 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = (𝑋 + (1 − 𝐼))) |
19 | | metakunt22.7 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
20 | 19 | elfzelzd 12942 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℤ) |
21 | | 1zzd 12037 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℤ) |
22 | | metakunt22.2 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) |
23 | 22 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) |
24 | 21, 23 | zsubcld 12116 |
. . . 4
⊢ (𝜑 → (1 − 𝐼) ∈
ℤ) |
25 | 20, 24 | zaddcld 12115 |
. . 3
⊢ (𝜑 → (𝑋 + (1 − 𝐼)) ∈ ℤ) |
26 | 2, 18, 19, 25 | fvmptd 6759 |
. 2
⊢ (𝜑 → (𝐵‘𝑋) = (𝑋 + (1 − 𝐼))) |
27 | | metakunt22.1 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
28 | | metakunt22.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
29 | | metakunt22.5 |
. . . . . . . 8
⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) |
30 | | metakunt22.6 |
. . . . . . . 8
⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) |
31 | 27, 22, 28, 1, 29, 30 | metakunt19 39650 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) |
32 | 31 | simpld 499 |
. . . . . 6
⊢ (𝜑 → (𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) |
33 | 32 | simp3d 1142 |
. . . . 5
⊢ (𝜑 → (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
34 | 31 | simprd 500 |
. . . . 5
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) |
35 | | indir 4176 |
. . . . . . 7
⊢
(((1...(𝐼 −
1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) |
36 | 35 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀}))) |
37 | 27, 22, 28 | metakunt18 39649 |
. . . . . . . . . 10
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) |
38 | 37 | simpld 499 |
. . . . . . . . 9
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) |
39 | 38 | simp2d 1141 |
. . . . . . . 8
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) |
40 | 38 | simp3d 1142 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) |
41 | 39, 40 | uneq12d 4065 |
. . . . . . 7
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = (∅ ∪
∅)) |
42 | | unidm 4053 |
. . . . . . . 8
⊢ (∅
∪ ∅) = ∅ |
43 | 42 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (∅ ∪ ∅) =
∅) |
44 | 41, 43 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = ∅) |
45 | 36, 44 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) |
46 | 27 | nnzd 12110 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
47 | 46, 21 | zsubcld 12116 |
. . . . . . 7
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
48 | | elfznn 12970 |
. . . . . . . . 9
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
49 | 19, 48 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℕ) |
50 | 49 | nnzd 12110 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ ℤ) |
51 | 22 | nnred 11674 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℝ) |
52 | 49 | nnred 11674 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
53 | 51, 52 | lenltd 10809 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) |
54 | 13, 53 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ≤ 𝑋) |
55 | | elfzle2 12945 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ≤ 𝑀) |
56 | 19, 55 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≤ 𝑀) |
57 | | df-ne 2950 |
. . . . . . . . . . . 12
⊢ (𝑋 ≠ 𝑀 ↔ ¬ 𝑋 = 𝑀) |
58 | 10, 57 | sylibr 237 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≠ 𝑀) |
59 | 58 | necomd 3004 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 𝑋) |
60 | 56, 59 | jca 516 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋)) |
61 | 27 | nnred 11674 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
62 | 52, 61 | ltlend 10808 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 < 𝑀 ↔ (𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋))) |
63 | 60, 62 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 < 𝑀) |
64 | | zltlem1 12059 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑋 < 𝑀 ↔ 𝑋 ≤ (𝑀 − 1))) |
65 | 50, 46, 64 | syl2anc 588 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 < 𝑀 ↔ 𝑋 ≤ (𝑀 − 1))) |
66 | 63, 65 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ (𝑀 − 1)) |
67 | 23, 47, 50, 54, 66 | elfzd 12932 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐼...(𝑀 − 1))) |
68 | | elun2 4078 |
. . . . . 6
⊢ (𝑋 ∈ (𝐼...(𝑀 − 1)) → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
69 | 67, 68 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
70 | 33, 34, 45, 69 | fvun1d 6738 |
. . . 4
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = ((𝐶 ∪ 𝐷)‘𝑋)) |
71 | 32 | simp1d 1140 |
. . . . . 6
⊢ (𝜑 → 𝐶 Fn (1...(𝐼 − 1))) |
72 | 32 | simp2d 1141 |
. . . . . 6
⊢ (𝜑 → 𝐷 Fn (𝐼...(𝑀 − 1))) |
73 | 38 | simp1d 1140 |
. . . . . 6
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) |
74 | 71, 72, 73, 67 | fvun2d 6739 |
. . . . 5
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝐷‘𝑋)) |
75 | 30 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) |
76 | | simpr 489 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
77 | 76 | oveq1d 7158 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (1 − 𝐼)) = (𝑋 + (1 − 𝐼))) |
78 | 20 | zred 12111 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) |
79 | | lenlt 10742 |
. . . . . . . . 9
⊢ ((𝐼 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) |
80 | 51, 78, 79 | syl2anc 588 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) |
81 | 13, 80 | mpbird 260 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ≤ 𝑋) |
82 | 78, 61 | ltlend 10808 |
. . . . . . . . 9
⊢ (𝜑 → (𝑋 < 𝑀 ↔ (𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋))) |
83 | 60, 82 | mpbird 260 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 < 𝑀) |
84 | 20, 46, 64 | syl2anc 588 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 < 𝑀 ↔ 𝑋 ≤ (𝑀 − 1))) |
85 | 83, 84 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ (𝑀 − 1)) |
86 | 23, 47, 20, 81, 85 | elfzd 12932 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐼...(𝑀 − 1))) |
87 | 75, 77, 86, 25 | fvmptd 6759 |
. . . . 5
⊢ (𝜑 → (𝐷‘𝑋) = (𝑋 + (1 − 𝐼))) |
88 | 74, 87 | eqtrd 2794 |
. . . 4
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝑋 + (1 − 𝐼))) |
89 | 70, 88 | eqtrd 2794 |
. . 3
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = (𝑋 + (1 − 𝐼))) |
90 | 89 | eqcomd 2765 |
. 2
⊢ (𝜑 → (𝑋 + (1 − 𝐼)) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |
91 | 26, 90 | eqtrd 2794 |
1
⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |