Metamath Proof Explorer


Theorem cbvsum

Description: Change bound variable in a sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypotheses cbvsum.1 j = k B = C
cbvsum.2 _ k A
cbvsum.3 _ j A
cbvsum.4 _ k B
cbvsum.5 _ j C
Assertion cbvsum j A B = k A C

Proof

Step Hyp Ref Expression
1 cbvsum.1 j = k B = C
2 cbvsum.2 _ k A
3 cbvsum.3 _ j A
4 cbvsum.4 _ k B
5 cbvsum.5 _ j C
6 4 5 1 cbvcsbw n / j B = n / k C
7 6 a1i n / j B = n / k C
8 7 ifeq1d if n A n / j B 0 = if n A n / k C 0
9 8 mpteq2dv n if n A n / j B 0 = n if n A n / k C 0
10 9 seqeq3d seq m + n if n A n / j B 0 = seq m + n if n A n / k C 0
11 10 mptru seq m + n if n A n / j B 0 = seq m + n if n A n / k C 0
12 11 breq1i seq m + n if n A n / j B 0 x seq m + n if n A n / k C 0 x
13 12 anbi2i A m seq m + n if n A n / j B 0 x A m seq m + n if n A n / k C 0 x
14 13 rexbii m A m seq m + n if n A n / j B 0 x m A m seq m + n if n A n / k C 0 x
15 4 5 1 cbvcsbw f n / j B = f n / k C
16 15 a1i f n / j B = f n / k C
17 16 mpteq2dv n f n / j B = n f n / k C
18 17 seqeq3d seq 1 + n f n / j B = seq 1 + n f n / k C
19 18 mptru seq 1 + n f n / j B = seq 1 + n f n / k C
20 19 fveq1i seq 1 + n f n / j B m = seq 1 + n f n / k C m
21 20 eqeq2i x = seq 1 + n f n / j B m x = seq 1 + n f n / k C m
22 21 anbi2i f : 1 m 1-1 onto A x = seq 1 + n f n / j B m f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
23 22 exbii f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
24 23 rexbii m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
25 14 24 orbi12i m A m seq m + n if n A n / j B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
26 25 iotabii ι x | m A m seq m + n if n A n / j B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m = ι x | m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
27 df-sum j A B = ι x | m A m seq m + n if n A n / j B 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / j B m
28 df-sum k A C = ι x | m A m seq m + n if n A n / k C 0 x m f f : 1 m 1-1 onto A x = seq 1 + n f n / k C m
29 26 27 28 3eqtr4i j A B = k A C