Proof of Theorem metakunt21
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | metakunt21.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 |  | metakunt21.8 | . . . . . . 7
⊢ (𝜑 → ¬ 𝑋 = 𝑀) | 
| 11 | 10 | iffalsed 4535 | . . . . . 6
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) | 
| 12 |  | metakunt21.9 | . . . . . . 7
⊢ (𝜑 → 𝑋 < 𝐼) | 
| 13 | 12 | iftrued 4532 | . . . . . 6
⊢ (𝜑 → if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼))) = (𝑋 + (𝑀 − 𝐼))) | 
| 14 | 11, 13 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (𝑀 − 𝐼))) | 
| 15 | 14 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑋 = 𝑀, 𝑀, if(𝑋 < 𝐼, (𝑋 + (𝑀 − 𝐼)), (𝑋 + (1 − 𝐼)))) = (𝑋 + (𝑀 − 𝐼))) | 
| 16 | 9, 15 | eqtrd 2776 | . . 3
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → if(𝑥 = 𝑀, 𝑀, if(𝑥 < 𝐼, (𝑥 + (𝑀 − 𝐼)), (𝑥 + (1 − 𝐼)))) = (𝑋 + (𝑀 − 𝐼))) | 
| 17 |  | metakunt21.7 | . . 3
⊢ (𝜑 → 𝑋 ∈ (1...𝑀)) | 
| 18 | 17 | elfzelzd 13566 | . . . 4
⊢ (𝜑 → 𝑋 ∈ ℤ) | 
| 19 |  | metakunt21.1 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 20 | 19 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 21 |  | metakunt21.2 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ ℕ) | 
| 22 | 21 | nnzd 12642 | . . . . 5
⊢ (𝜑 → 𝐼 ∈ ℤ) | 
| 23 | 20, 22 | zsubcld 12729 | . . . 4
⊢ (𝜑 → (𝑀 − 𝐼) ∈ ℤ) | 
| 24 | 18, 23 | zaddcld 12728 | . . 3
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) ∈ ℤ) | 
| 25 | 2, 16, 17, 24 | fvmptd 7022 | . 2
⊢ (𝜑 → (𝐵‘𝑋) = (𝑋 + (𝑀 − 𝐼))) | 
| 26 |  | metakunt21.3 | . . . . . . . 8
⊢ (𝜑 → 𝐼 ≤ 𝑀) | 
| 27 |  | metakunt21.5 | . . . . . . . 8
⊢ 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼))) | 
| 28 |  | metakunt21.6 | . . . . . . . 8
⊢ 𝐷 = (𝑥 ∈ (𝐼...(𝑀 − 1)) ↦ (𝑥 + (1 − 𝐼))) | 
| 29 | 19, 21, 26, 1, 27, 28 | metakunt19 42225 | . . . . . . 7
⊢ (𝜑 → ((𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) ∧ {〈𝑀, 𝑀〉} Fn {𝑀})) | 
| 30 | 29 | simpld 494 | . . . . . 6
⊢ (𝜑 → (𝐶 Fn (1...(𝐼 − 1)) ∧ 𝐷 Fn (𝐼...(𝑀 − 1)) ∧ (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))))) | 
| 31 | 30 | simp3d 1144 | . . . . 5
⊢ (𝜑 → (𝐶 ∪ 𝐷) Fn ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 32 | 29 | simprd 495 | . . . . 5
⊢ (𝜑 → {〈𝑀, 𝑀〉} Fn {𝑀}) | 
| 33 |  | indir 4285 | . . . . . . 7
⊢
(((1...(𝐼 −
1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) | 
| 34 | 33 | a1i 11 | . . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀}))) | 
| 35 | 19, 21, 26 | metakunt18 42224 | . . . . . . . . . 10
⊢ (𝜑 → ((((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) ∧ (((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ (1...(𝑀 − 𝐼))) = ∅ ∧ ((((𝑀 − 𝐼) + 1)...(𝑀 − 1)) ∩ {𝑀}) = ∅ ∧ ((1...(𝑀 − 𝐼)) ∩ {𝑀}) = ∅))) | 
| 36 | 35 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅ ∧ ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅ ∧ ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅)) | 
| 37 | 36 | simp2d 1143 | . . . . . . . 8
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ {𝑀}) = ∅) | 
| 38 | 36 | simp3d 1144 | . . . . . . . 8
⊢ (𝜑 → ((𝐼...(𝑀 − 1)) ∩ {𝑀}) = ∅) | 
| 39 | 37, 38 | uneq12d 4168 | . . . . . . 7
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = (∅ ∪
∅)) | 
| 40 |  | unidm 4156 | . . . . . . . 8
⊢ (∅
∪ ∅) = ∅ | 
| 41 | 40 | a1i 11 | . . . . . . 7
⊢ (𝜑 → (∅ ∪ ∅) =
∅) | 
| 42 | 39, 41 | eqtrd 2776 | . . . . . 6
⊢ (𝜑 → (((1...(𝐼 − 1)) ∩ {𝑀}) ∪ ((𝐼...(𝑀 − 1)) ∩ {𝑀})) = ∅) | 
| 43 | 34, 42 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1))) ∩ {𝑀}) = ∅) | 
| 44 |  | 1zzd 12650 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) | 
| 45 | 22, 44 | zsubcld 12729 | . . . . . . 7
⊢ (𝜑 → (𝐼 − 1) ∈ ℤ) | 
| 46 |  | elfznn 13594 | . . . . . . . . 9
⊢ (𝑋 ∈ (1...𝑀) → 𝑋 ∈ ℕ) | 
| 47 | 17, 46 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℕ) | 
| 48 | 47 | nnge1d 12315 | . . . . . . 7
⊢ (𝜑 → 1 ≤ 𝑋) | 
| 49 |  | zltlem1 12672 | . . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝐼 ∈ ℤ) → (𝑋 < 𝐼 ↔ 𝑋 ≤ (𝐼 − 1))) | 
| 50 | 18, 22, 49 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → (𝑋 < 𝐼 ↔ 𝑋 ≤ (𝐼 − 1))) | 
| 51 | 12, 50 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → 𝑋 ≤ (𝐼 − 1)) | 
| 52 | 44, 45, 18, 48, 51 | elfzd 13556 | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ (1...(𝐼 − 1))) | 
| 53 |  | elun1 4181 | . . . . . 6
⊢ (𝑋 ∈ (1...(𝐼 − 1)) → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 54 | 52, 53 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ ((1...(𝐼 − 1)) ∪ (𝐼...(𝑀 − 1)))) | 
| 55 | 31, 32, 43, 54 | fvun1d 7001 | . . . 4
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = ((𝐶 ∪ 𝐷)‘𝑋)) | 
| 56 | 30 | simp1d 1142 | . . . . . 6
⊢ (𝜑 → 𝐶 Fn (1...(𝐼 − 1))) | 
| 57 | 30 | simp2d 1143 | . . . . . 6
⊢ (𝜑 → 𝐷 Fn (𝐼...(𝑀 − 1))) | 
| 58 | 36 | simp1d 1142 | . . . . . 6
⊢ (𝜑 → ((1...(𝐼 − 1)) ∩ (𝐼...(𝑀 − 1))) = ∅) | 
| 59 | 56, 57, 58, 52 | fvun1d 7001 | . . . . 5
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝐶‘𝑋)) | 
| 60 | 27 | a1i 11 | . . . . . 6
⊢ (𝜑 → 𝐶 = (𝑥 ∈ (1...(𝐼 − 1)) ↦ (𝑥 + (𝑀 − 𝐼)))) | 
| 61 | 5 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → (𝑥 + (𝑀 − 𝐼)) = (𝑋 + (𝑀 − 𝐼))) | 
| 62 | 60, 61, 52, 24 | fvmptd 7022 | . . . . 5
⊢ (𝜑 → (𝐶‘𝑋) = (𝑋 + (𝑀 − 𝐼))) | 
| 63 | 59, 62 | eqtrd 2776 | . . . 4
⊢ (𝜑 → ((𝐶 ∪ 𝐷)‘𝑋) = (𝑋 + (𝑀 − 𝐼))) | 
| 64 | 55, 63 | eqtrd 2776 | . . 3
⊢ (𝜑 → (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋) = (𝑋 + (𝑀 − 𝐼))) | 
| 65 | 64 | eqcomd 2742 | . 2
⊢ (𝜑 → (𝑋 + (𝑀 − 𝐼)) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) | 
| 66 | 25, 65 | eqtrd 2776 | 1
⊢ (𝜑 → (𝐵‘𝑋) = (((𝐶 ∪ 𝐷) ∪ {〈𝑀, 𝑀〉})‘𝑋)) |