Proof of Theorem metakunt20
Step | Hyp | Ref
| Expression |
1 | | metakunt20.4 |
. . . . 5
⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))))) |
3 | | eqeq1 2763 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 = 𝑀 ↔ 𝑋 = 𝑀)) |
4 | | breq1 5028 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
5 | | oveq1 7150 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) |
6 | | oveq1 7150 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 + (1 − 𝐼)) = (𝑋 + (1 − 𝐼))) |
7 | 4, 5, 6 | ifbieq12d 4441 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) |
8 | 3, 7 | ifbieq2d 4439 |
. . . . . 6
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) |
9 | 8 | adantl 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) |
10 | | metakunt20.8 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 = 𝑀) |
11 | | iftrue 4419 |
. . . . . . . 8
⊢ (𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑀) |
12 | 10, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑀) |
13 | 12 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑀) |
14 | 10 | eqcomd 2765 |
. . . . . . 7
⊢ (𝜑 → 𝑀 = 𝑋) |
15 | 14 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑀 = 𝑋) |
16 | 13, 15 | eqtrd 2794 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑋) |
17 | 9, 16 | eqtrd 2794 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = 𝑋) |
18 | | metakunt20.7 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
19 | 2, 17, 18, 18 | fvmptd 6759 |
. . 3
⊢ (𝜑 → (𝐵‘𝑋) = 𝑋) |
20 | 10 | fveq2d 6655 |
. . . . 5
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑋) = ({〈𝑀, 𝑀〉}‘𝑀)) |
21 | | metakunt20.1 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) |
22 | | fvsng 6926 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ) →
({〈𝑀, 𝑀〉}‘𝑀) = 𝑀) |
23 | 21, 21, 22 | syl2anc 588 |
. . . . 5
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑀) = 𝑀) |
24 | 20, 23 | eqtrd 2794 |
. . . 4
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑋) = 𝑀) |
25 | 24 | eqcomd 2765 |
. . 3
⊢ (𝜑 → 𝑀 = ({〈𝑀, 𝑀〉}‘𝑋)) |
26 | 19, 10, 25 | 3eqtrd 2798 |
. 2
⊢ (𝜑 → (𝐵‘𝑋) = ({〈𝑀, 𝑀〉}‘𝑋)) |
27 | | metakunt20.2 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ∈ ℕ) |
28 | | metakunt20.3 |
. . . . . . 7
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
29 | | metakunt20.5 |
. . . . . . 7
⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) |
30 | | metakunt20.6 |
. . . . . . 7
⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) |
31 | 21, 27, 28, 1, 29, 30 | metakunt19 39650 |
. . . . . 6
⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) |
32 | 31 | simpld 499 |
. . . . 5
⊢ (𝜑 → (𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) |
33 | 32 | simp3d 1142 |
. . . 4
⊢ (𝜑 → (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
34 | 31 | simprd 500 |
. . . 4
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) |
35 | 21 | nnzd 12110 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
36 | | fzsn 12983 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
37 | 35, 36 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) |
38 | 37 | ineq2d 4113 |
. . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀})) |
39 | 38 | eqcomd 2765 |
. . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀))) |
40 | 27 | nncnd 11675 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ ℂ) |
41 | 21 | nncnd 11675 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℂ) |
42 | 40, 41 | pncan3d 11023 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 + (𝑀 − 𝐼)) = 𝑀) |
43 | 42 | oveq2d 7159 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1..^(𝐼 + (𝑀 − 𝐼))) = (1..^𝑀)) |
44 | | fzoval 13073 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ →
(1..^𝑀) = (1...(𝑀 − 1))) |
45 | 35, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1..^𝑀) = (1...(𝑀 − 1))) |
46 | 43, 45 | eqtrd 2794 |
. . . . . . . . . . 11
⊢ (𝜑 → (1..^(𝐼 + (𝑀 − 𝐼))) = (1...(𝑀 − 1))) |
47 | 46 | eqcomd 2765 |
. . . . . . . . . 10
⊢ (𝜑 → (1...(𝑀 − 1)) = (1..^(𝐼 + (𝑀 − 𝐼)))) |
48 | | nnuz 12306 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
49 | 27, 48 | eleqtrdi 2861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈
(ℤ≥‘1)) |
50 | 27 | nnzd 12110 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ ℤ) |
51 | 50, 35 | jca 516 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ)) |
52 | | znn0sub 12053 |
. . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 ≤ 𝑀 ↔ (𝑀 − 𝐼) ∈
ℕ0)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 ≤ 𝑀 ↔ (𝑀 − 𝐼) ∈
ℕ0)) |
54 | 28, 53 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 𝐼) ∈
ℕ0) |
55 | | fzoun 13108 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ (𝑀 − 𝐼) ∈ ℕ0) →
(1..^(𝐼 + (𝑀 − 𝐼))) = ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼))))) |
56 | 49, 54, 55 | syl2anc 588 |
. . . . . . . . . 10
⊢ (𝜑 → (1..^(𝐼 + (𝑀 − 𝐼))) = ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼))))) |
57 | 47, 56 | eqtrd 2794 |
. . . . . . . . 9
⊢ (𝜑 → (1...(𝑀 − 1)) = ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼))))) |
58 | | fzoval 13073 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ ℤ →
(1..^𝐼) = (1...(𝐼 − 1))) |
59 | 50, 58 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1..^𝐼) = (1...(𝐼 − 1))) |
60 | 42 | oveq2d 7159 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐼..^(𝐼 + (𝑀 − 𝐼))) = (𝐼..^𝑀)) |
61 | | fzoval 13073 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝐼..^𝑀) = (𝐼...(𝑀 − 1))) |
62 | 35, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐼..^𝑀) = (𝐼...(𝑀 − 1))) |
63 | 60, 62 | eqtrd 2794 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐼..^(𝐼 + (𝑀 − 𝐼))) = (𝐼...(𝑀 − 1))) |
64 | 59, 63 | uneq12d 4065 |
. . . . . . . . 9
⊢ (𝜑 → ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼)))) = ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
65 | 57, 64 | eqtrd 2794 |
. . . . . . . 8
⊢ (𝜑 → (1...(𝑀 − 1)) = ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
66 | 65 | ineq1d 4112 |
. . . . . . 7
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀))) |
67 | 66 | eqcomd 2765 |
. . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∩ (𝑀...𝑀))) |
68 | 21 | nnred 11674 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) |
69 | 68 | ltm1d 11595 |
. . . . . . 7
⊢ (𝜑 → (𝑀 − 1) < 𝑀) |
70 | | fzdisj 12968 |
. . . . . . 7
⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) |
71 | 69, 70 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) |
72 | 67, 71 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀)) = ∅) |
73 | 39, 72 | eqtrd 2794 |
. . . 4
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) |
74 | | elsng 4529 |
. . . . . 6
⊢ (𝑋 ∈ (1...𝑀) → (𝑋 ∈ {𝑀} ↔ 𝑋 = 𝑀)) |
75 | 18, 74 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑋 ∈ {𝑀} ↔ 𝑋 = 𝑀)) |
76 | 10, 75 | mpbird 260 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ {𝑀}) |
77 | 33, 34, 73, 76 | fvun2d 6739 |
. . 3
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = ({〈𝑀, 𝑀〉}‘𝑋)) |
78 | 77 | eqcomd 2765 |
. 2
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |
79 | 26, 78 | eqtrd 2794 |
1
⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |