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 2740 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 = 𝑀 ↔ 𝑋 = 𝑀)) | 
| 4 |  | breq1 5145 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) | 
| 5 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) | 
| 6 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 + (1 − 𝐼)) = (𝑋 + (1 − 𝐼))) | 
| 7 | 4, 5, 6 | ifbieq12d 4553 | . . . . . 6
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) | 
| 8 | 3, 7 | ifbieq2d 4551 | . . . . 5
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) | 
| 9 | 8 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) | 
| 10 |  | metakunt22.8 | . . . . . . 7
⊢ (𝜑 → ¬ 𝑋 = 𝑀) | 
| 11 |  | iffalse 4533 | . . . . . . 7
⊢ (¬
𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) | 
| 12 | 10, 11 | syl 17 | . . . . . 6
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) | 
| 13 |  | metakunt22.9 | . . . . . . 7
⊢ (𝜑 → ¬ 𝑋 < 𝐼) | 
| 14 |  | iffalse 4533 | . . . . . . 7
⊢ (¬
𝑋 < 𝐼 → if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))) = (𝑋 + (1 − 𝐼))) | 
| 15 | 13, 14 | syl 17 | . . . . . 6
⊢ (𝜑 → if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))) = (𝑋 + (1 − 𝐼))) | 
| 16 | 12, 15 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (1 − 𝐼))) | 
| 17 | 16 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (1 − 𝐼))) | 
| 18 | 9, 17 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = (𝑋 + (1 − 𝐼))) | 
| 19 |  | metakunt22.7 | . . 3
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) | 
| 20 | 19 | elfzelzd 13566 | . . . 4
⊢ (𝜑 → 𝑋 ∈ ℤ) | 
| 21 |  | 1zzd 12650 | . . . . 5
⊢ (𝜑 → 1 ∈
ℤ) | 
| 22 |  | metakunt22.2 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) | 
| 23 | 22 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 24 | 21, 23 | zsubcld 12729 | . . . 4
⊢ (𝜑 → (1 − 𝐼) ∈
ℤ) | 
| 25 | 20, 24 | zaddcld 12728 | . . 3
⊢ (𝜑 → (𝑋 + (1 − 𝐼)) ∈ ℤ) | 
| 26 | 2, 18, 19, 25 | fvmptd 7022 | . 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 42225 | . . . . . . 7
⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) | 
| 32 | 31 | simpld 494 | . . . . . 6
⊢ (𝜑 → (𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) | 
| 33 | 32 | simp3d 1144 | . . . . 5
⊢ (𝜑 → (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 34 | 31 | simprd 495 | . . . . 5
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) | 
| 35 |  | indir 4285 | . . . . . . 7
⊢
(((1...(𝐼 −
1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) | 
| 36 | 35 | a1i 11 | . . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀}))) | 
| 37 | 27, 22, 28 | metakunt18 42224 | . . . . . . . . . 10
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | 
| 38 | 37 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) | 
| 39 | 38 | simp2d 1143 | . . . . . . . 8
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) | 
| 40 | 38 | simp3d 1144 | . . . . . . . 8
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) | 
| 41 | 39, 40 | uneq12d 4168 | . . . . . . 7
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = (∅ ∪
∅)) | 
| 42 |  | unidm 4156 | . . . . . . . 8
⊢ (∅
∪ ∅) = ∅ | 
| 43 | 42 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (∅ ∪ ∅) =
∅) | 
| 44 | 41, 43 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = ∅) | 
| 45 | 36, 44 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) | 
| 46 | 27 | nnzd 12642 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 47 | 46, 21 | zsubcld 12729 | . . . . . . 7
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) | 
| 48 | 22 | nnred 12282 | . . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ ℝ) | 
| 49 |  | elfznn 13594 | . . . . . . . . . . 11
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) | 
| 50 | 19, 49 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℕ) | 
| 51 | 50 | nnred 12282 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 52 | 48, 51 | lenltd 11408 | . . . . . . . 8
⊢ (𝜑 → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) | 
| 53 | 13, 52 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → 𝐼 ≤ 𝑋) | 
| 54 |  | elfzle2 13569 | . . . . . . . . . . 11
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ≤ 𝑀) | 
| 55 | 19, 54 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ≤ 𝑀) | 
| 56 |  | df-ne 2940 | . . . . . . . . . . . 12
⊢ (𝑋 ≠ 𝑀 ↔ ¬ 𝑋 = 𝑀) | 
| 57 | 10, 56 | sylibr 234 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≠ 𝑀) | 
| 58 | 57 | necomd 2995 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ≠ 𝑋) | 
| 59 | 55, 58 | jca 511 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋)) | 
| 60 | 27 | nnred 12282 | . . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 61 | 51, 60 | ltlend 11407 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 < 𝑀 ↔ (𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋))) | 
| 62 | 59, 61 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 𝑋 < 𝑀) | 
| 63 |  | zltlem1 12672 | . . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑋 < 𝑀 ↔ 𝑋 ≤ (𝑀 − 1))) | 
| 64 | 20, 46, 63 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑋 < 𝑀 ↔ 𝑋 ≤ (𝑀 − 1))) | 
| 65 | 62, 64 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → 𝑋 ≤ (𝑀 − 1)) | 
| 66 | 23, 47, 20, 53, 65 | elfzd 13556 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐼...(𝑀 − 1))) | 
| 67 |  | elun2 4182 | . . . . . 6
⊢ (𝑋 ∈ (𝐼...(𝑀 − 1)) → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 68 | 66, 67 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 69 | 33, 34, 45, 68 | fvun1d 7001 | . . . 4
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = ((𝐶 ∪ 𝐷)‘𝑋)) | 
| 70 | 32 | simp1d 1142 | . . . . . 6
⊢ (𝜑 → 𝐶 Fn (1...(𝐼 − 1))) | 
| 71 | 32 | simp2d 1143 | . . . . . 6
⊢ (𝜑 → 𝐷 Fn (𝐼...(𝑀 − 1))) | 
| 72 | 38 | simp1d 1142 | . . . . . 6
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) | 
| 73 | 70, 71, 72, 66 | fvun2d 7002 | . . . . 5
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝐷‘𝑋)) | 
| 74 | 30 | a1i 11 | . . . . . 6
⊢ (𝜑 → 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼)))) | 
| 75 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑥 = 𝑋) | 
| 76 | 75 | oveq1d 7447 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (1 − 𝐼)) = (𝑋 + (1 − 𝐼))) | 
| 77 | 20 | zred 12724 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 78 |  | lenlt 11340 | . . . . . . . . 9
⊢ ((𝐼 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) | 
| 79 | 48, 77, 78 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝐼 ≤ 𝑋 ↔ ¬ 𝑋 < 𝐼)) | 
| 80 | 13, 79 | mpbird 257 | . . . . . . 7
⊢ (𝜑 → 𝐼 ≤ 𝑋) | 
| 81 | 77, 60 | ltlend 11407 | . . . . . . . . 9
⊢ (𝜑 → (𝑋 < 𝑀 ↔ (𝑋 ≤ 𝑀 ∧ 𝑀 ≠ 𝑋))) | 
| 82 | 59, 81 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 𝑋 < 𝑀) | 
| 83 | 82, 64 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → 𝑋 ≤ (𝑀 − 1)) | 
| 84 | 23, 47, 20, 80, 83 | elfzd 13556 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝐼...(𝑀 − 1))) | 
| 85 | 74, 76, 84, 25 | fvmptd 7022 | . . . . 5
⊢ (𝜑 → (𝐷‘𝑋) = (𝑋 + (1 − 𝐼))) | 
| 86 | 73, 85 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝑋 + (1 − 𝐼))) | 
| 87 | 69, 86 | eqtrd 2776 | . . 3
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = (𝑋 + (1 − 𝐼))) | 
| 88 | 87 | eqcomd 2742 | . 2
⊢ (𝜑 → (𝑋 + (1 − 𝐼)) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) | 
| 89 | 26, 88 | eqtrd 2776 | 1
⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |