| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
| 2 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝑀 ∈ ℤ) |
| 3 | | sumss.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
| 4 | | sumss.4 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ (ℤ≥‘𝑀)) |
| 5 | 3, 4 | sstrd 3994 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ (ℤ≥‘𝑀)) |
| 6 | 5 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝐴 ⊆ (ℤ≥‘𝑀)) |
| 7 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑘𝑚 |
| 8 | | nffvmpt1 6917 |
. . . . . . . 8
⊢
Ⅎ𝑘((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) |
| 9 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑚 ∈ 𝐴 |
| 10 | | nffvmpt1 6917 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) |
| 11 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑘0 |
| 12 | 9, 10, 11 | nfif 4556 |
. . . . . . . 8
⊢
Ⅎ𝑘if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 0) |
| 13 | 8, 12 | nfeq 2919 |
. . . . . . 7
⊢
Ⅎ𝑘((𝑘 ∈
(ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 0) |
| 14 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚)) |
| 15 | | eleq1w 2824 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐴 ↔ 𝑚 ∈ 𝐴)) |
| 16 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) |
| 17 | 15, 16 | ifbieq1d 4550 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0) = if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 0)) |
| 18 | 14, 17 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑘 = 𝑚 → (((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0) ↔ ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 0))) |
| 19 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑘 ∈
(ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0)) = (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0)) |
| 20 | 19 | fvmpt2i 7026 |
. . . . . . . . . 10
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 0))) |
| 21 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) = 𝐶) |
| 22 | 21 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐴 → ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 0)) = ( I ‘𝐶)) |
| 23 | 20, 22 | sylan9eq 2797 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = ( I ‘𝐶)) |
| 24 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) |
| 25 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 ↦ 𝐶) = (𝑘 ∈ 𝐴 ↦ 𝐶) |
| 26 | 25 | fvmpt2i 7026 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = ( I ‘𝐶)) |
| 27 | 24, 26 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0) = ( I ‘𝐶)) |
| 28 | 27 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0) = ( I ‘𝐶)) |
| 29 | 23, 28 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0)) |
| 30 | | iffalse 4534 |
. . . . . . . . . . . 12
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, 𝐶, 0) = 0) |
| 31 | 30 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (¬
𝑘 ∈ 𝐴 → ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 0)) = ( I ‘0)) |
| 32 | | 0z 12624 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
| 33 | | fvi 6985 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → ( I ‘0) = 0) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ( I
‘0) = 0 |
| 35 | 31, 34 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ 𝐴 → ( I ‘if(𝑘 ∈ 𝐴, 𝐶, 0)) = 0) |
| 36 | 20, 35 | sylan9eq 2797 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ¬ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = 0) |
| 37 | | iffalse 4534 |
. . . . . . . . . 10
⊢ (¬
𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0) = 0) |
| 38 | 37 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0) = 0) |
| 39 | 36, 38 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝑘 ∈
(ℤ≥‘𝑀) ∧ ¬ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0)) |
| 40 | 29, 39 | pm2.61dan 813 |
. . . . . . 7
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘), 0)) |
| 41 | 7, 13, 18, 40 | vtoclgaf 3576 |
. . . . . 6
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 0)) |
| 42 | 41 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐴, ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚), 0)) |
| 43 | | sumss.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
| 44 | 43 | fmpttd 7135 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
| 45 | 44 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
| 46 | 45 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) ∈ ℂ) |
| 47 | 1, 2, 6, 42, 46 | zsum 15754 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ( ⇝ ‘seq𝑀( + , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))))) |
| 48 | 4 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → 𝐵 ⊆ (ℤ≥‘𝑀)) |
| 49 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑘𝜑 |
| 50 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘 𝑚 ∈ 𝐵 |
| 51 | | nffvmpt1 6917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) |
| 52 | 50, 51, 11 | nfif 4556 |
. . . . . . . . . 10
⊢
Ⅎ𝑘if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0) |
| 53 | 8, 52 | nfeq 2919 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝑘 ∈
(ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0) |
| 54 | 49, 53 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0)) |
| 55 | | eleq1w 2824 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑘 ∈ 𝐵 ↔ 𝑚 ∈ 𝐵)) |
| 56 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
| 57 | 55, 56 | ifbieq1d 4550 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0)) |
| 58 | 14, 57 | eqeq12d 2753 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) ↔ ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0))) |
| 59 | 58 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑘 = 𝑚 → ((𝜑 → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0)) ↔ (𝜑 → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0)))) |
| 60 | 23 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = ( I ‘𝐶)) |
| 61 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ⊆ 𝐵) |
| 62 | 61 | sselda 3983 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐵) |
| 63 | | iftrue 4531 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘)) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ 𝐵 ↦ 𝐶) = (𝑘 ∈ 𝐵 ↦ 𝐶) |
| 65 | 64 | fvmpt2i 7026 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐵 → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘) = ( I ‘𝐶)) |
| 66 | 63, 65 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = ( I ‘𝐶)) |
| 67 | 62, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = ( I ‘𝐶)) |
| 68 | 60, 67 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0)) |
| 69 | 36 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = 0) |
| 70 | 66 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = ( I ‘𝐶)) |
| 71 | | eldif 3961 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (𝐵 ∖ 𝐴) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) |
| 72 | | sumss.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0) |
| 73 | 72 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → ( I ‘𝐶) = ( I ‘0)) |
| 74 | | 0cn 11253 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℂ |
| 75 | | fvi 6985 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
ℂ → ( I ‘0) = 0) |
| 76 | 74, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ( I
‘0) = 0 |
| 77 | 73, 76 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → ( I ‘𝐶) = 0) |
| 78 | 71, 77 | sylan2br 595 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → ( I ‘𝐶) = 0) |
| 79 | 70, 78 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0) |
| 80 | 79 | expr 456 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0)) |
| 81 | | iffalse 4534 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑘 ∈ 𝐵 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0) |
| 82 | 81 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐵) → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0) |
| 83 | 82 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0)) |
| 84 | 80, 83 | pm2.61dan 813 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0)) |
| 85 | 84 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (¬ 𝑘 ∈ 𝐴 → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0)) |
| 86 | 85 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0) = 0) |
| 87 | 69, 86 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) ∧ ¬ 𝑘 ∈ 𝐴) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0)) |
| 88 | 68, 87 | pm2.61dan 813 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0)) |
| 89 | 88 | expcom 413 |
. . . . . . . 8
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝜑 → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑘) = if(𝑘 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑘), 0))) |
| 90 | 7, 54, 59, 89 | vtoclgaf 3576 |
. . . . . . 7
⊢ (𝑚 ∈
(ℤ≥‘𝑀) → (𝜑 → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0))) |
| 91 | 90 | impcom 407 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0)) |
| 92 | 91 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ (ℤ≥‘𝑀)) → ((𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))‘𝑚) = if(𝑚 ∈ 𝐵, ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚), 0)) |
| 93 | 43 | ex 412 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
| 94 | 93 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
| 95 | 72, 74 | eqeltrdi 2849 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ) |
| 96 | 71, 95 | sylan2br 595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → 𝐶 ∈ ℂ) |
| 97 | 96 | expr 456 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ)) |
| 98 | 94, 97 | pm2.61d 179 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
| 99 | 98 | fmpttd 7135 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ) |
| 100 | 99 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ) |
| 101 | 100 | ffvelcdmda 7104 |
. . . . 5
⊢ (((𝜑 ∧ 𝑀 ∈ ℤ) ∧ 𝑚 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ) |
| 102 | 1, 2, 48, 92, 101 | zsum 15754 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ( ⇝ ‘seq𝑀( + , (𝑘 ∈ (ℤ≥‘𝑀) ↦ if(𝑘 ∈ 𝐴, 𝐶, 0))))) |
| 103 | 47, 102 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚)) |
| 104 | | sumfc 15745 |
. . 3
⊢
Σ𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶 |
| 105 | | sumfc 15745 |
. . 3
⊢
Σ𝑚 ∈
𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐵 𝐶 |
| 106 | 103, 104,
105 | 3eqtr3g 2800 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
| 107 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 ⊆ 𝐵) |
| 108 | | uzf 12881 |
. . . . . . . . . . . 12
⊢
ℤ≥:ℤ⟶𝒫 ℤ |
| 109 | 108 | fdmi 6747 |
. . . . . . . . . . 11
⊢ dom
ℤ≥ = ℤ |
| 110 | 109 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑀 ∈ dom
ℤ≥ ↔ 𝑀 ∈ ℤ) |
| 111 | | ndmfv 6941 |
. . . . . . . . . 10
⊢ (¬
𝑀 ∈ dom
ℤ≥ → (ℤ≥‘𝑀) = ∅) |
| 112 | 110, 111 | sylnbir 331 |
. . . . . . . . 9
⊢ (¬
𝑀 ∈ ℤ →
(ℤ≥‘𝑀) = ∅) |
| 113 | 112 | sseq2d 4016 |
. . . . . . . 8
⊢ (¬
𝑀 ∈ ℤ →
(𝐵 ⊆
(ℤ≥‘𝑀) ↔ 𝐵 ⊆ ∅)) |
| 114 | 4, 113 | imbitrid 244 |
. . . . . . 7
⊢ (¬
𝑀 ∈ ℤ →
(𝜑 → 𝐵 ⊆ ∅)) |
| 115 | 114 | impcom 407 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐵 ⊆ ∅) |
| 116 | 107, 115 | sstrd 3994 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 ⊆ ∅) |
| 117 | | ss0 4402 |
. . . . 5
⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) |
| 118 | 116, 117 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 = ∅) |
| 119 | | ss0 4402 |
. . . . 5
⊢ (𝐵 ⊆ ∅ → 𝐵 = ∅) |
| 120 | 115, 119 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐵 = ∅) |
| 121 | 118, 120 | eqtr4d 2780 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → 𝐴 = 𝐵) |
| 122 | 121 | sumeq1d 15736 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑀 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
| 123 | 106, 122 | pm2.61dan 813 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |