Proof of Theorem sumsplit
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sumsplit.4 | . . 3
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝑍) | 
| 2 |  | sumsplit.7 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∪ 𝐵)) → 𝐶 ∈ ℂ) | 
| 3 | 2 | ralrimiva 3146 | . . 3
⊢ (𝜑 → ∀𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 ∈ ℂ) | 
| 4 |  | sumsplit.1 | . . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) | 
| 5 | 4 | eqimssi 4044 | . . . . 5
⊢ 𝑍 ⊆
(ℤ≥‘𝑀) | 
| 6 | 5 | a1i 11 | . . . 4
⊢ (𝜑 → 𝑍 ⊆ (ℤ≥‘𝑀)) | 
| 7 | 6 | orcd 874 | . . 3
⊢ (𝜑 → (𝑍 ⊆ (ℤ≥‘𝑀) ∨ 𝑍 ∈ Fin)) | 
| 8 |  | sumss2 15762 | . . 3
⊢ ((((𝐴 ∪ 𝐵) ⊆ 𝑍 ∧ ∀𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 ∈ ℂ) ∧ (𝑍 ⊆ (ℤ≥‘𝑀) ∨ 𝑍 ∈ Fin)) → Σ𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0)) | 
| 9 | 1, 3, 7, 8 | syl21anc 838 | . 2
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0)) | 
| 10 |  | sumsplit.2 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 11 |  | sumsplit.5 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = if(𝑘 ∈ 𝐴, 𝐶, 0)) | 
| 12 |  | iftrue 4531 | . . . . . . . 8
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶) | 
| 13 | 12 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶) | 
| 14 |  | elun1 4182 | . . . . . . . 8
⊢ (𝑘 ∈ 𝐴 → 𝑘 ∈ (𝐴 ∪ 𝐵)) | 
| 15 | 14, 2 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) | 
| 16 | 13, 15 | eqeltrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) | 
| 17 |  | iffalse 4534 | . . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) = 0) | 
| 18 |  | 0cn 11253 | . . . . . . . 8
⊢ 0 ∈
ℂ | 
| 19 | 17, 18 | eqeltrdi 2849 | . . . . . . 7
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) | 
| 20 | 19 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) | 
| 21 | 16, 20 | pm2.61dan 813 | . . . . 5
⊢ (𝜑 → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) | 
| 22 | 21 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → if(𝑘 ∈ 𝐴, 𝐶, 0) ∈ ℂ) | 
| 23 |  | sumsplit.6 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = if(𝑘 ∈ 𝐵, 𝐶, 0)) | 
| 24 |  | iftrue 4531 | . . . . . . . 8
⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶) | 
| 25 | 24 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 𝐶) | 
| 26 |  | elun2 4183 | . . . . . . . 8
⊢ (𝑘 ∈ 𝐵 → 𝑘 ∈ (𝐴 ∪ 𝐵)) | 
| 27 | 26, 2 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) | 
| 28 | 25, 27 | eqeltrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) | 
| 29 |  | iffalse 4534 | . . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 0) = 0) | 
| 30 | 29, 18 | eqeltrdi 2849 | . . . . . . 7
⊢ (¬
𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) | 
| 31 | 30 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) | 
| 32 | 28, 31 | pm2.61dan 813 | . . . . 5
⊢ (𝜑 → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) | 
| 33 | 32 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → if(𝑘 ∈ 𝐵, 𝐶, 0) ∈ ℂ) | 
| 34 |  | sumsplit.8 | . . . 4
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) | 
| 35 |  | sumsplit.9 | . . . 4
⊢ (𝜑 → seq𝑀( + , 𝐺) ∈ dom ⇝ ) | 
| 36 | 4, 10, 11, 22, 23, 33, 34, 35 | isumadd 15803 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝑍 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐵, 𝐶, 0))) | 
| 37 | 15 | addridd 11461 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐶 + 0) = 𝐶) | 
| 38 |  | noel 4338 | . . . . . . . . . . 11
⊢  ¬
𝑘 ∈
∅ | 
| 39 |  | sumsplit.3 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) | 
| 40 | 39 | eleq2d 2827 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ 𝑘 ∈ ∅)) | 
| 41 |  | elin 3967 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ (𝐴 ∩ 𝐵) ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) | 
| 42 | 40, 41 | bitr3di 286 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ ∅ ↔ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵))) | 
| 43 | 38, 42 | mtbii 326 | . . . . . . . . . 10
⊢ (𝜑 → ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) | 
| 44 |  | imnan 399 | . . . . . . . . . 10
⊢ ((𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵) ↔ ¬ (𝑘 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) | 
| 45 | 43, 44 | sylibr 234 | . . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 → ¬ 𝑘 ∈ 𝐵)) | 
| 46 | 45 | imp 406 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐵) | 
| 47 | 46, 29 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, 𝐶, 0) = 0) | 
| 48 | 13, 47 | oveq12d 7449 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (𝐶 + 0)) | 
| 49 |  | iftrue 4531 | . . . . . . . 8
⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) → if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = 𝐶) | 
| 50 | 14, 49 | syl 17 | . . . . . . 7
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = 𝐶) | 
| 51 | 50 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = 𝐶) | 
| 52 | 37, 48, 51 | 3eqtr4rd 2788 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0))) | 
| 53 | 32 | addlidd 11462 | . . . . . . 7
⊢ (𝜑 → (0 + if(𝑘 ∈ 𝐵, 𝐶, 0)) = if(𝑘 ∈ 𝐵, 𝐶, 0)) | 
| 54 | 53 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐴) → (0 + if(𝑘 ∈ 𝐵, 𝐶, 0)) = if(𝑘 ∈ 𝐵, 𝐶, 0)) | 
| 55 | 17 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, 𝐶, 0) = 0) | 
| 56 | 55 | oveq1d 7446 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0)) = (0 + if(𝑘 ∈ 𝐵, 𝐶, 0))) | 
| 57 |  | elun 4153 | . . . . . . . . 9
⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) | 
| 58 |  | biorf 937 | . . . . . . . . 9
⊢ (¬
𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐵 ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))) | 
| 59 | 57, 58 | bitr4id 290 | . . . . . . . 8
⊢ (¬
𝑘 ∈ 𝐴 → (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ 𝑘 ∈ 𝐵)) | 
| 60 | 59 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐴) → (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ 𝑘 ∈ 𝐵)) | 
| 61 | 60 | ifbid 4549 | . . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = if(𝑘 ∈ 𝐵, 𝐶, 0)) | 
| 62 | 54, 56, 61 | 3eqtr4rd 2788 | . . . . 5
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0))) | 
| 63 | 52, 62 | pm2.61dan 813 | . . . 4
⊢ (𝜑 → if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0))) | 
| 64 | 63 | sumeq2sdv 15739 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ 𝑍 if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0) = Σ𝑘 ∈ 𝑍 (if(𝑘 ∈ 𝐴, 𝐶, 0) + if(𝑘 ∈ 𝐵, 𝐶, 0))) | 
| 65 | 1 | unssad 4193 | . . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑍) | 
| 66 | 15 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) | 
| 67 |  | sumss2 15762 | . . . . 5
⊢ (((𝐴 ⊆ 𝑍 ∧ ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) ∧ (𝑍 ⊆ (ℤ≥‘𝑀) ∨ 𝑍 ∈ Fin)) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐴, 𝐶, 0)) | 
| 68 | 65, 66, 7, 67 | syl21anc 838 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐴, 𝐶, 0)) | 
| 69 | 1 | unssbd 4194 | . . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝑍) | 
| 70 | 27 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) | 
| 71 |  | sumss2 15762 | . . . . 5
⊢ (((𝐵 ⊆ 𝑍 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) ∧ (𝑍 ⊆ (ℤ≥‘𝑀) ∨ 𝑍 ∈ Fin)) → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐵, 𝐶, 0)) | 
| 72 | 69, 70, 7, 71 | syl21anc 838 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐵, 𝐶, 0)) | 
| 73 | 68, 72 | oveq12d 7449 | . . 3
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶) = (Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐴, 𝐶, 0) + Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐵, 𝐶, 0))) | 
| 74 | 36, 64, 73 | 3eqtr4rd 2788 | . 2
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶) = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ (𝐴 ∪ 𝐵), 𝐶, 0)) | 
| 75 | 9, 74 | eqtr4d 2780 | 1
⊢ (𝜑 → Σ𝑘 ∈ (𝐴 ∪ 𝐵)𝐶 = (Σ𝑘 ∈ 𝐴 𝐶 + Σ𝑘 ∈ 𝐵 𝐶)) |