Theorem fsum0diaglem2 7209

Description: Lemma for fsum0diag 7210 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 6386	. . . 4 |- (n e. NN0 <-> n e. (ZZ>` 0))
2		fsumclt 6968	. . . . . . . . . . . . . . . . . 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		fznn0subt 6443	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (n - j) e. NN0)
4		nn0uz 6383	. . . . . . . . . . . . . . . . . . . 20 |- NN0 = (ZZ>` 0)
5	3, 4	syl6eleq 1556	. . . . . . . . . . . . . . . . . . 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 7208	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (0...(n - j)) (_ (0...n))
8	7	sseld 2064	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> (k e. (0...(n - j)) -> k e. (0...n)))
9		visset 1810	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- n e. V
10	9	fzelp1 6454	. . . . . . . . . . . . . . . . . . . . . . . 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		axmulcl 5256	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
14	13	ex 373	. . . . . . . . . . . . . . . . . . . . . . 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 1709	. . . . . . . . . . . . . . . . . . . 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 350	. . . . . . . . . . . . . . . . . . 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 489	. . . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . . 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		axmulcl 5256	. . . . . . . . . . . . . . . . . 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 2039	. . . . . . . . . . . . . . . . . . . . 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 5252	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. CC
25		addsubt 5367	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((n e. CC /\ 1 e. CC /\ j e. CC) -> ((n + 1) - j) = ((n - j) + 1))
26	24, 25	mp3an2 903	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((n e. CC /\ j e. CC) -> ((n + 1) - j) = ((n - j) + 1))
27		eluzelz 6368	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n e. (ZZ>` 0) -> n e. ZZ)
28		zcnt 6097	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n e. ZZ -> n e. CC)
29	27, 28	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. (ZZ>` 0) -> n e. CC)
30		elfzelz 6427	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. (0...n) -> j e. ZZ)
31		zcnt 6097	. . . . . . . . . . . . . . . . . . . . . . . 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 454	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> ((n + 1) - j) = ((n - j) + 1))
34		fznn0sub2t 6444	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((n + 1) e. (ZZ>` 0) /\ j e. (0...(n + 1))) -> ((n + 1) - j) e. (0...(n + 1)))
35		peano2uz 6392	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. (ZZ>` 0) -> (n + 1) e. (ZZ>` 0))
36	9	fzelp1 6454	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. (0...n) -> j e. (0...(n + 1)))
37	34, 35, 36	syl2an 454	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> ((n + 1) - j) e. (0...(n + 1)))
38	33, 37	eqeltrrd 1547	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. (ZZ>` 0) /\ j e. (0...n)) -> ((n - j) + 1) e. (0...(n + 1)))
39	23, 38	sylan 448	. . . . . . . . . . . . . . . . . . . 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 489	. . . . . . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . . . . . 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 288	. . . . . . . . . . . . . . . 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