Proof of Theorem metakunt32
Step | Hyp | Ref
| Expression |
1 | | metakunt32.5 |
. . 3
⊢ 𝐷 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑥, if(𝑥 < 𝐼, ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)), ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0))))) |
2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝐼, 𝑥, if(𝑥 < 𝐼, ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)), ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0)))))) |
3 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) |
4 | 3 | eqeq1d 2739 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 = 𝐼 ↔ 𝑋 = 𝐼)) |
5 | 3 | breq1d 5063 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) |
6 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) |
7 | 6 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) |
8 | 7 | breq2d 5065 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝐼 ≤ (𝑥 + (𝑀 − 𝐼)) ↔ 𝐼 ≤ (𝑋 + (𝑀 − 𝐼)))) |
9 | 8 | ifbid 4462 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0) = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) |
10 | 7, 9 | oveq12d 7231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)) = ((𝑋 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0))) |
11 | | metakunt32.6 |
. . . . . . . . 9
⊢ 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) |
13 | 12 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) = 𝐺) |
14 | 13 | oveq2d 7229 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑋 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐺)) |
15 | 10, 14 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)) = ((𝑋 + (𝑀 − 𝐼)) + 𝐺)) |
16 | 3 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 − 𝐼) = (𝑋 − 𝐼)) |
17 | 16 | breq2d 5065 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝐼 ≤ (𝑥 − 𝐼) ↔ 𝐼 ≤ (𝑋 − 𝐼))) |
18 | 17 | ifbid 4462 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝐼 ≤ (𝑥 − 𝐼), 1, 0) = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) |
19 | 16, 18 | oveq12d 7231 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0)) = ((𝑋 − 𝐼) + if(𝐼 ≤ (𝑋 − 𝐼), 1, 0))) |
20 | | metakunt32.7 |
. . . . . . . . 9
⊢ 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) |
22 | 21 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) = 𝐻) |
23 | 22 | oveq2d 7229 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑋 − 𝐼) + if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) = ((𝑋 − 𝐼) + 𝐻)) |
24 | 19, 23 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0)) = ((𝑋 − 𝐼) + 𝐻)) |
25 | 5, 15, 24 | ifbieq12d 4467 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 < 𝐼, ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)), ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0))) = if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) |
26 | 4, 3, 25 | ifbieq12d 4467 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑥, if(𝑥 < 𝐼, ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)), ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0)))) = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻)))) |
27 | | metakunt32.8 |
. . . . 5
⊢ 𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) |
28 | 27 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻)))) |
29 | 28 | eqcomd 2743 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) = 𝑅) |
30 | 26, 29 | eqtrd 2777 |
. 2
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝐼, 𝑥, if(𝑥 < 𝐼, ((𝑥 + (𝑀 − 𝐼)) + if(𝐼 ≤ (𝑥 + (𝑀 − 𝐼)), 1, 0)), ((𝑥 − 𝐼) + if(𝐼 ≤ (𝑥 − 𝐼), 1, 0)))) = 𝑅) |
31 | | metakunt32.4 |
. 2
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) |
32 | 31 | elfzelzd 13113 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℤ) |
33 | | metakunt32.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℕ) |
34 | 33 | nnzd 12281 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
35 | | metakunt32.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℕ) |
36 | 35 | nnzd 12281 |
. . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ ℤ) |
37 | 34, 36 | zsubcld 12287 |
. . . . . . 7
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ) |
38 | 32, 37 | zaddcld 12286 |
. . . . . 6
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) |
39 | | 1zzd 12208 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
40 | | 0zd 12188 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) |
41 | 39, 40 | ifcld 4485 |
. . . . . . 7
⊢ (𝜑 → if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ) |
42 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 = if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0)) |
43 | 42 | eleq1d 2822 |
. . . . . . 7
⊢ (𝜑 → (𝐺 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 + (𝑀 − 𝐼)), 1, 0) ∈ ℤ)) |
44 | 41, 43 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ ℤ) |
45 | 38, 44 | zaddcld 12286 |
. . . . 5
⊢ (𝜑 → ((𝑋 + (𝑀 − 𝐼)) + 𝐺) ∈ ℤ) |
46 | 32, 36 | zsubcld 12287 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 𝐼) ∈ ℤ) |
47 | 39, 40 | ifcld 4485 |
. . . . . . 7
⊢ (𝜑 → if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) ∈ ℤ) |
48 | 20 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = if(𝐼 ≤ (𝑋 − 𝐼), 1, 0)) |
49 | 48 | eleq1d 2822 |
. . . . . . 7
⊢ (𝜑 → (𝐻 ∈ ℤ ↔ if(𝐼 ≤ (𝑋 − 𝐼), 1, 0) ∈ ℤ)) |
50 | 47, 49 | mpbird 260 |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ ℤ) |
51 | 46, 50 | zaddcld 12286 |
. . . . 5
⊢ (𝜑 → ((𝑋 − 𝐼) + 𝐻) ∈ ℤ) |
52 | 45, 51 | ifcld 4485 |
. . . 4
⊢ (𝜑 → if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻)) ∈ ℤ) |
53 | 32, 52 | ifcld 4485 |
. . 3
⊢ (𝜑 → if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) ∈ ℤ) |
54 | 27 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝑅 = if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻)))) |
55 | 54 | eleq1d 2822 |
. . 3
⊢ (𝜑 → (𝑅 ∈ ℤ ↔ if(𝑋 = 𝐼, 𝑋, if(𝑋 < 𝐼, ((𝑋 + (𝑀 − 𝐼)) + 𝐺), ((𝑋 − 𝐼) + 𝐻))) ∈ ℤ)) |
56 | 53, 55 | mpbird 260 |
. 2
⊢ (𝜑 → 𝑅 ∈ ℤ) |
57 | 2, 30, 31, 56 | fvmptd 6825 |
1
⊢ (𝜑 → (𝐷‘𝑋) = 𝑅) |