Proof of Theorem metakunt21
Step | Hyp | Ref
| Expression |
1 | | metakunt21.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 | | metakunt21.8 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑋 = 𝑀) |
11 | 10 | iffalsed 4424 |
. . . . . 6
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) |
12 | | metakunt21.9 |
. . . . . . 7
⊢ (𝜑 → 𝑋 < 𝐼) |
13 | 12 | iftrued 4421 |
. . . . . 6
⊢ (𝜑 → if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))) = (𝑋 + (𝑀 − 𝐼))) |
14 | 11, 13 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (𝑀 − 𝐼))) |
15 | 14 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (𝑀 − 𝐼))) |
16 | 9, 15 | eqtrd 2794 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = (𝑋 + (𝑀 − 𝐼))) |
17 | | metakunt21.7 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
18 | 17 | elfzelzd 12942 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℤ) |
19 | | metakunt21.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
20 | 19 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
21 | | metakunt21.2 |
. . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) |
22 | 21 | nnzd 12110 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) |
23 | 20, 22 | zsubcld 12116 |
. . . 4
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ) |
24 | 18, 23 | zaddcld 12115 |
. . 3
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) |
25 | 2, 16, 17, 24 | fvmptd 6759 |
. 2
⊢ (𝜑 → (𝐵‘𝑋) = (𝑋 + (𝑀 − 𝐼))) |
26 | | metakunt21.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
27 | | metakunt21.5 |
. . . . . . . 8
⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) |
28 | | metakunt21.6 |
. . . . . . . 8
⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) |
29 | 19, 21, 26, 1, 27, 28 | metakunt19 39650 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) |
30 | 29 | simpld 499 |
. . . . . 6
⊢ (𝜑 → (𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) |
31 | 30 | simp3d 1142 |
. . . . 5
⊢ (𝜑 → (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
32 | 29 | simprd 500 |
. . . . 5
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) |
33 | | indir 4176 |
. . . . . . 7
⊢
(((1...(𝐼 −
1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) |
34 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀}))) |
35 | 19, 21, 26 | metakunt18 39649 |
. . . . . . . . . 10
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) |
36 | 35 | simpld 499 |
. . . . . . . . 9
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) |
37 | 36 | simp2d 1141 |
. . . . . . . 8
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) |
38 | 36 | simp3d 1142 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) |
39 | 37, 38 | uneq12d 4065 |
. . . . . . 7
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = (∅ ∪
∅)) |
40 | | unidm 4053 |
. . . . . . . 8
⊢ (∅
∪ ∅) = ∅ |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (∅ ∪ ∅) =
∅) |
42 | 39, 41 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = ∅) |
43 | 34, 42 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) |
44 | | 1zzd 12037 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
45 | 22, 44 | zsubcld 12116 |
. . . . . . 7
⊢ (𝜑 → (𝐼 − 1) ∈ ℤ) |
46 | | elfznn 12970 |
. . . . . . . . 9
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) |
47 | 17, 46 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℕ) |
48 | 47 | nnge1d 11707 |
. . . . . . 7
⊢ (𝜑 → 1 ≤ 𝑋) |
49 | | zltlem1 12059 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑋 < 𝐼 ↔ 𝑋 ≤ (𝐼 − 1))) |
50 | 18, 22, 49 | syl2anc 588 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 < 𝐼 ↔ 𝑋 ≤ (𝐼 − 1))) |
51 | 12, 50 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ≤ (𝐼 − 1)) |
52 | 44, 45, 18, 48, 51 | elfzd 12932 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (1...(𝐼 − 1))) |
53 | | elun1 4077 |
. . . . . 6
⊢ (𝑋 ∈ (1...(𝐼 − 1)) → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
54 | 52, 53 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
55 | 31, 32, 43, 54 | fvun1d 6738 |
. . . 4
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = ((𝐶 ∪ 𝐷)‘𝑋)) |
56 | 30 | simp1d 1140 |
. . . . . 6
⊢ (𝜑 → 𝐶 Fn (1...(𝐼 − 1))) |
57 | 30 | simp2d 1141 |
. . . . . 6
⊢ (𝜑 → 𝐷 Fn (𝐼...(𝑀 − 1))) |
58 | 36 | simp1d 1140 |
. . . . . 6
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) |
59 | 56, 57, 58, 52 | fvun1d 6738 |
. . . . 5
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝐶‘𝑋)) |
60 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))) |
61 | 5 | adantl 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) |
62 | 60, 61, 52, 24 | fvmptd 6759 |
. . . . 5
⊢ (𝜑 → (𝐶‘𝑋) = (𝑋 + (𝑀 − 𝐼))) |
63 | 59, 62 | eqtrd 2794 |
. . . 4
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝑋 + (𝑀 − 𝐼))) |
64 | 55, 63 | eqtrd 2794 |
. . 3
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = (𝑋 + (𝑀 − 𝐼))) |
65 | 64 | eqcomd 2765 |
. 2
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |
66 | 25, 65 | eqtrd 2794 |
1
⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |