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 2740 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 = 𝑀 ↔ 𝑋 = 𝑀)) | 
| 4 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 < 𝐼 ↔ 𝑋 < 𝐼)) | 
| 5 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) | 
| 6 |  | oveq1 7439 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (𝑥 + (1 − 𝐼)) = (𝑋 + (1 − 𝐼))) | 
| 7 | 4, 5, 6 | ifbieq12d 4553 | . . . . . . 7
⊢ (𝑥 = 𝑋 → if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) | 
| 8 | 3, 7 | ifbieq2d 4551 | . . . . . 6
⊢ (𝑥 = 𝑋 → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) | 
| 9 | 8 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))))) | 
| 10 |  | metakunt20.8 | . . . . . . . 8
⊢ (𝜑 → 𝑋 = 𝑀) | 
| 11 |  | iftrue 4530 | . . . . . . . 8
⊢ (𝑋 = 𝑀 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑀) | 
| 12 | 10, 11 | syl 17 | . . . . . . 7
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑀) | 
| 13 | 12 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑀) | 
| 14 | 10 | eqcomd 2742 | . . . . . . 7
⊢ (𝜑 → 𝑀 = 𝑋) | 
| 15 | 14 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → 𝑀 = 𝑋) | 
| 16 | 13, 15 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = 𝑋) | 
| 17 | 9, 16 | eqtrd 2776 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = 𝑋) | 
| 18 |  | metakunt20.7 | . . . 4
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) | 
| 19 | 2, 17, 18, 18 | fvmptd 7022 | . . 3
⊢ (𝜑 → (𝐵‘𝑋) = 𝑋) | 
| 20 | 10 | fveq2d 6909 | . . . . 5
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑋) = ({〈𝑀, 𝑀〉}‘𝑀)) | 
| 21 |  | metakunt20.1 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 22 |  | fvsng 7201 | . . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ) →
({〈𝑀, 𝑀〉}‘𝑀) = 𝑀) | 
| 23 | 21, 21, 22 | syl2anc 584 | . . . . 5
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑀) = 𝑀) | 
| 24 | 20, 23 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑋) = 𝑀) | 
| 25 | 24 | eqcomd 2742 | . . 3
⊢ (𝜑 → 𝑀 = ({〈𝑀, 𝑀〉}‘𝑋)) | 
| 26 | 19, 10, 25 | 3eqtrd 2780 | . 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 42225 | . . . . . 6
⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) | 
| 32 | 31 | simpld 494 | . . . . 5
⊢ (𝜑 → (𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) | 
| 33 | 32 | simp3d 1144 | . . . 4
⊢ (𝜑 → (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 34 | 31 | simprd 495 | . . . 4
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) | 
| 35 | 21 | nnzd 12642 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 36 |  | fzsn 13607 | . . . . . . . 8
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) | 
| 37 | 35, 36 | syl 17 | . . . . . . 7
⊢ (𝜑 → (𝑀...𝑀) = {𝑀}) | 
| 38 | 37 | ineq2d 4219 | . . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀})) | 
| 39 | 38 | eqcomd 2742 | . . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀))) | 
| 40 | 27 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ ℂ) | 
| 41 | 21 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈ ℂ) | 
| 42 | 40, 41 | pncan3d 11624 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 + (𝑀 − 𝐼)) = 𝑀) | 
| 43 | 42 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝜑 → (1..^(𝐼 + (𝑀 − 𝐼))) = (1..^𝑀)) | 
| 44 |  | fzoval 13701 | . . . . . . . . . . . . 13
⊢ (𝑀 ∈ ℤ →
(1..^𝑀) = (1...(𝑀 − 1))) | 
| 45 | 35, 44 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (1..^𝑀) = (1...(𝑀 − 1))) | 
| 46 | 43, 45 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → (1..^(𝐼 + (𝑀 − 𝐼))) = (1...(𝑀 − 1))) | 
| 47 | 46 | eqcomd 2742 | . . . . . . . . . 10
⊢ (𝜑 → (1...(𝑀 − 1)) = (1..^(𝐼 + (𝑀 − 𝐼)))) | 
| 48 |  | nnuz 12922 | . . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) | 
| 49 | 27, 48 | eleqtrdi 2850 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈
(ℤ≥‘1)) | 
| 50 | 27 | nnzd 12642 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 51 | 50, 35 | jca 511 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ)) | 
| 52 |  | znn0sub 12666 | . . . . . . . . . . . . 13
⊢ ((𝐼 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐼 ≤ 𝑀 ↔ (𝑀 − 𝐼) ∈
ℕ0)) | 
| 53 | 51, 52 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐼 ≤ 𝑀 ↔ (𝑀 − 𝐼) ∈
ℕ0)) | 
| 54 | 28, 53 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − 𝐼) ∈
ℕ0) | 
| 55 |  | fzoun 13737 | . . . . . . . . . . 11
⊢ ((𝐼 ∈
(ℤ≥‘1) ∧ (𝑀 − 𝐼) ∈ ℕ0) →
(1..^(𝐼 + (𝑀 − 𝐼))) = ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼))))) | 
| 56 | 49, 54, 55 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (1..^(𝐼 + (𝑀 − 𝐼))) = ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼))))) | 
| 57 | 47, 56 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (1...(𝑀 − 1)) = ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼))))) | 
| 58 |  | fzoval 13701 | . . . . . . . . . . 11
⊢ (𝐼 ∈ ℤ →
(1..^𝐼) = (1...(𝐼 − 1))) | 
| 59 | 50, 58 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (1..^𝐼) = (1...(𝐼 − 1))) | 
| 60 | 42 | oveq2d 7448 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐼..^(𝐼 + (𝑀 − 𝐼))) = (𝐼..^𝑀)) | 
| 61 |  | fzoval 13701 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ → (𝐼..^𝑀) = (𝐼...(𝑀 − 1))) | 
| 62 | 35, 61 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐼..^𝑀) = (𝐼...(𝑀 − 1))) | 
| 63 | 60, 62 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (𝐼..^(𝐼 + (𝑀 − 𝐼))) = (𝐼...(𝑀 − 1))) | 
| 64 | 59, 63 | uneq12d 4168 | . . . . . . . . 9
⊢ (𝜑 → ((1..^𝐼) ∪ (𝐼..^(𝐼 + (𝑀 − 𝐼)))) = ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 65 | 57, 64 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → (1...(𝑀 − 1)) = ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 66 | 65 | ineq1d 4218 | . . . . . . 7
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑀)) = (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀))) | 
| 67 | 66 | eqcomd 2742 | . . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀)) = ((1...(𝑀 − 1)) ∩ (𝑀...𝑀))) | 
| 68 | 21 | nnred 12282 | . . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℝ) | 
| 69 | 68 | ltm1d 12201 | . . . . . . 7
⊢ (𝜑 → (𝑀 − 1) < 𝑀) | 
| 70 |  | fzdisj 13592 | . . . . . . 7
⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 71 | 69, 70 | syl 17 | . . . . . 6
⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑀)) = ∅) | 
| 72 | 67, 71 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ (𝑀...𝑀)) = ∅) | 
| 73 | 39, 72 | eqtrd 2776 | . . . 4
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) | 
| 74 |  | elsng 4639 | . . . . . 6
⊢ (𝑋 ∈ (1...𝑀) → (𝑋 ∈ {𝑀} ↔ 𝑋 = 𝑀)) | 
| 75 | 18, 74 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑋 ∈ {𝑀} ↔ 𝑋 = 𝑀)) | 
| 76 | 10, 75 | mpbird 257 | . . . 4
⊢ (𝜑 → 𝑋 ∈ {𝑀}) | 
| 77 | 33, 34, 73, 76 | fvun2d 7002 | . . 3
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = ({〈𝑀, 𝑀〉}‘𝑋)) | 
| 78 | 77 | eqcomd 2742 | . 2
⊢ (𝜑 → ({〈𝑀, 𝑀〉}‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) | 
| 79 | 26, 78 | eqtrd 2776 | 1
⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |