Step | Hyp | Ref
| Expression |
1 | | metakunt25.1 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | | metakunt25.2 |
. . 3
⊢ (𝜑 → 𝐼 ∈ ℕ) |
3 | | metakunt25.3 |
. . 3
⊢ (𝜑 → 𝐼 ≤ 𝑀) |
4 | | eqid 2759 |
. . 3
⊢ (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) |
5 | 1, 2, 3, 4 | metakunt15 39646 |
. 2
⊢ (𝜑 → (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))):(1...(𝐼 − 1))–1-1-onto→(((𝑀 − 𝐼) + 1)...(𝑀 − 1))) |
6 | | eqid 2759 |
. . 3
⊢ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) |
7 | 1, 2, 3, 6 | metakunt16 39647 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))):(𝐼...(𝑀 − 1))–1-1-onto→(1...(𝑀 − 𝐼))) |
8 | | f1osng 6635 |
. . 3
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ) →
{〈𝑀, 𝑀〉}:{𝑀}–1-1-onto→{𝑀}) |
9 | 1, 1, 8 | syl2anc 588 |
. 2
⊢ (𝜑 → {〈𝑀, 𝑀〉}:{𝑀}–1-1-onto→{𝑀}) |
10 | 1, 2, 3 | metakunt18 39649 |
. . . 4
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) |
11 | 10 | simpld 499 |
. . 3
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) |
12 | 11 | simp1d 1140 |
. 2
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) |
13 | 11 | simp2d 1141 |
. 2
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) |
14 | 11 | simp3d 1142 |
. 2
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) |
15 | 10 | simprd 500 |
. . 3
⊢ (𝜑 → (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅)) |
16 | 15 | simp1d 1140 |
. 2
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅) |
17 | 15 | simp2d 1141 |
. 2
⊢ (𝜑 → ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅) |
18 | 15 | simp3d 1142 |
. 2
⊢ (𝜑 → ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅) |
19 | | eleq1 2838 |
. . . . . 6
⊢ (𝑀 = if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) → (𝑀 ∈ ℤ ↔ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) ∈ ℤ)) |
20 | | eleq1 2838 |
. . . . . 6
⊢ (if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) = if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) → (if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ ↔ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) ∈ ℤ)) |
21 | 1 | nnzd 12110 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
22 | 21 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑀 ∈ ℤ) |
23 | 22 | adantr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ 𝑥 = 𝑀) → 𝑀 ∈ ℤ) |
24 | | eleq1 2838 |
. . . . . . 7
⊢ ((𝑥 + (𝑀 − 𝐼)) = if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) → ((𝑥 + (𝑀 − 𝐼)) ∈ ℤ ↔ if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ)) |
25 | | eleq1 2838 |
. . . . . . 7
⊢ ((𝑥 + (1 − 𝐼)) = if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) → ((𝑥 + (1 − 𝐼)) ∈ ℤ ↔ if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ)) |
26 | | elfzelz 12941 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1...𝑀) → 𝑥 ∈ ℤ) |
27 | 26 | adantl 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝑥 ∈ ℤ) |
28 | 27 | adantr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → 𝑥 ∈ ℤ) |
29 | 28 | adantr 485 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → 𝑥 ∈ ℤ) |
30 | 22 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → 𝑀 ∈ ℤ) |
31 | 2 | nnzd 12110 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ ℤ) |
32 | 31 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → 𝐼 ∈ ℤ) |
33 | 32 | adantr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → 𝐼 ∈ ℤ) |
34 | 33 | adantr 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → 𝐼 ∈ ℤ) |
35 | 30, 34 | zsubcld 12116 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → (𝑀 − 𝐼) ∈ ℤ) |
36 | 29, 35 | zaddcld 12115 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ 𝑥 < 𝐼) → (𝑥 + (𝑀 − 𝐼)) ∈ ℤ) |
37 | 28 | adantr 485 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → 𝑥 ∈ ℤ) |
38 | | 1zzd 12037 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → 1 ∈ ℤ) |
39 | 33 | adantr 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → 𝐼 ∈ ℤ) |
40 | 38, 39 | zsubcld 12116 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → (1 − 𝐼) ∈ ℤ) |
41 | 37, 40 | zaddcld 12115 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) ∧ ¬ 𝑥 < 𝐼) → (𝑥 + (1 − 𝐼)) ∈ ℤ) |
42 | 24, 25, 36, 41 | ifbothda 4451 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑀)) ∧ ¬ 𝑥 = 𝑀) → if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) ∈ ℤ) |
43 | 19, 20, 23, 42 | ifbothda 4451 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑀)) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) ∈ ℤ) |
44 | | metakunt25.4 |
. . . . 5
⊢ 𝐵 = (𝑥 ∈ (1...𝑀) ↦ if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))))) |
45 | 43, 44 | fmptd 6862 |
. . . 4
⊢ (𝜑 → 𝐵:(1...𝑀)⟶ℤ) |
46 | 45 | ffnd 6492 |
. . 3
⊢ (𝜑 → 𝐵 Fn (1...𝑀)) |
47 | 1, 2, 3, 44, 4, 6 | metakunt19 39650 |
. . . . . 6
⊢ (𝜑 → (((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) Fn (1...(𝐼 − 1)) ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) Fn (𝐼...(𝑀 − 1)) ∧ ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) |
48 | 47 | simpld 499 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) Fn (1...(𝐼 − 1)) ∧ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) Fn (𝐼...(𝑀 − 1)) ∧ ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) |
49 | 48 | simp3d 1142 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) |
50 | 47 | simprd 500 |
. . . 4
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) |
51 | 1, 2, 3 | metakunt24 39655 |
. . . . 5
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅ ∧ (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀}) ∧ (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀}))) |
52 | 51 | simp1d 1140 |
. . . 4
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) |
53 | 49, 50, 52 | fnund 6439 |
. . 3
⊢ (𝜑 → (((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) ∪ {〈𝑀, 𝑀〉}) Fn (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) |
54 | 51 | simp2d 1141 |
. . 3
⊢ (𝜑 → (1...𝑀) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∪ {𝑀})) |
55 | 1 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝑀 ∈ ℕ) |
56 | 2 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝐼 ∈ ℕ) |
57 | 3 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝐼 ≤ 𝑀) |
58 | | simpr 489 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → 𝑦 ∈ (1...𝑀)) |
59 | 55, 56, 57, 44, 4, 6, 58 | metakunt23 39654 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝑀)) → (𝐵‘𝑦) = ((((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) ∪ {〈𝑀, 𝑀〉})‘𝑦)) |
60 | 46, 53, 54, 59 | eqfnfv2d2 39534 |
. 2
⊢ (𝜑 → 𝐵 = (((𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) ∪ (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) ∪ {〈𝑀, 𝑀〉})) |
61 | 51 | simp3d 1142 |
. 2
⊢ (𝜑 → (1...𝑀) = (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∪ (1...(𝑀 − 𝐼))) ∪ {𝑀})) |
62 | 5, 7, 9, 12, 13, 14, 16, 17, 18, 60, 54, 61 | metakunt17 39648 |
1
⊢ (𝜑 → 𝐵:(1...𝑀)–1-1-onto→(1...𝑀)) |