Theorem fsum0diag4 7196

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

Assertion

Ref	Expression
fsum0diag4	|- ((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)(B x. sum_j e. (0...(N - k))A))

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

Proof of Theorem fsum0diag4

Step	Hyp	Ref	Expression
1		elfzuz3t 6410	. . . . . . . . . . . . . . . . 17 |- ((N e. NN0 /\ m e. (0...N)) -> N e. (ZZ>` m))
2		0z 6093	. . . . . . . . . . . . . . . . . 18 |- 0 e. ZZ
3		fzss2t 6436	. . . . . . . . . . . . . . . . . 18 |- ((N e. (ZZ>` m) /\ 0 e. ZZ) -> (0...m) (_ (0...N))
4	2, 3	mpan2 694	. . . . . . . . . . . . . . . . 17 |- (N e. (ZZ>` m) -> (0...m) (_ (0...N))
5	1, 4	syl 10	. . . . . . . . . . . . . . . 16 |- ((N e. NN0 /\ m e. (0...N)) -> (0...m) (_ (0...N))
6	5	sseld 2057	. . . . . . . . . . . . . . 15 |- ((N e. NN0 /\ m e. (0...N)) -> (k e. (0...m) -> k e. (0...N)))
7	6	imim1d 28	. . . . . . . . . . . . . 14 |- ((N e. NN0 /\ m e. (0...N)) -> ((k e. (0...N) -> B e. CC) -> (k e. (0...m) -> B e. CC)))
8	7	adantlr 393	. . . . . . . . . . . . 13 |- (((N e. NN0 /\ A.j e. (0...N)A e. CC) /\ m e. (0...N)) -> ((k e. (0...N) -> B e. CC) -> (k e. (0...m) -> B e. CC)))
9		axmulcom 5248	. . . . . . . . . . . . . . . 16 |- (([_(m - k) / j]_A e. CC /\ B e. CC) -> ([_(m - k) / j]_A x. B) = (B x. [_(m - k) / j]_A))
10		ra4csbela 2032	. . . . . . . . . . . . . . . . . . . . 21 |- (((m - k) e. (0...N) /\ A.j e. (0...N)A e. CC) -> [_(m - k) / j]_A e. CC)
11		elfzle2 6416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (k e. (0...m) -> k <_ m)
12	11	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. (0...N) /\ k e. (0...m)) -> k <_ m)
13		subge0t 5647	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. RR /\ k e. RR) -> (0 <_ (m - k) <-> k <_ m))
14		elfzelz 6414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. (0...N) -> m e. ZZ)
15		zret 6086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (m e. ZZ -> m e. RR)
16	14, 15	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (m e. (0...N) -> m e. RR)
17		elfzelz 6414	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (k e. (0...m) -> k e. ZZ)
18		zret 6086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (k e. ZZ -> k e. RR)
19	17, 18	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (k e. (0...m) -> k e. RR)
20	13, 16, 19	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. (0...N) /\ k e. (0...m)) -> (0 <_ (m - k) <-> k <_ m))
21	12, 20	mpbird 196	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((m e. (0...N) /\ k e. (0...m)) -> 0 <_ (m - k))
22	21	adantll 392	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> 0 <_ (m - k))
23		zsubclt 6115	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. ZZ /\ k e. ZZ) -> (m - k) e. ZZ)
24	23, 14, 17	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. (0...N) /\ k e. (0...m)) -> (m - k) e. ZZ)
25		zret 6086	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m - k) e. ZZ -> (m - k) e. RR)
26	24, 25	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. (0...N) /\ k e. (0...m)) -> (m - k) e. RR)
27	26	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> (m - k) e. RR)
28	16	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> m e. RR)
29		nn0ret 6055	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (N e. NN0 -> N e. RR)
30	29	ad2antrr 404	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> N e. RR)
31		elfzle1 6415	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (k e. (0...m) -> 0 <_ k)
32	31	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. (0...N) /\ k e. (0...m)) -> 0 <_ k)
33		subge02t 5650	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((m e. RR /\ k e. RR) -> (0 <_ k <-> (m - k) <_ m))
34	33, 16, 19	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((m e. (0...N) /\ k e. (0...m)) -> (0 <_ k <-> (m - k) <_ m))
35	32, 34	mpbid 195	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((m e. (0...N) /\ k e. (0...m)) -> (m - k) <_ m)
36	35	adantll 392	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> (m - k) <_ m)
37		elfzle2 6416	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (m e. (0...N) -> m <_ N)
38	37	ad2antlr 405	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> m <_ N)
39	27, 28, 30, 36, 38	letrd 5499	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> (m - k) <_ N)
40	22, 39	jca 288	. . . . . . . . . . . . . . . . . . . . . 22 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> (0 <_ (m - k) /\ (m - k) <_ N))
41		elfzt 6403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((m - k) e. ZZ /\ 0 e. ZZ /\ N e. ZZ) -> ((m - k) e. (0...N) <-> (0 <_ (m - k) /\ (m - k) <_ N)))
42	2, 41	mp3an2 901	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((m - k) e. ZZ /\ N e. ZZ) -> ((m - k) e. (0...N) <-> (0 <_ (m - k) /\ (m - k) <_ N)))
43		nn0zt 6101	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (N e. NN0 -> N e. ZZ)
44	42, 24, 43	syl2an 454	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((m e. (0...N) /\ k e. (0...m)) /\ N e. NN0) -> ((m - k) e. (0...N) <-> (0 <_ (m - k) /\ (m - k) <_ N)))
45	44	ancoms 436	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((N e. NN0 /\ (m e. (0...N) /\ k e. (0...m))) -> ((m - k) e. (0...N) <-> (0 <_ (m - k) /\ (m - k) <_ N)))
46	45	anassrs 441	. . . . . . . . . . . . . . . . . . . . . 22 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> ((m - k) e. (0...N) <-> (0 <_ (m - k) /\ (m - k) <_ N)))
47	40, 46	mpbird 196	. . . . . . . . . . . . . . . . . . . . 21 |- (((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) -> (m - k) e. (0...N))
48	10, 47	sylan 448	. . . . . . . . . . . . . . . . . . . 20 |- ((((N e. NN0 /\ m e. (0...N)) /\ k e. (0...m)) /\ A.j e. (0...N)A e. CC) -> [_(m - k) / j]_A e. CC)
49	48	exp41 382	. . . . . . . . . . . . . . . . . . 19 |- (N e. NN0 -> (m e. (0...N) -> (k e. (0...m) -> (A.j e. (0...N)A e. CC -> [_(m - k) / j]_A e. CC))))
50	49	com23 32	. . . . . . . . . . . . . . . . . 18 |- (N e. NN0 -> (k e. (0...m) -> (m e. (0...N) -> (A.j e. (0...N)A e. CC -> [_(m - k) / j]_A e. CC))))
51	50	com24 37	. . . . . . . . . . . . . . . . 17 |- (N e. NN0 -> (A.j e. (0...N)A e. CC -> (m e. (0...N) -> (k e. (0...m) -> [_(m - k) / j]_A e. CC))))
52	51	imp41 368	. . . . . . . . . . . . . . . 16 |- ((((N e. NN0 /\ A.j e. (0...N)A e. CC) /\ m e. (0...N)) /\ k e. (0...m)) -> [_(m - k) / j]_A e. CC)
53	9, 52	sylan 448	. . . . . . . . . . . . . . 15 |- (((((N e. NN0 /\ A.j e. (0...N)A e. CC) /\ m e. (0...N)) /\ k e. (0...m)) /\ B e. CC) -> ([_(m - k) / j]_A x. B) = (B x. [_(m - k) / j]_A))
54	53	exp31 376	. . . . . . . . . . . . . 14 |- (((N e. NN0 /\ A.j e. (0...N)A e. CC) /\ m e. (0...N)) -> (k e. (0...m) -> (B e. CC -> ([_(m - k) / j]_A x. B) = (B x. [_(m - k) / j]_A))))
55	54	a2d 13	. . . . . . . . . . . . 13 |- (((N e. NN0 /\ A.j e. (0...N)A e. CC) /\ m e. (0...N)) -> ((k e. (0...m) -> B e. CC) -> (k e. (0...m) -> ([_(m - k) / j]_A x. B) = (B x. [_(m - k) / j]_A))))
56	8, 55	syld 27	. . . . . . . . . . . 12 |- (((N e. NN0 /\ A.j e. (0...N)A e. CC) /\ m e. (