Step | Hyp | Ref
| Expression |
1 | | isumshft.5 |
. . . . . . . . 9
β’ (π β π β β€) |
2 | | isumshft.4 |
. . . . . . . . 9
β’ (π β πΎ β β€) |
3 | 1, 2 | zaddcld 12618 |
. . . . . . . 8
β’ (π β (π + πΎ) β β€) |
4 | | isumshft.2 |
. . . . . . . . . 10
β’ π =
(β€β₯β(π + πΎ)) |
5 | 4 | eleq2i 2830 |
. . . . . . . . 9
β’ (π β π β π β (β€β₯β(π + πΎ))) |
6 | 2 | zcnd 12615 |
. . . . . . . . . . 11
β’ (π β πΎ β β) |
7 | | eluzelcn 12782 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β(π + πΎ)) β π β β) |
8 | 7, 4 | eleq2s 2856 |
. . . . . . . . . . 11
β’ (π β π β π β β) |
9 | | isumshft.1 |
. . . . . . . . . . . . . 14
β’ π =
(β€β₯βπ) |
10 | 9 | fvexi 6861 |
. . . . . . . . . . . . 13
β’ π β V |
11 | 10 | mptex 7178 |
. . . . . . . . . . . 12
β’ (π β π β¦ π΅) β V |
12 | 11 | shftval 14966 |
. . . . . . . . . . 11
β’ ((πΎ β β β§ π β β) β (((π β π β¦ π΅) shift πΎ)βπ) = ((π β π β¦ π΅)β(π β πΎ))) |
13 | 6, 8, 12 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (((π β π β¦ π΅) shift πΎ)βπ) = ((π β π β¦ π΅)β(π β πΎ))) |
14 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β π β π) |
15 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β¦ π΅) = (π β π β¦ π΅) |
16 | 15 | fvmpt2i 6963 |
. . . . . . . . . . . . . . . 16
β’ (π β π β ((π β π β¦ π΅)βπ) = ( I βπ΅)) |
17 | 14, 16 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = ( I βπ΅)) |
18 | | eluzelcn 12782 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯βπ) β π β β) |
19 | 18, 9 | eleq2s 2856 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π β β) |
20 | | addcom 11348 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β β β§ π β β) β (πΎ + π) = (π + πΎ)) |
21 | 6, 19, 20 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β (πΎ + π) = (π + πΎ)) |
22 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β π β π) |
23 | 22, 9 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β π β (β€β₯βπ)) |
24 | | eluzadd 12799 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β
(β€β₯βπ) β§ πΎ β β€) β (π + πΎ) β
(β€β₯β(π + πΎ))) |
25 | 23, 2, 24 | syl2anr 598 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β π) β (π + πΎ) β
(β€β₯β(π + πΎ))) |
26 | 21, 25 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π) β (πΎ + π) β (β€β₯β(π + πΎ))) |
27 | 26, 4 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π) β (πΎ + π) β π) |
28 | | isumshft.3 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πΎ + π) β π΄ = π΅) |
29 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β¦ π΄) = (π β π β¦ π΄) |
30 | 28, 29 | fvmpti 6952 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ + π) β π β ((π β π β¦ π΄)β(πΎ + π)) = ( I βπ΅)) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π) β ((π β π β¦ π΄)β(πΎ + π)) = ( I βπ΅)) |
32 | 17, 31 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
33 | 32 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ (π β βπ β π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
34 | | nffvmpt1 6858 |
. . . . . . . . . . . . . . 15
β’
β²π((π β π β¦ π΅)βπ) |
35 | 34 | nfeq1 2923 |
. . . . . . . . . . . . . 14
β’
β²π((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) |
36 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)βπ)) |
37 | | oveq2 7370 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΎ + π) = (πΎ + π)) |
38 | 37 | fveq2d 6851 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π β π β¦ π΄)β(πΎ + π)) = ((π β π β¦ π΄)β(πΎ + π))) |
39 | 36, 38 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
β’ (π = π β (((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)))) |
40 | 35, 39 | rspc 3572 |
. . . . . . . . . . . . 13
β’ (π β π β (βπ β π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)))) |
41 | 33, 40 | mpan9 508 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
42 | 41 | ralrimiva 3144 |
. . . . . . . . . . 11
β’ (π β βπ β π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π))) |
43 | 1 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β β€) |
44 | 2 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β πΎ β β€) |
45 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π) β π β π) |
46 | 45, 4 | eleqtrdi 2848 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π) β π β (β€β₯β(π + πΎ))) |
47 | | eluzsub 12800 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ πΎ β β€ β§ π β
(β€β₯β(π + πΎ))) β (π β πΎ) β (β€β₯βπ)) |
48 | 43, 44, 46, 47 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (π β πΎ) β (β€β₯βπ)) |
49 | 48, 9 | eleqtrrdi 2849 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (π β πΎ) β π) |
50 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = (π β πΎ) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)β(π β πΎ))) |
51 | | oveq2 7370 |
. . . . . . . . . . . . . 14
β’ (π = (π β πΎ) β (πΎ + π) = (πΎ + (π β πΎ))) |
52 | 51 | fveq2d 6851 |
. . . . . . . . . . . . 13
β’ (π = (π β πΎ) β ((π β π β¦ π΄)β(πΎ + π)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ)))) |
53 | 50, 52 | eqeq12d 2753 |
. . . . . . . . . . . 12
β’ (π = (π β πΎ) β (((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β ((π β π β¦ π΅)β(π β πΎ)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ))))) |
54 | 53 | rspccva 3583 |
. . . . . . . . . . 11
β’
((βπ β
π ((π β π β¦ π΅)βπ) = ((π β π β¦ π΄)β(πΎ + π)) β§ (π β πΎ) β π) β ((π β π β¦ π΅)β(π β πΎ)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ)))) |
55 | 42, 49, 54 | syl2an2r 684 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((π β π β¦ π΅)β(π β πΎ)) = ((π β π β¦ π΄)β(πΎ + (π β πΎ)))) |
56 | | pncan3 11416 |
. . . . . . . . . . . 12
β’ ((πΎ β β β§ π β β) β (πΎ + (π β πΎ)) = π) |
57 | 6, 8, 56 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΎ + (π β πΎ)) = π) |
58 | 57 | fveq2d 6851 |
. . . . . . . . . 10
β’ ((π β§ π β π) β ((π β π β¦ π΄)β(πΎ + (π β πΎ))) = ((π β π β¦ π΄)βπ)) |
59 | 13, 55, 58 | 3eqtrrd 2782 |
. . . . . . . . 9
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) = (((π β π β¦ π΅) shift πΎ)βπ)) |
60 | 5, 59 | sylan2br 596 |
. . . . . . . 8
β’ ((π β§ π β (β€β₯β(π + πΎ))) β ((π β π β¦ π΄)βπ) = (((π β π β¦ π΅) shift πΎ)βπ)) |
61 | 3, 60 | seqfeq 13940 |
. . . . . . 7
β’ (π β seq(π + πΎ)( + , (π β π β¦ π΄)) = seq(π + πΎ)( + , ((π β π β¦ π΅) shift πΎ))) |
62 | 61 | breq1d 5120 |
. . . . . 6
β’ (π β (seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯ β seq(π + πΎ)( + , ((π β π β¦ π΅) shift πΎ)) β π₯)) |
63 | 11 | isershft 15555 |
. . . . . . 7
β’ ((π β β€ β§ πΎ β β€) β
(seqπ( + , (π β π β¦ π΅)) β π₯ β seq(π + πΎ)( + , ((π β π β¦ π΅) shift πΎ)) β π₯)) |
64 | 1, 2, 63 | syl2anc 585 |
. . . . . 6
β’ (π β (seqπ( + , (π β π β¦ π΅)) β π₯ β seq(π + πΎ)( + , ((π β π β¦ π΅) shift πΎ)) β π₯)) |
65 | 62, 64 | bitr4d 282 |
. . . . 5
β’ (π β (seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯ β seqπ( + , (π β π β¦ π΅)) β π₯)) |
66 | 65 | iotabidv 6485 |
. . . 4
β’ (π β (β©π₯seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯) = (β©π₯seqπ( + , (π β π β¦ π΅)) β π₯)) |
67 | | df-fv 6509 |
. . . 4
β’ ( β
βseq(π + πΎ)( + , (π β π β¦ π΄))) = (β©π₯seq(π + πΎ)( + , (π β π β¦ π΄)) β π₯) |
68 | | df-fv 6509 |
. . . 4
β’ ( β
βseqπ( + , (π β π β¦ π΅))) = (β©π₯seqπ( + , (π β π β¦ π΅)) β π₯) |
69 | 66, 67, 68 | 3eqtr4g 2802 |
. . 3
β’ (π β ( β βseq(π + πΎ)( + , (π β π β¦ π΄))) = ( β βseqπ( + , (π β π β¦ π΅)))) |
70 | | eqidd 2738 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) = ((π β π β¦ π΄)βπ)) |
71 | | isumshft.6 |
. . . . . 6
β’ ((π β§ π β π) β π΄ β β) |
72 | 71 | fmpttd 7068 |
. . . . 5
β’ (π β (π β π β¦ π΄):πβΆβ) |
73 | 72 | ffvelcdmda 7040 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΄)βπ) β β) |
74 | 4, 3, 70, 73 | isum 15611 |
. . 3
β’ (π β Ξ£π β π ((π β π β¦ π΄)βπ) = ( β βseq(π + πΎ)( + , (π β π β¦ π΄)))) |
75 | | eqidd 2738 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) = ((π β π β¦ π΅)βπ)) |
76 | 27 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ β π (πΎ + π) β π) |
77 | 37 | eleq1d 2823 |
. . . . . . . 8
β’ (π = π β ((πΎ + π) β π β (πΎ + π) β π)) |
78 | 77 | rspccva 3583 |
. . . . . . 7
β’
((βπ β
π (πΎ + π) β π β§ π β π) β (πΎ + π) β π) |
79 | 76, 78 | sylan 581 |
. . . . . 6
β’ ((π β§ π β π) β (πΎ + π) β π) |
80 | | ffvelcdm 7037 |
. . . . . 6
β’ (((π β π β¦ π΄):πβΆβ β§ (πΎ + π) β π) β ((π β π β¦ π΄)β(πΎ + π)) β β) |
81 | 72, 79, 80 | syl2an2r 684 |
. . . . 5
β’ ((π β§ π β π) β ((π β π β¦ π΄)β(πΎ + π)) β β) |
82 | 41, 81 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π β π) β ((π β π β¦ π΅)βπ) β β) |
83 | 9, 1, 75, 82 | isum 15611 |
. . 3
β’ (π β Ξ£π β π ((π β π β¦ π΅)βπ) = ( β βseqπ( + , (π β π β¦ π΅)))) |
84 | 69, 74, 83 | 3eqtr4d 2787 |
. 2
β’ (π β Ξ£π β π ((π β π β¦ π΄)βπ) = Ξ£π β π ((π β π β¦ π΅)βπ)) |
85 | | sumfc 15601 |
. 2
β’
Ξ£π β
π ((π β π β¦ π΄)βπ) = Ξ£π β π π΄ |
86 | | sumfc 15601 |
. 2
β’
Ξ£π β
π ((π β π β¦ π΅)βπ) = Ξ£π β π π΅ |
87 | 84, 85, 86 | 3eqtr3g 2800 |
1
β’ (π β Ξ£π β π π΄ = Ξ£π β π π΅) |