Theorem fsum0diaglem2 8519

Description: Lemma for fsum0diag 8520 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 7610	. . . 4 |- (n e. NN0 <-> n e. (ZZ>=` 0))
2		fznn0sub 7670	. . . . . . . . . . . . . . . . . . . 20 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> (n - j) e. NN0)
3		nn0uz 7607	. . . . . . . . . . . . . . . . . . . 20 |- NN0 = (ZZ>=` 0)
4	2, 3	syl6eleq 1981	. . . . . . . . . . . . . . . . . . 19 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> (n - j) e. (ZZ>=` 0))
5	4	ad2ant2r 445	. . . . . . . . . . . . . . . . . 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))
6		fsum0diaglem1 8518	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> (0...(n - j)) C_ (0...n))
7	6	sseld 2619	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> (k e. (0...(n - j)) -> k e. (0...n)))
8		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- n e. _V
9	8	fzelp1i 7682	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k e. (0...n) -> k e. (0...(n + 1)))
10	7, 9	syl6 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> (k e. (0...(n - j)) -> k e. (0...(n + 1))))
11	10	adantrr 431	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>=` 0) /\ (j e. (0...n) /\ A e. CC)) -> (k e. (0...(n - j)) -> k e. (0...(n + 1))))
12		mulcl 6456	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
13	12	ex 402	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A e. CC -> (B e. CC -> (A x. B) e. CC))
14	13	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>=` 0) /\ (j e. (0...n) /\ A e. CC)) -> (B e. CC -> (A x. B) e. CC))
15	11, 14	imim12d 69	. . . . . . . . . . . . . . . . . . . . 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)))
16	15	ralimdv2 2173	. . . . . . . . . . . . . . . . . . . 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))
17	16	imp 377	. . . . . . . . . . . . . . . . . . 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)
18	17	an1rs 547	. . . . . . . . . . . . . . . . . 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)
19		fsumcl 8275	. . . . . . . . . . . . . . . . . 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)
20	5, 18, 19	syl11anc 524	. . . . . . . . . . . . . . . . 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		simprr 451	. . . . . . . . . . . . . . . . . 18 |- (((n e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC) /\ (j e. (0...n) /\ A e. CC)) -> A e. CC)
22		ra4csbela 2587	. . . . . . . . . . . . . . . . . . . . 21 |- ((((n - j) + 1) e. (0...(n + 1)) /\ A.k e. (0...(n + 1))B e. CC) -> [_((n - j) + 1) / k]_B e. CC)
23		ax1cn 6422	. . . . . . . . . . . . . . . . . . . . . . . 24 |- 1 e. CC
24		addsub 6542	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((n e. CC /\ 1 e. CC /\ j e. CC) -> ((n + 1) - j) = ((n - j) + 1))
25	23, 24	mp3an2 1179	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((n e. CC /\ j e. CC) -> ((n + 1) - j) = ((n - j) + 1))
26		eluzelz 7592	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n e. (ZZ>=` 0) -> n e. ZZ)
27		zcn 7349	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (n e. ZZ -> n e. CC)
28	26, 27	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. (ZZ>=` 0) -> n e. CC)
29		elfzelz 7652	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. (0...n) -> j e. ZZ)
30		zcn 7349	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (j e. ZZ -> j e. CC)
31	29, 30	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. (0...n) -> j e. CC)
32	25, 28, 31	syl2an 503	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> ((n + 1) - j) = ((n - j) + 1))
33		fznn0sub2 7671	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((n + 1) e. (ZZ>=` 0) /\ j e. (0...(n + 1))) -> ((n + 1) - j) e. (0...(n + 1)))
34		peano2uz 7616	. . . . . . . . . . . . . . . . . . . . . . 23 |- (n e. (ZZ>=` 0) -> (n + 1) e. (ZZ>=` 0))
35	8	fzelp1i 7682	. . . . . . . . . . . . . . . . . . . . . . 23 |- (j e. (0...n) -> j e. (0...(n + 1)))
36	33, 34, 35	syl2an 503	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> ((n + 1) - j) e. (0...(n + 1)))
37	32, 36	eqeltrrd 1972	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> ((n - j) + 1) e. (0...(n + 1)))
38	22, 37	sylan 497	. . . . . . . . . . . . . . . . . . . 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)
39	38	an1rs 547	. . . . . . . . . . . . . . . . . . 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)
40	39	adantrr 431	. . . . . . . . . . . . . . . . . 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)
41		mulcl 6456	. . . . . . . . . . . . . . . . . 18 |- ((A e. CC /\ [_((n - j) + 1) / k]_B e. CC) -> (A x. [_((n - j) + 1) / k]_B) e. CC)
42	21, 40, 41	syl11anc 524	. . . . . . . . . . . . . . . . 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 310	. . . . . . . . . . . . . . . 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 408	. . . . . . . . . . . . . . 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 16	. . . . . . . . . . . . . 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	35	imim1i 19	. . . . . . . . . . . . . 14 |- ((j e. (0...(n + 1)) -> A e. CC) -> (j e. (0...n) -> A e. CC))
47	45, 46	syl5 20	. . . . . . . . . . . . 13 |- ((n e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC) -> ((j e. (0...(n + 1)) -> 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))))
48	47	ralimdv2 2173	. . . . . . . . . . . 12 |- ((n e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC) -> (A.j e. (0...(n + 1))A e. CC -> A.j e. (0...n)(sum_k e. (0...(n - j))(A x. B) e. CC /\ (A x. [_((n - j) + 1) / k]_B) e. CC)))
49	48	impcom 378	. . . . . . . . . . 11 |- ((A.j e. (0...(n + 1))A e. CC /\ (n e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC)) -> A.j e. (0...n)(sum_k e. (0...(n - j))(A x. B) e. CC /\ (A x. [_((n - j) + 1) / k]_B) e. CC))
50	49	an1s 544	. . . . . . . . . 10 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> A.j e. (0...n)(sum_k e. (0...(n - j))(A x. B) e. CC /\ (A x. [_((n - j) + 1) / k]_B) e. CC))
51		fsumadd 8282	. . . . . . . . . 10 |- ((n e. (ZZ>=` 0) /\ A.j e. (0...n)(sum_k e. (0...(n - j))(A x. B) e. CC /\ (A x. [_((n - j) + 1) / k]_B) e. CC)) -> sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) = (sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B)))
52	50, 51	syldan 516	. . . . . . . . 9 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) = (sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B)))
53	52	opreq1d 4897	. . . . . . . 8 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> (sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)) = ((sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)))
54		fsumcl 8275	. . . . . . . . . 10 |- ((n e. (ZZ>=` 0) /\ A.j e. (0...n)sum_k e. (0...(n - j))(A x. B) e. CC) -> sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) e. CC)
55		fznn0sub 7670	. . . . . . . . . . . . . . . . . 18 |- ((n e. _V /\ j e. (0...n)) -> (n - j) e. NN0)
56	8, 55	mpan 759	. . . . . . . . . . . . . . . . 17 |- (j e. (0...n) -> (n - j) e. NN0)
57	56, 3	syl6eleq 1981	. . . . . . . . . . . . . . . 16 |- (j e. (0...n) -> (n - j) e. (ZZ>=` 0))
58	57	ad2antlr 441	. . . . . . . . . . . . . . 15 |- (((A.k e. (0...n)B e. CC /\ j e. (0...n)) /\ A e. CC) -> (n - j) e. (ZZ>=` 0))
59		fsum0diaglem1 8518	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((n e. _V /\ j e. (0...n)) -> (0...(n - j)) C_ (0...n))
60	8, 59	mpan 759	. . . . . . . . . . . . . . . . . . . . . 22 |- (j e. (0...n) -> (0...(n - j)) C_ (0...n))
61	60	sseld 2619	. . . . . . . . . . . . . . . . . . . . 21 |- (j e. (0...n) -> (k e. (0...(n - j)) -> k e. (0...n)))
62	61	imim1d 33	. . . . . . . . . . . . . . . . . . . 20 |- (j e. (0...n) -> ((k e. (0...n) -> B e. CC) -> (k e. (0...(n - j)) -> B e. CC)))
63	62	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((j e. (0...n) /\ A e. CC) -> ((k e. (0...n) -> B e. CC) -> (k e. (0...(n - j)) -> B e. CC)))
64	13	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((j e. (0...n) /\ A e. CC) -> (B e. CC -> (A x. B) e. CC))
65	63, 64	syl6d 67	. . . . . . . . . . . . . . . . . 18 |- ((j e. (0...n) /\ A e. CC) -> ((k e. (0...n) -> B e. CC) -> (k e. (0...(n - j)) -> (A x. B) e. CC)))
66	65	ralimdv2 2173	. . . . . . . . . . . . . . . . 17 |- ((j e. (0...n) /\ A e. CC) -> (A.k e. (0...n)B e. CC -> A.k e. (0...(n - j))(A x. B) e. CC))
67	66	impcom 378	. . . . . . . . . . . . . . . 16 |- ((A.k e. (0...n)B e. CC /\ (j e. (0...n) /\ A e. CC)) -> A.k e. (0...(n - j))(A x. B) e. CC)
68	67	anassrs 489	. . . . . . . . . . . . . . 15 |- (((A.k e. (0...n)B e. CC /\ j e. (0...n)) /\ A e. CC) -> A.k e. (0...(n - j))(A x. B) e. CC)
69	58, 68, 19	syl11anc 524	. . . . . . . . . . . . . 14 |- (((A.k e. (0...n)B e. CC /\ j e. (0...n)) /\ A e. CC) -> sum_k e. (0...(n - j))(A x. B) e. CC)
70	69	ex 402	. . . . . . . . . . . . 13 |- ((A.k e. (0...n)B e. CC /\ j e. (0...n)) -> (A e. CC -> sum_k e. (0...(n - j))(A x. B) e. CC))
71	70	ralimdvaa 2171	. . . . . . . . . . . 12 |- (A.k e. (0...n)B e. CC -> (A.j e. (0...n)A e. CC -> A.j e. (0...n)sum_k e. (0...(n - j))(A x. B) e. CC))
72	71	impcom 378	. . . . . . . . . . 11 |- ((A.j e. (0...n)A e. CC /\ A.k e. (0...n)B e. CC) -> A.j e. (0...n)sum_k e. (0...(n - j))(A x. B) e. CC)
73	46	ralimi2 2165	. . . . . . . . . . 11 |- (A.j e. (0...(n + 1))A e. CC -> A.j e. (0...n)A e. CC)
74	9	imim1i 19	. . . . . . . . . . . 12 |- ((k e. (0...(n + 1)) -> B e. CC) -> (k e. (0...n) -> B e. CC))
75	74	ralimi2 2165	. . . . . . . . . . 11 |- (A.k e. (0...(n + 1))B e. CC -> A.k e. (0...n)B e. CC)
76	72, 73, 75	syl2an 503	. . . . . . . . . 10 |- ((A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC) -> A.j e. (0...n)sum_k e. (0...(n - j))(A x. B) e. CC)
77	54, 76	sylan2 500	. . . . . . . . 9 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) e. CC)
78	42	exp32 408	. . . . . . . . . . . . . . 15 |- ((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)))
79	78	a2d 16	. . . . . . . . . . . . . 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) -> (A x. [_((n - j) + 1) / k]_B) e. CC)))
80	79, 46	syl5 20	. . . . . . . . . . . . 13 |- ((n e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC) -> ((j e. (0...(n + 1)) -> A e. CC) -> (j e. (0...n) -> (A x. [_((n - j) + 1) / k]_B) e. CC)))
81	80	ralimdv2 2173	. . . . . . . . . . . 12 |- ((n e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC) -> (A.j e. (0...(n + 1))A e. CC -> A.j e. (0...n)(A x. [_((n - j) + 1) / k]_B) e. CC))
82	81	impcom 378	. . . . . . . . . . 11 |- ((A.j e. (0...(n + 1))A e. CC /\ (n e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC)) -> A.j e. (0...n)(A x. [_((n - j) + 1) / k]_B) e. CC)
83	82	an1s 544	. . . . . . . . . 10 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> A.j e. (0...n)(A x. [_((n - j) + 1) / k]_B) e. CC)
84		fsumcl 8275	. . . . . . . . . 10 |- ((n e. (ZZ>=` 0) /\ A.j e. (0...n)(A x. [_((n - j) + 1) / k]_B) e. CC) -> sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) e. CC)
85	83, 84	syldan 516	. . . . . . . . 9 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) e. CC)
86		ra4csbela 2587	. . . . . . . . . . . . . 14 |- (((n + 1) e. (0...(n + 1)) /\ A.j e. (0...(n + 1))A e. CC) -> [_(n + 1) / j]_A e. CC)
87		eluzfz2 7659	. . . . . . . . . . . . . 14 |- ((n + 1) e. (ZZ>=` 0) -> (n + 1) e. (0...(n + 1)))
88	86, 87	sylan 497	. . . . . . . . . . . . 13 |- (((n + 1) e. (ZZ>=` 0) /\ A.j e. (0...(n + 1))A e. CC) -> [_(n + 1) / j]_A e. CC)
89		ra4csbela 2587	. . . . . . . . . . . . . 14 |- ((0 e. (0...(n + 1)) /\ A.k e. (0...(n + 1))B e. CC) -> [_0 / k]_B e. CC)
90		eluzfz1 7657	. . . . . . . . . . . . . 14 |- ((n + 1) e. (ZZ>=` 0) -> 0 e. (0...(n + 1)))
91	89, 90	sylan 497	. . . . . . . . . . . . 13 |- (((n + 1) e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC) -> [_0 / k]_B e. CC)
92	88, 91	anim12i 360	. . . . . . . . . . . 12 |- ((((n + 1) e. (ZZ>=` 0) /\ A.j e. (0...(n + 1))A e. CC) /\ ((n + 1) e. (ZZ>=` 0) /\ A.k e. (0...(n + 1))B e. CC)) -> ([_(n + 1) / j]_A e. CC /\ [_0 / k]_B e. CC))
93	92	anandis 570	. . . . . . . . . . 11 |- (((n + 1) e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> ([_(n + 1) / j]_A e. CC /\ [_0 / k]_B e. CC))
94	93, 34	sylan 497	. . . . . . . . . 10 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> ([_(n + 1) / j]_A e. CC /\ [_0 / k]_B e. CC))
95		mulcl 6456	. . . . . . . . . 10 |- (([_(n + 1) / j]_A e. CC /\ [_0 / k]_B e. CC) -> ([_(n + 1) / j]_A x. [_0 / k]_B) e. CC)
96	94, 95	syl 12	. . . . . . . . 9 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> ([_(n + 1) / j]_A x. [_0 / k]_B) e. CC)
97		addass 6460	. . . . . . . . 9 |- ((sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) e. CC /\ sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) e. CC /\ ([_(n + 1) / j]_A x. [_0 / k]_B) e. CC) -> ((sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)) = (sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
98	77, 85, 96, 97	syl111anc 1100	. . . . . . . 8 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> ((sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)) = (sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
99	53, 98	eqtrd 1925	. . . . . . 7 |- ((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC)) -> (sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)) = (sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
100		opreq1 4889	. . . . . . 7 |- (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) -> (sum_j e. (0...n)sum_k e. (0...(n - j))(A x. B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))) = (sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
101	99, 100	sylan9eq 1948	. . . . . 6 |- (((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))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)) -> (sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)) = (sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
102		sumex 8241	. . . . . . . . 9 |- sum_k e. (0...((n + 1) - j))(A x. B) e. _V
103		sumex 8241	. . . . . . . . 9 |- sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B) e. _V
104		ax-17 1317	. . . . . . . . . 10 |- (m e. (0...((n + 1) - (n + 1))) -> A.j m e. (0...((n + 1) - (n + 1))))
105		oprex 4907	. . . . . . . . . . . 12 |- (n + 1) e. _V
106		ax-17 1317	. . . . . . . . . . . 12 |- (m e. (n + 1) -> A.j m e. (n + 1))
107	105, 106	hbcsb1 2568	. . . . . . . . . . 11 |- (m e. [_(n + 1) / j]_A -> A.j m e. [_(n + 1) / j]_A)
108		ax-17 1317	. . . . . . . . . . 11 |- (m e. x. -> A.j m e. x. )
109		ax-17 1317	. . . . . . . . . . 11 |- (m e. B -> A.j m e. B)
110	107, 108, 109	hbopr 4904	. . . . . . . . . 10 |- (m e. ([_(n + 1) / j]_A x. B) -> A.j m e. ([_(n + 1) / j]_A x. B))
111	104, 110	hbsum 8244	. . . . . . . . 9 |- (m e. sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B) -> A.j m e. sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B))
112		opreq2 4890	. . . . . . . . . . 11 |- (j = (n + 1) -> ((n + 1) - j) = ((n + 1) - (n + 1)))
113	112	opreq2d 4898	. . . . . . . . . 10 |- (j = (n + 1) -> (0...((n + 1) - j)) = (0...((n + 1) - (n + 1))))
114		csbeq1a 2546	. . . . . . . . . . . 12 |- (j = (n + 1) -> A = [_(n + 1) / j]_A)
115	114	opreq1d 4897	. . . . . . . . . . 11 |- (j = (n + 1) -> (A x. B) = ([_(n + 1) / j]_A x. B))
116	115	adantr 425	. . . . . . . . . 10 |- ((j = (n + 1) /\ k e. (0...((n + 1) - (n + 1)))) -> (A x. B) = ([_(n + 1) / j]_A x. B))
117	113, 116	sumeq12rdv 8256	. . . . . . . . 9 |- (j = (n + 1) -> sum_k e. (0...((n + 1) - j))(A x. B) = sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B))
118	102, 103, 111, 117	fsump1fi 8271	. . . . . . . 8 |- (n e. (ZZ>=` 0) -> sum_j e. (0...(n + 1))sum_k e. (0...((n + 1) - j))(A x. B) = (sum_j e. (0...n)sum_k e. (0...((n + 1) - j))(A x. B) + sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B)))
119	25	opreq2d 4898	. . . . . . . . . . . . 13 |- ((n e. CC /\ j e. CC) -> (0...((n + 1) - j)) = (0...((n - j) + 1)))
120	119	sumeq1d 8250	. . . . . . . . . . . 12 |- ((n e. CC /\ j e. CC) -> sum_k e. (0...((n + 1) - j))(A x. B) = sum_k e. (0...((n - j) + 1))(A x. B))
121	120, 28, 31	syl2an 503	. . . . . . . . . . 11 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> sum_k e. (0...((n + 1) - j))(A x. B) = sum_k e. (0...((n - j) + 1))(A x. B))
122		oprex 4907	. . . . . . . . . . . . 13 |- (A x. B) e. _V
123		oprex 4907	. . . . . . . . . . . . 13 |- (A x. [_((n - j) + 1) / k]_B) e. _V
124		ax-17 1317	. . . . . . . . . . . . . 14 |- (m e. A -> A.k m e. A)
125		ax-17 1317	. . . . . . . . . . . . . 14 |- (m e. x. -> A.k m e. x. )
126		oprex 4907	. . . . . . . . . . . . . . 15 |- ((n - j) + 1) e. _V
127		ax-17 1317	. . . . . . . . . . . . . . 15 |- (m e. ((n - j) + 1) -> A.k m e. ((n - j) + 1))
128	126, 127	hbcsb1 2568	. . . . . . . . . . . . . 14 |- (m e. [_((n - j) + 1) / k]_B -> A.k m e. [_((n - j) + 1) / k]_B)
129	124, 125, 128	hbopr 4904	. . . . . . . . . . . . 13 |- (m e. (A x. [_((n - j) + 1) / k]_B) -> A.k m e. (A x. [_((n - j) + 1) / k]_B))
130		csbeq1a 2546	. . . . . . . . . . . . . 14 |- (k = ((n - j) + 1) -> B = [_((n - j) + 1) / k]_B)
131	130	opreq2d 4898	. . . . . . . . . . . . 13 |- (k = ((n - j) + 1) -> (A x. B) = (A x. [_((n - j) + 1) / k]_B))
132	122, 123, 129, 131	fsump1fi 8271	. . . . . . . . . . . 12 |- ((n - j) e. (ZZ>=` 0) -> sum_k e. (0...((n - j) + 1))(A x. B) = (sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)))
133	4, 132	syl 12	. . . . . . . . . . 11 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> sum_k e. (0...((n - j) + 1))(A x. B) = (sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)))
134	121, 133	eqtrd 1925	. . . . . . . . . 10 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> sum_k e. (0...((n + 1) - j))(A x. B) = (sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)))
135	134	sumeq2dv 8252	. . . . . . . . 9 |- (n e. (ZZ>=` 0) -> sum_j e. (0...n)sum_k e. (0...((n + 1) - j))(A x. B) = sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)))
136		peano2cn 6498	. . . . . . . . . . . . . 14 |- (n e. CC -> (n + 1) e. CC)
137	28, 136	syl 12	. . . . . . . . . . . . 13 |- (n e. (ZZ>=` 0) -> (n + 1) e. CC)
138		subid 6555	. . . . . . . . . . . . 13 |- ((n + 1) e. CC -> ((n + 1) - (n + 1)) = 0)
139	137, 138	syl 12	. . . . . . . . . . . 12 |- (n e. (ZZ>=` 0) -> ((n + 1) - (n + 1)) = 0)
140	139	opreq2d 4898	. . . . . . . . . . 11 |- (n e. (ZZ>=` 0) -> (0...((n + 1) - (n + 1))) = (0...0))
141	140	sumeq1d 8250	. . . . . . . . . 10 |- (n e. (ZZ>=` 0) -> sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B) = sum_k e. (0...0)([_(n + 1) / j]_A x. B))
142		ax-17 1317	. . . . . . . . . . . . 13 |- (m e. [_(n + 1) / j]_A -> A.k m e. [_(n + 1) / j]_A)
143		0z 7355	. . . . . . . . . . . . . 14 |- 0 e. ZZ
144		ax-17 1317	. . . . . . . . . . . . . . 15 |- (m e. 0 -> A.k m e. 0)
145	144	hbcsb1g 2567	. . . . . . . . . . . . . 14 |- (0 e. ZZ -> (m e. [_0 / k]_B -> A.k m e. [_0 / k]_B))
146	143, 145	ax-mp 7	. . . . . . . . . . . . 13 |- (m e. [_0 / k]_B -> A.k m e. [_0 / k]_B)
147	142, 125, 146	hbopr 4904	. . . . . . . . . . . 12 |- (m e. ([_(n + 1) / j]_A x. [_0 / k]_B) -> A.k m e. ([_(n + 1) / j]_A x. [_0 / k]_B))
148		csbeq1a 2546	. . . . . . . . . . . . 13 |- (k = 0 -> B = [_0 / k]_B)
149	148	opreq2d 4898	. . . . . . . . . . . 12 |- (k = 0 -> ([_(n + 1) / j]_A x. B) = ([_(n + 1) / j]_A x. [_0 / k]_B))
150	147, 149	fsum1fi 8267	. . . . . . . . . . 11 |- ((([_(n + 1) / j]_A x. [_0 / k]_B) e. _V /\ 0 e. ZZ) -> sum_k e. (0...0)([_(n + 1) / j]_A x. B) = ([_(n + 1) / j]_A x. [_0 / k]_B))
151		oprex 4907	. . . . . . . . . . 11 |- ([_(n + 1) / j]_A x. [_0 / k]_B) e. _V
152		eluzel2 7593	. . . . . . . . . . 11 |- (n e. (ZZ>=` 0) -> 0 e. ZZ)
153	150, 151, 152	sylancr 526	. . . . . . . . . 10 |- (n e. (ZZ>=` 0) -> sum_k e. (0...0)([_(n + 1) / j]_A x. B) = ([_(n + 1) / j]_A x. [_0 / k]_B))
154	141, 153	eqtrd 1925	. . . . . . . . 9 |- (n e. (ZZ>=` 0) -> sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B) = ([_(n + 1) / j]_A x. [_0 / k]_B))
155	135, 154	opreq12d 4900	. . . . . . . 8 |- (n e. (ZZ>=` 0) -> (sum_j e. (0...n)sum_k e. (0...((n + 1) - j))(A x. B) + sum_k e. (0...((n + 1) - (n + 1)))([_(n + 1) / j]_A x. B)) = (sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)))
156	118, 155	eqtrd 1925	. . . . . . 7 |- (n e. (ZZ>=` 0) -> sum_j e. (0...(n + 1))sum_k e. (0...((n + 1) - j))(A x. B) = (sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)))
157	156	ad2antrr 440	. . . . . 6 |- (((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))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)) -> sum_j e. (0...(n + 1))sum_k e. (0...((n + 1) - j))(A x. B) = (sum_j e. (0...n)(sum_k e. (0...(n - j))(A x. B) + (A x. [_((n - j) + 1) / k]_B)) + ([_(n + 1) / j]_A x. [_0 / k]_B)))
158		sumex 8241	. . . . . . . . 9 |- sum_j e. (0...k)(A x. [_(k - j) / k]_B) e. _V
159		sumex 8241	. . . . . . . . 9 |- sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B) e. _V
160		ax-17 1317	. . . . . . . . . 10 |- (m e. (0...(n + 1)) -> A.k m e. (0...(n + 1)))
161		oprex 4907	. . . . . . . . . . . 12 |- ((n + 1) - j) e. _V
162		ax-17 1317	. . . . . . . . . . . 12 |- (m e. ((n + 1) - j) -> A.k m e. ((n + 1) - j))
163	161, 162	hbcsb1 2568	. . . . . . . . . . 11 |- (m e. [_((n + 1) - j) / k]_B -> A.k m e. [_((n + 1) - j) / k]_B)
164	124, 125, 163	hbopr 4904	. . . . . . . . . 10 |- (m e. (A x. [_((n + 1) - j) / k]_B) -> A.k m e. (A x. [_((n + 1) - j) / k]_B))
165	160, 164	hbsum 8244	. . . . . . . . 9 |- (m e. sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B) -> A.k m e. sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B))
166		opreq2 4890	. . . . . . . . . 10 |- (k = (n + 1) -> (0...k) = (0...(n + 1)))
167		opreq1 4889	. . . . . . . . . . . . 13 |- (k = (n + 1) -> (k - j) = ((n + 1) - j))
168	167	csbeq1d 2544	. . . . . . . . . . . 12 |- (k = (n + 1) -> [_(k - j) / k]_B = [_((n + 1) - j) / k]_B)
169	168	opreq2d 4898	. . . . . . . . . . 11 |- (k = (n + 1) -> (A x. [_(k - j) / k]_B) = (A x. [_((n + 1) - j) / k]_B))
170	169	adantr 425	. . . . . . . . . 10 |- ((k = (n + 1) /\ j e. (0...(n + 1))) -> (A x. [_(k - j) / k]_B) = (A x. [_((n + 1) - j) / k]_B))
171	166, 170	sumeq12rdv 8256	. . . . . . . . 9 |- (k = (n + 1) -> sum_j e. (0...k)(A x. [_(k - j) / k]_B) = sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B))
172	158, 159, 165, 171	fsump1fi 8271	. . . . . . . 8 |- (n e. (ZZ>=` 0) -> sum_k e. (0...(n + 1))sum_j e. (0...k)(A x. [_(k - j) / k]_B) = (sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B) + sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B)))
173		oprex 4907	. . . . . . . . . . 11 |- (A x. [_((n + 1) - j) / k]_B) e. _V
174		oprex 4907	. . . . . . . . . . 11 |- ([_(n + 1) / j]_A x. [_((n + 1) - (n + 1)) / k]_B) e. _V
175		ax-17 1317	. . . . . . . . . . . 12 |- (m e. [_((n + 1) - (n + 1)) / k]_B -> A.j m e. [_((n + 1) - (n + 1)) / k]_B)
176	107, 108, 175	hbopr 4904	. . . . . . . . . . 11 |- (m e. ([_(n + 1) / j]_A x. [_((n + 1) - (n + 1)) / k]_B) -> A.j m e. ([_(n + 1) / j]_A x. [_((n + 1) - (n + 1)) / k]_B))
177	112	csbeq1d 2544	. . . . . . . . . . . 12 |- (j = (n + 1) -> [_((n + 1) - j) / k]_B = [_((n + 1) - (n + 1)) / k]_B)
178	114, 177	opreq12d 4900	. . . . . . . . . . 11 |- (j = (n + 1) -> (A x. [_((n + 1) - j) / k]_B) = ([_(n + 1) / j]_A x. [_((n + 1) - (n + 1)) / k]_B))
179	173, 174, 176, 178	fsump1fi 8271	. . . . . . . . . 10 |- (n e. (ZZ>=` 0) -> sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B) = (sum_j e. (0...n)(A x. [_((n + 1) - j) / k]_B) + ([_(n + 1) / j]_A x. [_((n + 1) - (n + 1)) / k]_B)))
180	25	csbeq1d 2544	. . . . . . . . . . . . . 14 |- ((n e. CC /\ j e. CC) -> [_((n + 1) - j) / k]_B = [_((n - j) + 1) / k]_B)
181	180	opreq2d 4898	. . . . . . . . . . . . 13 |- ((n e. CC /\ j e. CC) -> (A x. [_((n + 1) - j) / k]_B) = (A x. [_((n - j) + 1) / k]_B))
182	181, 28, 31	syl2an 503	. . . . . . . . . . . 12 |- ((n e. (ZZ>=` 0) /\ j e. (0...n)) -> (A x. [_((n + 1) - j) / k]_B) = (A x. [_((n - j) + 1) / k]_B))
183	182	sumeq2dv 8252	. . . . . . . . . . 11 |- (n e. (ZZ>=` 0) -> sum_j e. (0...n)(A x. [_((n + 1) - j) / k]_B) = sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B))
184	139	csbeq1d 2544	. . . . . . . . . . . 12 |- (n e. (ZZ>=` 0) -> [_((n + 1) - (n + 1)) / k]_B = [_0 / k]_B)
185	184	opreq2d 4898	. . . . . . . . . . 11 |- (n e. (ZZ>=` 0) -> ([_(n + 1) / j]_A x. [_((n + 1) - (n + 1)) / k]_B) = ([_(n + 1) / j]_A x. [_0 / k]_B))
186	183, 185	opreq12d 4900	. . . . . . . . . 10 |- (n e. (ZZ>=` 0) -> (sum_j e. (0...n)(A x. [_((n + 1) - j) / k]_B) + ([_(n + 1) / j]_A x. [_((n + 1) - (n + 1)) / k]_B)) = (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B)))
187	179, 186	eqtrd 1925	. . . . . . . . 9 |- (n e. (ZZ>=` 0) -> sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B) = (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B)))
188	187	opreq2d 4898	. . . . . . . 8 |- (n e. (ZZ>=` 0) -> (sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B) + sum_j e. (0...(n + 1))(A x. [_((n + 1) - j) / k]_B)) = (sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
189	172, 188	eqtrd 1925	. . . . . . 7 |- (n e. (ZZ>=` 0) -> sum_k e. (0...(n + 1))sum_j e. (0...k)(A x. [_(k - j) / k]_B) = (sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
190	189	ad2antrr 440	. . . . . 6 |- (((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))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)) -> sum_k e. (0...(n + 1))sum_j e. (0...k)(A x. [_(k - j) / k]_B) = (sum_k e. (0...n)sum_j e. (0...k)(A x. [_(k - j) / k]_B) + (sum_j e. (0...n)(A x. [_((n - j) + 1) / k]_B) + ([_(n + 1) / j]_A x. [_0 / k]_B))))
191	101, 157, 190	3eqtr4d 1937	. . . . 5 |- (((n e. (ZZ>=` 0) /\ (A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))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)) -> 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))
192	191	exp31 407	. . . 4 |- (n e. (ZZ>=` 0) -> ((A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))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) -> 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))))
193	1, 192	sylbi 216	. . 3 |- (n e. NN0 -> ((A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))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) -> 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))))
194	193	a2d 16	. 2 |- (n e. NN0 -> (((A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))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))))
195	73, 75	anim12i 360	. . 3 |- ((A.j e. (0...(n + 1))A e. CC /\ A.k e. (0...(n + 1))B e. CC) -> (A.j e. (0...n)A e. CC /\ A.k e. (0...n)B e. CC))
196	195	imim1i 19	. 2 |- (((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)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)))
197	194, 196	syl5 20	1 |- (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))))

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105  _Vcvv 2292  [_csb 2540   C_ wss 2593  ` cfv 3998  (class class class)co 4884  CCcc 6384  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445  NN0cn0 6450  ZZcz 6451  ZZ>=cuz 7586  ...cfz 7637  sum_csu 8239

This theorem is referenced by:  fsum0diag 8520

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-n0 7309  df-z 7345  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-clim 8235  df-sum 8240

Copyright terms: Public domain