Theorem fsumabs2mul 7044

Description: The sum of absolute values of the product A(j) x. B(m) is less than or equal to the product of the two sums of absolute values.

Assertion

Ref	Expression
fsumabs2mul	|- (((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) /\ (N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC)) -> (abs` sum_j e. (J...K)sum_m e. (M...N)(A x. B)) <_ (sum_j e. (J...K)(abs` A) x. sum_m e. (M...N)(abs` B)))

Distinct variable groups:   A,m   B,j   j,J   j,K   j,m,M   j,N,m

Proof of Theorem fsumabs2mul

Step	Hyp	Ref	Expression
1		fsum2mul 7037	. . . 4 |- (((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) /\ (N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC)) -> sum_j e. (J...K)sum_m e. (M...N)(A x. B) = (sum_j e. (J...K)A x. sum_m e. (M...N)B))
2	1	fveq2d 3728	. . 3 |- (((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) /\ (N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC)) -> (abs` sum_j e. (J...K)sum_m e. (M...N)(A x. B)) = (abs` (sum_j e. (J...K)A x. sum_m e. (M...N)B)))
3		absmult 6858	. . . 4 |- ((sum_j e. (J...K)A e. CC /\ sum_m e. (M...N)B e. CC) -> (abs` (sum_j e. (J...K)A x. sum_m e. (M...N)B)) = ((abs` sum_j e. (J...K)A) x. (abs` sum_m e. (M...N)B)))
4		fsumclt 7015	. . . 4 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> sum_j e. (J...K)A e. CC)
5		fsumclt 7015	. . . 4 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> sum_m e. (M...N)B e. CC)
6	3, 4, 5	syl2an 454	. . 3 |- (((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) /\ (N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC)) -> (abs` (sum_j e. (J...K)A x. sum_m e. (M...N)B)) = ((abs` sum_j e. (J...K)A) x. (abs` sum_m e. (M...N)B)))
7	2, 6	eqtrd 1507	. 2 |- (((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) /\ (N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC)) -> (abs` sum_j e. (J...K)sum_m e. (M...N)(A x. B)) = ((abs` sum_j e. (J...K)A) x. (abs` sum_m e. (M...N)B)))
8		lemul12itOLD 5843	. . 3 |- (((((abs` sum_j e. (J...K)A) e. RR /\ sum_j e. (J...K)(abs` A) e. RR) /\ (0 <_ (abs` sum_j e. (J...K)A) /\ (abs` sum_j e. (J...K)A) <_ sum_j e. (J...K)(abs` A))) /\ (((abs` sum_m e. (M...N)B) e. RR /\ sum_m e. (M...N)(abs` B) e. RR) /\ (0 <_ (abs` sum_m e. (M...N)B) /\ (abs` sum_m e. (M...N)B) <_ sum_m e. (M...N)(abs` B)))) -> ((abs` sum_j e. (J...K)A) x. (abs` sum_m e. (M...N)B)) <_ (sum_j e. (J...K)(abs` A) x. sum_m e. (M...N)(abs` B)))
9		absclt 6833	. . . . . 6 |- (sum_j e. (J...K)A e. CC -> (abs` sum_j e. (J...K)A) e. RR)
10	4, 9	syl 10	. . . . 5 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> (abs` sum_j e. (J...K)A) e. RR)
11		fsumreclt 7017	. . . . . 6 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)(abs` A) e. RR) -> sum_j e. (J...K)(abs` A) e. RR)
12		absclt 6833	. . . . . . 7 |- (A e. CC -> (abs` A) e. RR)
13	12	r19.20si 1706	. . . . . 6 |- (A.j e. (J...K)A e. CC -> A.j e. (J...K)(abs` A) e. RR)
14	11, 13	sylan2 451	. . . . 5 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> sum_j e. (J...K)(abs` A) e. RR)
15	10, 14	jca 288	. . . 4 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> ((abs` sum_j e. (J...K)A) e. RR /\ sum_j e. (J...K)(abs` A) e. RR))
16		absge0t 6854	. . . . . 6 |- (sum_j e. (J...K)A e. CC -> 0 <_ (abs` sum_j e. (J...K)A))
17	4, 16	syl 10	. . . . 5 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> 0 <_ (abs` sum_j e. (J...K)A))
18		fsumabs 7043	. . . . 5 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> (abs` sum_j e. (J...K)A) <_ sum_j e. (J...K)(abs` A))
19	17, 18	jca 288	. . . 4 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> (0 <_ (abs` sum_j e. (J...K)A) /\ (abs` sum_j e. (J...K)A) <_ sum_j e. (J...K)(abs` A)))
20	15, 19	jca 288	. . 3 |- ((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) -> (((abs` sum_j e. (J...K)A) e. RR /\ sum_j e. (J...K)(abs` A) e. RR) /\ (0 <_ (abs` sum_j e. (J...K)A) /\ (abs` sum_j e. (J...K)A) <_ sum_j e. (J...K)(abs` A))))
21		absclt 6833	. . . . . 6 |- (sum_m e. (M...N)B e. CC -> (abs` sum_m e. (M...N)B) e. RR)
22	5, 21	syl 10	. . . . 5 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> (abs` sum_m e. (M...N)B) e. RR)
23		fsumreclt 7017	. . . . . 6 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)(abs` B) e. RR) -> sum_m e. (M...N)(abs` B) e. RR)
24		absclt 6833	. . . . . . 7 |- (B e. CC -> (abs` B) e. RR)
25	24	r19.20si 1706	. . . . . 6 |- (A.m e. (M...N)B e. CC -> A.m e. (M...N)(abs` B) e. RR)
26	23, 25	sylan2 451	. . . . 5 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> sum_m e. (M...N)(abs` B) e. RR)
27	22, 26	jca 288	. . . 4 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> ((abs` sum_m e. (M...N)B) e. RR /\ sum_m e. (M...N)(abs` B) e. RR))
28		absge0t 6854	. . . . . 6 |- (sum_m e. (M...N)B e. CC -> 0 <_ (abs` sum_m e. (M...N)B))
29	5, 28	syl 10	. . . . 5 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> 0 <_ (abs` sum_m e. (M...N)B))
30		fsumabs 7043	. . . . 5 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> (abs` sum_m e. (M...N)B) <_ sum_m e. (M...N)(abs` B))
31	29, 30	jca 288	. . . 4 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> (0 <_ (abs` sum_m e. (M...N)B) /\ (abs` sum_m e. (M...N)B) <_ sum_m e. (M...N)(abs` B)))
32	27, 31	jca 288	. . 3 |- ((N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC) -> (((abs` sum_m e. (M...N)B) e. RR /\ sum_m e. (M...N)(abs` B) e. RR) /\ (0 <_ (abs` sum_m e. (M...N)B) /\ (abs` sum_m e. (M...N)B) <_ sum_m e. (M...N)(abs` B))))
33	8, 20, 32	syl2an 454	. 2 |- (((K e. (ZZ>` J) /\ A.j e. (J...K)A e. CC) /\ (N e. (ZZ>` M) /\ A.m e. (M...N)B e. CC)) -> ((abs` sum_j e. (J...K)A) x. (abs` sum_m e. (M...N)B)) <_ (sum_j e. (J...K)(abs` A) x. sum_m e. (M