Theorem fsum0diaglem2 7380

Description: Lemma for fsum0diag 7381 that provides its induction hypothesis. Warning: The HTML proof page is 0.8 megabyte in size.

Assertion

Ref	Expression
fsum0diaglem2	|- (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)) -> ((A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC) -> sum_j e. (0...(n + 1))sum_k e. (0...((n + 1) - j))(A x. B) = sum_k e. (0...(n + 1))sum_j e. (0...k)(A x. [_(k - j) / k]_B))))

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

Proof of Theorem fsum0diaglem2

Step	Hyp	Ref	Expression
1		elnn0uz 6501	. . . 4 |- (n e. NN0 <-> n e. (ZZ>` 0))
2		fsumcl 7138	. . . . . . . . . . . . . . . . . 18 |- (((n - j) e. (ZZ>` 0) /\ A.k e. (0...(n - j))(A x. B) e. CC) -> sum_k e. (0...(n - j))(A x. B) e. CC)
3		fznn0sub 6558	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (n - j) e. NN0)
4		nn0uz 6498	. . . . . . . . . . . . . . . . . . . 20 |- NN0 = (ZZ>` 0)
5	3, 4	syl6eleq 1595	. . . . . . . . . . . . . . . . . . 19 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (n - j) e. (ZZ>` 0))
6	5	ad2ant2r 409	. . . . . . . . . . . . . . . . . 18 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> (n - j) e. (ZZ>` 0))
7		fsum0diaglem1 7379	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (0...(n - j)) (_ (0...n))
8	7	sseld 2111	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (k e. (0...(n - j)) -> k e. (0...n)))
9		visset 1851	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- n e. V
10	9	fzelp1i 6569	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k e. (0...n) -> k e. (0...(n + 1)))
11	8, 10	syl6 22	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (k e. (0...(n - j)) -> k e. (0...(n + 1))))
12	11	adantrr 395	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>` 0) /\ (j e. (0...n) /\ A e. CC)) -> (k e. (0...(n - j)) -> k e. (0...(n + 1))))
13		mulcl 5392	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
14	13	ex 371	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. CC -> (B e. CC -> (A x. B) e. CC))
15	14	ad2antll 407	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>` 0) /\ (j e. (0...n) /\ A e. CC)) -> (B e. CC -> (A x. B) e. CC))
16	12, 15	imim12d 29	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. (ZZ>` 0) /\ (j e. (0...n) /\ A e. CC)) -> ((k e. (0...(n + 1)) -> B e. CC) -> (k e. (0...(n - j)) -> (A x. B) e. CC)))
17	16	r19.20dv2 1749	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. (ZZ>` 0) /\ (j e. (0...n) /\ A e. CC)) -> (A.k e. (0...(n + 1))B e. CC -> A.k e. (0...(n - j))(A x. B) e. CC))
18	17	imp 348	. . . . . . . . . . . . . . . . . . 19 |- (((n e. (ZZ>` 0) /\ (j e. (0...n) /\ A e. CC)) /\ A.k e. (0...(n + 1))B e. CC) -> A.k e. (0...(n - j))(A x. B) e. CC)
19	18	an1rs 491	. . . . . . . . . . . . . . . . . 18 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> A.k e. (0...(n - j))(A x. B) e. CC)
20	2, 6, 19	sylanc 473	. . . . . . . . . . . . . . . . 17 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> sum_k e. (0...(n - j))(A x. B) e. CC)
21		mulcl 5392	. . . . . . . . . . . . . . . . . 18 |- ((A e. CC /\ [_((n - j) + 1) / k]_B e. CC) -> (A x. [_((n - j) + 1) / k]_B) e. CC)
22		simprr 415	. . . . . . . . . . . . . . . . . 18 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> A e. CC)
23		ra4csbela 2086	. . . . . . . . . . . . . . . . . . . . 21 |- ((((n - j) + 1) e. (0...(n + 1)) /\ A.k e. (0...(n + 1))B e. CC) -> [_((n - j) + 1) / k]_B e. CC)
24		ax1cn 5358	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. CC
25		addsub 5473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((n e. CC /\ 1 e. CC /\ j e. CC) -> ((n + 1) - j) = ((n - j) + 1))
26	24, 25	mp3an2 907	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((n e. CC /\ j e. CC) -> ((n + 1) - j) = ((n - j) + 1))
27		eluzelz 6483	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n e. (ZZ>` 0) -> n e. ZZ)
28		zcn 6250	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n e. ZZ -> n e. CC)
29	27, 28	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. (ZZ>` 0) -> n e. CC)
30		elfzelz 6542	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. (0...n) -> j e. ZZ)
31		zcn 6250	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. ZZ -> j e. CC)
32	30, 31	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. (0...n) -> j e. CC)
33	26, 29, 32	syl2an 456	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> ((n + 1) - j) = ((n - j) + 1))
34		fznn0sub2 6559	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((n + 1) e. (ZZ>` 0) /\ j e. (0...(n + 1))) -> ((n + 1) - j) e. (0...(n + 1)))
35		peano2uz 6507	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. (ZZ>` 0) -> (n + 1) e. (ZZ>` 0))
36	9	fzelp1i 6569	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. (0...n) -> j e. (0...(n + 1)))
37	34, 35, 36	syl2an 456	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> ((n + 1) - j) e. (0...(n + 1)))
38	33, 37	eqeltrrd 1586	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> ((n - j) + 1) e. (0...(n + 1)))
39	23, 38	sylan 450	. . . . . . . . . . . . . . . . . . . 20 |- (((n e. (ZZ>` 0) /\ j e. (0...n)) /\ A.k e. (0...(n + 1))B e. CC) -> [_((n - j) + 1) / k]_B e. CC)
40	39	an1rs 491	. . . . . . . . . . . . . . . . . . 19 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ j e. (0...n)) -> [_((n - j) + 1) / k]_B e. CC)
41	40	adantrr 395	. . . . . . . . . . . . . . . . . 18 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> [_((n - j) + 1) / k]_B e. CC)
42	21, 22, 41	sylanc 473	. . . . . . . . . . . . . . . . 17 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> (A x. [_((n - j) + 1) / k]_B) e. CC)
43	20, 42	jca 286	. . . . . . . . . . . . . . . 16 |- (((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> (sum_k e. (0...(n - j))(A x. B) e. CC /\ (A x. [_((n - j) + 1) / k]_B) e. CC))
44	43	exp32 377	. . . . . . . . . . . . . . 15 |- ((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) -> (j e. (0...n) -> (A e. CC -> (sum_k e. (0...(n - j))(A x. B) e. CC /\ (A x. [_((n - j) + 1) / k]_B) e. CC))))
45	44	a2d 13	. . . . . . . . . . . . . 14 |- ((n e. (ZZ>` 0) /\ A.k e. (0...(n + 1))B e. CC) -> ((j e. (0...n) -> A e. CC) -> (j e. (0...n) -> (sum_k e. (0...(n - j))(A x. B) e. CC /\ (A x. [_((n - j) + 1) / k]_B) e. CC))))
46	36	imim1i 16	. . . . . . . . . . . . . 14 |- ((j e. (0...(n + 1)) -> A e. CC) -> (j e. (0...n) -> A e. CC))
47	45, 46