Theorem fsum0diag2 7382

Description: Two ways to express "the sum of A(j) x. B(k) where j + k <_ N."

Assertion

Ref	Expression
fsum0diag2	|- ((N e. NN0 /\ A.j e. (0...N)A e. CC /\ A.k e. (0...N)B e. CC) -> sum_j e. (0...N)sum_k e. (0...(N - j))(A x. B) = sum_j e. (0...N)sum_k e. (0...j)([_(j - k) / j]_A x. B))

Distinct variable groups:   A,k   B,j   j,k,N

Proof of Theorem fsum0diag2

Step	Hyp	Ref	Expression
1		fsum0diag 7381	. 2 |- ((N e. NN0 /\ A.j e. (0...N)A e. CC /\ A.k e. (0...N)B e. CC) -> sum_j e. (0...N)sum_k e. (0...(N - j))(A x. B) = sum_k e. (0...N)sum_j e. (0...k)(A x. [_(k - j) / k]_B))
2		fsumrev 7152	. . . . . . . . . 10 |- ((m e. (ZZ>` 0) /\ m e. ZZ /\ A.j e. (0...m)(A x. [_(m - j) / k]_B) e. CC) -> sum_j e. (0...m)(A x. [_(m - j) / k]_B) = sum_n e. ((m - m)...(m - 0))[_(m - n) / j]_(A x. [_(m - j) / k]_B))
3		elfzuz 6548	. . . . . . . . . . 11 |- (m e. (0...N) -> m e. (ZZ>` 0))
4	3	adantl 388	. . . . . . . . . 10 |- (((N e. NN0 /\ (A.j e. (0...N)A e. CC /\ A.k e. (0...N)B e. CC)) /\ m e. (0...N)) -> m e. (ZZ>` 0))
5		elfzelz 6542	. . . . . . . . . . 11 |- (m e. (0...N) -> m e. ZZ)
6	5	adantl 388	. . . . . . . . . 10 |- (((N e. NN0 /\ (A.j e. (0...N)A e. CC /\ A.k e. (0...N)B e. CC)) /\ m e. (0...N)) -> m e. ZZ)
7		elfzuz3 6538	. . . . . . . . . . . . . . . . . . 19 |- ((N e. NN0 /\ m e. (0...N)) -> N e. (ZZ>` m))
8		0z 6256	. . . . . . . . . . . . . . . . . . . 20 |- 0 e. ZZ
9		fzss2 6564	. . . . . . . . . . . . . . . . . . . 20 |- ((N e. (ZZ>` m) /\ 0 e. ZZ) -> (0...m) (_ (0...N))
10	8, 9	mpan2 699	. . . . . . . . . . . . . . . . . . 19 |- (N e. (ZZ>` m) -> (0...m) (_ (0...N))
11	7, 10	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((N e. NN0 /\ m e. (0...N)) -> (0...m) (_ (0...N))
12	11	sseld 2111	. . . . . . . . . . . . . . . . 17 |- ((N e. NN0 /\ m e. (0...N)) -> (j e. (0...m) -> j e. (0...N)))
13	12	imim1d 28	. . . . . . . . . . . . . . . 16 |- ((N e. NN0 /\ m e. (0...N)) -> ((j e. (0...N) -> A e. CC) -> (j e. (0...m) -> A e. CC)))
14	13	adantr 389	. . . . . . . . . . . . . . 15 |- (((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) -> ((j e. (0...N) -> A e. CC) -> (j e. (0...m) -> A e. CC)))
15		mulcl 5392	. . . . . . . . . . . . . . . . . . 19 |- ((A e. CC /\ [_(m - j) / k]_B e. CC) -> (A x. [_(m - j) / k]_B) e. CC)
16		ra4csbela 2086	. . . . . . . . . . . . . . . . . . . . 21 |- (((m - j) e. (0...N) /\ A.k e. (0...N)B e. CC) -> [_(m - j) / k]_B e. CC)
17	11	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- (((N e. NN0 /\ m e. (0...N)) /\ j e. (0...m)) -> (0...m) (_ (0...N))
18		visset 1851	. . . . . . . . . . . . . . . . . . . . . . . 24 |- m e. V
19		fznn0sub2 6559	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((m e. V /\ j e. (0...m)) -> (m - j) e. (0...m))
20	18, 19	mpan 698	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. (0...m) -> (m - j) e. (0...m))
21	20	adantl 388	. . . . . . . . . . . . . . . . . . . . . 22 |- (((N e. NN0 /\ m e. (0...N)) /\ j e. (0...m)) -> (m - j) e. (0...m))
22	17, 21	sseldd 2112	. . . . . . . . . . . . . . . . . . . . 21 |- (((N e. NN0 /\ m e. (0...N)) /\ j e. (0...m)) -> (m - j) e. (0...N))
23	16, 22	sylan 450	. . . . . . . . . . . . . . . . . . . 20 |- ((((N e. NN0 /\ m e. (0...N)) /\ j e. (0...m)) /\ A.k e. (0...N)B e. CC) -> [_(m - j) / k]_B e. CC)
24	23	an1rs 491	. . . . . . . . . . . . . . . . . . 19 |- ((((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) /\ j e. (0...m)) -> [_(m - j) / k]_B e. CC)
25	15, 24	sylan2 453	. . . . . . . . . . . . . . . . . 18 |- ((A e. CC /\ (((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) /\ j e. (0...m))) -> (A x. [_(m - j) / k]_B) e. CC)
26	25	exp32 377	. . . . . . . . . . . . . . . . 17 |- (A e. CC -> (((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) -> (j e. (0...m) -> (A x. [_(m - j) / k]_B) e. CC)))
27	26	com3l 34	. . . . . . . . . . . . . . . 16 |- (((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) -> (j e. (0...m) -> (A e. CC -> (A x. [_(m - j) / k]_B) e. CC)))
28	27	a2d 13	. . . . . . . . . . . . . . 15 |- (((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) -> ((j e. (0...m) -> A e. CC) -> (j e. (0...m) -> (A x. [_(m - j) / k]_B) e. CC)))
29	14, 28	syld 27	. . . . . . . . . . . . . 14 |- (((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) -> ((j e. (0...N) -> A e. CC) -> (j e. (0...m) -> (A x. [_(m - j) / k]_B) e. CC)))
30	29	r19.20dv2 1749	. . . . . . . . . . . . 13 |- (((N e. NN0 /\ m e. (0...N)) /\ A.k e. (0...N)B e. CC) -> (A.j e. (0...N)A e. CC -> A.j e. (0...m)(A x. [_(m - j) / k]_B) e. CC))
31	30	exp31 376	. . . . . . . . . . . 12 |- (N e. NN0 -> (m e. (0...N) -> (A.k e. (0...N)B e. CC -> (A.j e. (0...N)A e. CC -> A.j e. (0...m)(A x. [_(m - j) / k]_B) e. CC))))
32	31	com24 37	. . . . . . . . . . 11 |- (N e. NN0 -> (A.j e. (0...N)A e. CC -> (A.k e. (0...N)B e. CC -> (m e. (0...N) -> A.j e. (0...m)(A x. [_(m - j) / k]_B) e. CC))))
33	32	imp42 367	. . . . . . . . . 10 |- (((N e. NN0 /\ (A.j e. (0...N)A e. CC /\ A.k e. (0...N)B e. CC)) /\ m e. (0...N)) -> A.j e. (0...m)(A x. [_(m - j) / k]_B) e. CC)
34	2, 4, 6, 33	syl3anc 861	. . . . . . . . 9 |- (((N e. NN0 /\ (A.j e. (0...N)A e. CC /\ A.k e. (0...N)B e. CC)) /\ m e. (0...N)) -> sum_j e. (0...m)(A x. [_(m - j) / k]_B) = sum_n e. ((m - m)...(m - 0))[_(m - n) / j]_(A x. [_(m - j) / k]_B))
35		zcn 6250	. . . . . . . . . . . . . 14 |- (m e. ZZ -> m e. CC)
36	5, 35	syl 10	. . . . . . . . . . . . 13 |- (m e. (0...N) -> m e. CC)
37		subid 5484	. . . . . . . . . . . . . 14 |- (m e. CC -> (m - m) = 0)
38		subid1 5485	. . . . . . . . . . . . . 14 |- (m e. CC -> (m - 0) = m)
39	37, 38	opreq12d 4054	. . . . . . . . . . . . 13 |- (m e. CC -> ((m - m)...(m - 0)) = (0...m))
40	36, 39	syl 10	. . . . . . . . . . . 12 |- (m e. (0...N) -> ((m - m)...(m - 0)) = (0...m))
41	40	adantl 388	. . . . . . . . . . 11 |- ((N e. NN0 /\ m e. (0...N)) -> ((m - m)...(m - 0)) = (0...m))
42		nncan 5558	. . . . . . . . . . . . . . . 16 |- ((m e. CC /\ n e. CC) -> (m - (m - n)) = n)
43	18	elfzel2i 6539	. . . . . . . . . . . . . . . . 17 |- (n e. (0...m) -> m e. ZZ)
44	43, 35	syl 10	. . . . . . . . . . . . . . . 16 |- (n e. (0...m) -> m e. CC)
45		elfzelz 6542	. . . . . . . . . . . . . . . . 17 |- (n e. (0...m) -> n e. ZZ)
46		zcn 6250	. . . . . . . . . . . . . . . . 17 |- (n e. ZZ -> n e. CC)
47	45, 46	syl 10	. . . . . . . . . . . . . . . 16 |- (n e. (0...m) -> n e. CC)
48	42, 44, 47	sylanc 473	. . . . . . . . . . . . . . 15 |- (n e. (0...m) -> (m - (m - n)) = n)
49	48	csbeq1d 2047	. . . . . . . . . . . . . 14 |- (n e. (0...m) -> [_(m - (m - n)) / k]_B = [_n / k]_B)
50	49	opreq2d 4052	. . . . . . . . . . . . 13 |- (n e. (