Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
β’
(β€β₯βπ) = (β€β₯βπ) |
2 | | simpr 486 |
. . . . 5
β’ ((π β§ π β β€) β π β β€) |
3 | | sumss.1 |
. . . . . . 7
β’ (π β π΄ β π΅) |
4 | | sumss.4 |
. . . . . . 7
β’ (π β π΅ β (β€β₯βπ)) |
5 | 3, 4 | sstrd 3959 |
. . . . . 6
β’ (π β π΄ β (β€β₯βπ)) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ π β β€) β π΄ β (β€β₯βπ)) |
7 | | nfcv 2908 |
. . . . . . 7
β’
β²ππ |
8 | | nffvmpt1 6858 |
. . . . . . . 8
β’
β²π((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) |
9 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π β π΄ |
10 | | nffvmpt1 6858 |
. . . . . . . . 9
β’
β²π((π β π΄ β¦ πΆ)βπ) |
11 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π0 |
12 | 9, 10, 11 | nfif 4521 |
. . . . . . . 8
β’
β²πif(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0) |
13 | 8, 12 | nfeq 2921 |
. . . . . . 7
β’
β²π((π β
(β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0) |
14 | | fveq2 6847 |
. . . . . . . 8
β’ (π = π β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ)) |
15 | | eleq1w 2821 |
. . . . . . . . 9
β’ (π = π β (π β π΄ β π β π΄)) |
16 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = π β ((π β π΄ β¦ πΆ)βπ) = ((π β π΄ β¦ πΆ)βπ)) |
17 | 15, 16 | ifbieq1d 4515 |
. . . . . . . 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 6963 |
. . . . . . . . . 10
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = ( I βif(π β π΄, πΆ, 0))) |
21 | | iftrue 4497 |
. . . . . . . . . . 11
β’ (π β π΄ β if(π β π΄, πΆ, 0) = πΆ) |
22 | 21 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π β π΄ β ( I βif(π β π΄, πΆ, 0)) = ( I βπΆ)) |
23 | 20, 22 | sylan9eq 2797 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β π΄) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = ( I βπΆ)) |
24 | | iftrue 4497 |
. . . . . . . . . . 11
β’ (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0) = ((π β π΄ β¦ πΆ)βπ)) |
25 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (π β π΄ β¦ πΆ) = (π β π΄ β¦ πΆ) |
26 | 25 | fvmpt2i 6963 |
. . . . . . . . . . 11
β’ (π β π΄ β ((π β π΄ β¦ πΆ)βπ) = ( I βπΆ)) |
27 | 24, 26 | eqtrd 2777 |
. . . . . . . . . 10
β’ (π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0) = ( I βπΆ)) |
28 | 27 | adantl 483 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0) = ( I βπΆ)) |
29 | 23, 28 | eqtr4d 2780 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ π β π΄) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0)) |
30 | | iffalse 4500 |
. . . . . . . . . . . 12
β’ (Β¬
π β π΄ β if(π β π΄, πΆ, 0) = 0) |
31 | 30 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (Β¬
π β π΄ β ( I βif(π β π΄, πΆ, 0)) = ( I β0)) |
32 | | 0z 12517 |
. . . . . . . . . . . 12
β’ 0 β
β€ |
33 | | fvi 6922 |
. . . . . . . . . . . 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 4500 |
. . . . . . . . . 10
β’ (Β¬
π β π΄ β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0) = 0) |
38 | 37 | adantl 483 |
. . . . . . . . 9
β’ ((π β
(β€β₯βπ) β§ Β¬ π β π΄) β if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0) = 0) |
39 | 36, 38 | eqtr4d 2780 |
. . . . . . . 8
β’ ((π β
(β€β₯βπ) β§ Β¬ π β π΄) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0)) |
40 | 29, 39 | pm2.61dan 812 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0)) |
41 | 7, 13, 18, 40 | vtoclgaf 3536 |
. . . . . 6
β’ (π β
(β€β₯βπ) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0)) |
42 | 41 | adantl 483 |
. . . . 5
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΄, ((π β π΄ β¦ πΆ)βπ), 0)) |
43 | | sumss.2 |
. . . . . . . 8
β’ ((π β§ π β π΄) β πΆ β β) |
44 | 43 | fmpttd 7068 |
. . . . . . 7
β’ (π β (π β π΄ β¦ πΆ):π΄βΆβ) |
45 | 44 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β€) β (π β π΄ β¦ πΆ):π΄βΆβ) |
46 | 45 | ffvelcdmda 7040 |
. . . . 5
β’ (((π β§ π β β€) β§ π β π΄) β ((π β π΄ β¦ πΆ)βπ) β β) |
47 | 1, 2, 6, 42, 46 | zsum 15610 |
. . . 4
β’ ((π β§ π β β€) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = ( β βseqπ( + , (π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))))) |
48 | 4 | adantr 482 |
. . . . 5
β’ ((π β§ π β β€) β π΅ β (β€β₯βπ)) |
49 | | nfv 1918 |
. . . . . . . . 9
β’
β²ππ |
50 | | nfv 1918 |
. . . . . . . . . . 11
β’
β²π π β π΅ |
51 | | nffvmpt1 6858 |
. . . . . . . . . . 11
β’
β²π((π β π΅ β¦ πΆ)βπ) |
52 | 50, 51, 11 | nfif 4521 |
. . . . . . . . . 10
β’
β²πif(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) |
53 | 8, 52 | nfeq 2921 |
. . . . . . . . 9
β’
β²π((π β
(β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) |
54 | 49, 53 | nfim 1900 |
. . . . . . . 8
β’
β²π(π β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)) |
55 | | eleq1w 2821 |
. . . . . . . . . . 11
β’ (π = π β (π β π΅ β π β π΅)) |
56 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β ((π β π΅ β¦ πΆ)βπ) = ((π β π΅ β¦ πΆ)βπ)) |
57 | 55, 56 | ifbieq1d 4515 |
. . . . . . . . . 10
β’ (π = π β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)) |
58 | 14, 57 | eqeq12d 2753 |
. . . . . . . . 9
β’ (π = π β (((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0))) |
59 | 58 | imbi2d 341 |
. . . . . . . 8
β’ (π = π β ((π β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)) β (π β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)))) |
60 | 23 | adantll 713 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = ( I βπΆ)) |
61 | 3 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β€β₯βπ)) β π΄ β π΅) |
62 | 61 | sselda 3949 |
. . . . . . . . . . . 12
β’ (((π β§ π β (β€β₯βπ)) β§ π β π΄) β π β π΅) |
63 | | iftrue 4497 |
. . . . . . . . . . . . 13
β’ (π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = ((π β π΅ β¦ πΆ)βπ)) |
64 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β¦ πΆ) = (π β π΅ β¦ πΆ) |
65 | 64 | fvmpt2i 6963 |
. . . . . . . . . . . . 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 713 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯βπ)) β§ Β¬ π β π΄) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = 0) |
70 | 66 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = ( I βπΆ)) |
71 | | eldif 3925 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅ β π΄) β (π β π΅ β§ Β¬ π β π΄)) |
72 | | sumss.3 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (π΅ β π΄)) β πΆ = 0) |
73 | 72 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π΅ β π΄)) β ( I βπΆ) = ( I β0)) |
74 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . 19
β’ 0 β
β |
75 | | fvi 6922 |
. . . . . . . . . . . . . . . . . . 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 596 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β ( I βπΆ) = 0) |
79 | 70, 78 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0) |
80 | 79 | expr 458 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0)) |
81 | | iffalse 4500 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π β π΅ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0) |
82 | 81 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ π β π΅) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0) |
83 | 82 | a1d 25 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ π β π΅) β (Β¬ π β π΄ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0)) |
84 | 80, 83 | pm2.61dan 812 |
. . . . . . . . . . . . 13
β’ (π β (Β¬ π β π΄ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0)) |
85 | 84 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β€β₯βπ)) β (Β¬ π β π΄ β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0)) |
86 | 85 | imp 408 |
. . . . . . . . . . 11
β’ (((π β§ π β (β€β₯βπ)) β§ Β¬ π β π΄) β if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0) = 0) |
87 | 69, 86 | eqtr4d 2780 |
. . . . . . . . . 10
β’ (((π β§ π β (β€β₯βπ)) β§ Β¬ π β π΄) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)) |
88 | 68, 87 | pm2.61dan 812 |
. . . . . . . . 9
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)) |
89 | 88 | expcom 415 |
. . . . . . . 8
β’ (π β
(β€β₯βπ) β (π β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0))) |
90 | 7, 54, 59, 89 | vtoclgaf 3536 |
. . . . . . 7
β’ (π β
(β€β₯βπ) β (π β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0))) |
91 | 90 | impcom 409 |
. . . . . 6
β’ ((π β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)) |
92 | 91 | adantlr 714 |
. . . . 5
β’ (((π β§ π β β€) β§ π β (β€β₯βπ)) β ((π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))βπ) = if(π β π΅, ((π β π΅ β¦ πΆ)βπ), 0)) |
93 | 43 | ex 414 |
. . . . . . . . . 10
β’ (π β (π β π΄ β πΆ β β)) |
94 | 93 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (π β π΄ β πΆ β β)) |
95 | 72, 74 | eqeltrdi 2846 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΅ β π΄)) β πΆ β β) |
96 | 71, 95 | sylan2br 596 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ Β¬ π β π΄)) β πΆ β β) |
97 | 96 | expr 458 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β (Β¬ π β π΄ β πΆ β β)) |
98 | 94, 97 | pm2.61d 179 |
. . . . . . . 8
β’ ((π β§ π β π΅) β πΆ β β) |
99 | 98 | fmpttd 7068 |
. . . . . . 7
β’ (π β (π β π΅ β¦ πΆ):π΅βΆβ) |
100 | 99 | adantr 482 |
. . . . . 6
β’ ((π β§ π β β€) β (π β π΅ β¦ πΆ):π΅βΆβ) |
101 | 100 | ffvelcdmda 7040 |
. . . . 5
β’ (((π β§ π β β€) β§ π β π΅) β ((π β π΅ β¦ πΆ)βπ) β β) |
102 | 1, 2, 48, 92, 101 | zsum 15610 |
. . . 4
β’ ((π β§ π β β€) β Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ) = ( β βseqπ( + , (π β (β€β₯βπ) β¦ if(π β π΄, πΆ, 0))))) |
103 | 47, 102 | eqtr4d 2780 |
. . 3
β’ ((π β§ π β β€) β Ξ£π β π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΅ ((π β π΅ β¦ πΆ)βπ)) |
104 | | sumfc 15601 |
. . 3
β’
Ξ£π β
π΄ ((π β π΄ β¦ πΆ)βπ) = Ξ£π β π΄ πΆ |
105 | | sumfc 15601 |
. . 3
β’
Ξ£π β
π΅ ((π β π΅ β¦ πΆ)βπ) = Ξ£π β π΅ πΆ |
106 | 103, 104,
105 | 3eqtr3g 2800 |
. 2
β’ ((π β§ π β β€) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |
107 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ Β¬ π β β€) β π΄ β π΅) |
108 | | uzf 12773 |
. . . . . . . . . . . 12
β’
β€β₯:β€βΆπ« β€ |
109 | 108 | fdmi 6685 |
. . . . . . . . . . 11
β’ dom
β€β₯ = β€ |
110 | 109 | eleq2i 2830 |
. . . . . . . . . 10
β’ (π β dom
β€β₯ β π β β€) |
111 | | ndmfv 6882 |
. . . . . . . . . 10
β’ (Β¬
π β dom
β€β₯ β (β€β₯βπ) = β
) |
112 | 110, 111 | sylnbir 331 |
. . . . . . . . 9
β’ (Β¬
π β β€ β
(β€β₯βπ) = β
) |
113 | 112 | sseq2d 3981 |
. . . . . . . 8
β’ (Β¬
π β β€ β
(π΅ β
(β€β₯βπ) β π΅ β β
)) |
114 | 4, 113 | imbitrid 243 |
. . . . . . 7
β’ (Β¬
π β β€ β
(π β π΅ β β
)) |
115 | 114 | impcom 409 |
. . . . . 6
β’ ((π β§ Β¬ π β β€) β π΅ β β
) |
116 | 107, 115 | sstrd 3959 |
. . . . 5
β’ ((π β§ Β¬ π β β€) β π΄ β β
) |
117 | | ss0 4363 |
. . . . 5
β’ (π΄ β β
β π΄ = β
) |
118 | 116, 117 | syl 17 |
. . . 4
β’ ((π β§ Β¬ π β β€) β π΄ = β
) |
119 | | ss0 4363 |
. . . . 5
β’ (π΅ β β
β π΅ = β
) |
120 | 115, 119 | syl 17 |
. . . 4
β’ ((π β§ Β¬ π β β€) β π΅ = β
) |
121 | 118, 120 | eqtr4d 2780 |
. . 3
β’ ((π β§ Β¬ π β β€) β π΄ = π΅) |
122 | 121 | sumeq1d 15593 |
. 2
β’ ((π β§ Β¬ π β β€) β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |
123 | 106, 122 | pm2.61dan 812 |
1
β’ (π β Ξ£π β π΄ πΆ = Ξ£π β π΅ πΆ) |