Theorem csbrni 15832

Description: Cauchy-Schwarz-Bunjakovsky inequality for R^n.

Hypotheses

Ref	Expression
csbrni.1	|- N e. NN
csbrni.2	|- X:(1...N)-->RR
csbrni.3	|- Y:(1...N)-->RR

Assertion

Ref	Expression
csbrni	|- (sum_k e. (1...N)((X` k) x. (Y` k))^2) <_ (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))

Distinct variable groups:   k,N   k,X   k,Y

Proof of Theorem csbrni

Step	Hyp	Ref	Expression
1		csbrni.1	. . . . . . 7 |- N e. NN
2		elnnuz 7609	. . . . . . 7 |- (N e. NN <-> N e. (ZZ>=` 1))
3	1, 2	mpbi 206	. . . . . 6 |- N e. (ZZ>=` 1)
4		reexpcl 7823	. . . . . . . . 9 |- (((X` k) e. RR /\ 2 e. NN0) -> ((X` k)^2) e. RR)
5		csbrni.2	. . . . . . . . . 10 |- X:(1...N)-->RR
6	5	ffvelrni 4788	. . . . . . . . 9 |- (k e. (1...N) -> (X` k) e. RR)
7		2nn0 7324	. . . . . . . . 9 |- 2 e. NN0
8	4, 6, 7	sylancl 525	. . . . . . . 8 |- (k e. (1...N) -> ((X` k)^2) e. RR)
9		sqge0 7878	. . . . . . . . 9 |- ((X` k) e. RR -> 0 <_ ((X` k)^2))
10	6, 9	syl 12	. . . . . . . 8 |- (k e. (1...N) -> 0 <_ ((X` k)^2))
11	8, 10	jca 310	. . . . . . 7 |- (k e. (1...N) -> (((X` k)^2) e. RR /\ 0 <_ ((X` k)^2)))
12	11	rgen 2159	. . . . . 6 |- A.k e. (1...N)(((X` k)^2) e. RR /\ 0 <_ ((X` k)^2))
13		fsumcmp0 8301	. . . . . 6 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)(((X` k)^2) e. RR /\ 0 <_ ((X` k)^2))) -> 0 <_ sum_k e. (1...N)((X` k)^2))
14	3, 12, 13	mp2an 761	. . . . 5 |- 0 <_ sum_k e. (1...N)((X` k)^2)
15	8	rgen 2159	. . . . . . 7 |- A.k e. (1...N)((X` k)^2) e. RR
16		fsumrecl 8277	. . . . . . 7 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)((X` k)^2) e. RR) -> sum_k e. (1...N)((X` k)^2) e. RR)
17	3, 15, 16	mp2an 761	. . . . . 6 |- sum_k e. (1...N)((X` k)^2) e. RR
18		2re 7163	. . . . . . 7 |- 2 e. RR
19		csbrni.3	. . . . . . . . . . 11 |- Y:(1...N)-->RR
20	19	ffvelrni 4788	. . . . . . . . . 10 |- (k e. (1...N) -> (Y` k) e. RR)
21		remulcl 6457	. . . . . . . . . 10 |- (((X` k) e. RR /\ (Y` k) e. RR) -> ((X` k) x. (Y` k)) e. RR)
22	6, 20, 21	syl11anc 524	. . . . . . . . 9 |- (k e. (1...N) -> ((X` k) x. (Y` k)) e. RR)
23	22	rgen 2159	. . . . . . . 8 |- A.k e. (1...N)((X` k) x. (Y` k)) e. RR
24		fsumrecl 8277	. . . . . . . 8 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)((X` k) x. (Y` k)) e. RR) -> sum_k e. (1...N)((X` k) x. (Y` k)) e. RR)
25	3, 23, 24	mp2an 761	. . . . . . 7 |- sum_k e. (1...N)((X` k) x. (Y` k)) e. RR
26	18, 25	remulcli 6488	. . . . . 6 |- (2 x. sum_k e. (1...N)((X` k) x. (Y` k))) e. RR
27		reexpcl 7823	. . . . . . . . 9 |- (((Y` k) e. RR /\ 2 e. NN0) -> ((Y` k)^2) e. RR)
28	27, 20, 7	sylancl 525	. . . . . . . 8 |- (k e. (1...N) -> ((Y` k)^2) e. RR)
29	28	rgen 2159	. . . . . . 7 |- A.k e. (1...N)((Y` k)^2) e. RR
30		fsumrecl 8277	. . . . . . 7 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)((Y` k)^2) e. RR) -> sum_k e. (1...N)((Y` k)^2) e. RR)
31	3, 29, 30	mp2an 761	. . . . . 6 |- sum_k e. (1...N)((Y` k)^2) e. RR
32		fsumcmp0 8301	. . . . . . . . 9 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)((((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)) e. RR /\ 0 <_ (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)))) -> 0 <_ sum_k e. (1...N)(((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)))
33		remulcl 6457	. . . . . . . . . . . . . . 15 |- ((((X` k)^2) e. RR /\ (t^2) e. RR) -> (((X` k)^2) x. (t^2)) e. RR)
34		resqcl 7866	. . . . . . . . . . . . . . 15 |- (t e. RR -> (t^2) e. RR)
35	33, 8, 34	syl2an 503	. . . . . . . . . . . . . 14 |- ((k e. (1...N) /\ t e. RR) -> (((X` k)^2) x. (t^2)) e. RR)
36	35	ancoms 484	. . . . . . . . . . . . 13 |- ((t e. RR /\ k e. (1...N)) -> (((X` k)^2) x. (t^2)) e. RR)
37		remulcl 6457	. . . . . . . . . . . . . . 15 |- (((2 x. ((X` k) x. (Y` k))) e. RR /\ t e. RR) -> ((2 x. ((X` k) x. (Y` k))) x. t) e. RR)
38		remulcl 6457	. . . . . . . . . . . . . . . 16 |- ((2 e. RR /\ ((X` k) x. (Y` k)) e. RR) -> (2 x. ((X` k) x. (Y` k))) e. RR)
39	38, 18, 22	sylancr 526	. . . . . . . . . . . . . . 15 |- (k e. (1...N) -> (2 x. ((X` k) x. (Y` k))) e. RR)
40	37, 39	sylan 497	. . . . . . . . . . . . . 14 |- ((k e. (1...N) /\ t e. RR) -> ((2 x. ((X` k) x. (Y` k))) x. t) e. RR)
41	40	ancoms 484	. . . . . . . . . . . . 13 |- ((t e. RR /\ k e. (1...N)) -> ((2 x. ((X` k) x. (Y` k))) x. t) e. RR)
42		readdcl 6455	. . . . . . . . . . . . 13 |- (((((X` k)^2) x. (t^2)) e. RR /\ ((2 x. ((X` k) x. (Y` k))) x. t) e. RR) -> ((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. RR)
43	36, 41, 42	syl11anc 524	. . . . . . . . . . . 12 |- ((t e. RR /\ k e. (1...N)) -> ((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. RR)
44	28	adantl 424	. . . . . . . . . . . 12 |- ((t e. RR /\ k e. (1...N)) -> ((Y` k)^2) e. RR)
45		readdcl 6455	. . . . . . . . . . . 12 |- ((((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. RR /\ ((Y` k)^2) e. RR) -> (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)) e. RR)
46	43, 44, 45	syl11anc 524	. . . . . . . . . . 11 |- ((t e. RR /\ k e. (1...N)) -> (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)) e. RR)
47		remulcl 6457	. . . . . . . . . . . . . . . 16 |- (((X` k) e. RR /\ t e. RR) -> ((X` k) x. t) e. RR)
48	47, 6	sylan 497	. . . . . . . . . . . . . . 15 |- ((k e. (1...N) /\ t e. RR) -> ((X` k) x. t) e. RR)
49	48	ancoms 484	. . . . . . . . . . . . . 14 |- ((t e. RR /\ k e. (1...N)) -> ((X` k) x. t) e. RR)
50	20	adantl 424	. . . . . . . . . . . . . 14 |- ((t e. RR /\ k e. (1...N)) -> (Y` k) e. RR)
51		readdcl 6455	. . . . . . . . . . . . . 14 |- ((((X` k) x. t) e. RR /\ (Y` k) e. RR) -> (((X` k) x. t) + (Y` k)) e. RR)
52	49, 50, 51	syl11anc 524	. . . . . . . . . . . . 13 |- ((t e. RR /\ k e. (1...N)) -> (((X` k) x. t) + (Y` k)) e. RR)
53		sqge0 7878	. . . . . . . . . . . . 13 |- ((((X` k) x. t) + (Y` k)) e. RR -> 0 <_ ((((X` k) x. t) + (Y` k))^2))
54	52, 53	syl 12	. . . . . . . . . . . 12 |- ((t e. RR /\ k e. (1...N)) -> 0 <_ ((((X` k) x. t) + (Y` k))^2))
55		mulcl 6456	. . . . . . . . . . . . . . . 16 |- (((X` k) e. CC /\ t e. CC) -> ((X` k) x. t) e. CC)
56	6	recnd 6468	. . . . . . . . . . . . . . . 16 |- (k e. (1...N) -> (X` k) e. CC)
57		recn 6466	. . . . . . . . . . . . . . . 16 |- (t e. RR -> t e. CC)
58	55, 56, 57	syl2an 503	. . . . . . . . . . . . . . 15 |- ((k e. (1...N) /\ t e. RR) -> ((X` k) x. t) e. CC)
59	58	ancoms 484	. . . . . . . . . . . . . 14 |- ((t e. RR /\ k e. (1...N)) -> ((X` k) x. t) e. CC)
60	20	recnd 6468	. . . . . . . . . . . . . . 15 |- (k e. (1...N) -> (Y` k) e. CC)
61	60	adantl 424	. . . . . . . . . . . . . 14 |- ((t e. RR /\ k e. (1...N)) -> (Y` k) e. CC)
62		binom2 7896	. . . . . . . . . . . . . 14 |- ((((X` k) x. t) e. CC /\ (Y` k) e. CC) -> ((((X` k) x. t) + (Y` k))^2) = (((((X` k) x. t)^2) + (2 x. (((X` k) x. t) x. (Y` k)))) + ((Y` k)^2)))
63	59, 61, 62	syl11anc 524	. . . . . . . . . . . . 13 |- ((t e. RR /\ k e. (1...N)) -> ((((X` k) x. t) + (Y` k))^2) = (((((X` k) x. t)^2) + (2 x. (((X` k) x. t) x. (Y` k)))) + ((Y` k)^2)))
64	56	adantl 424	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ k e. (1...N)) -> (X` k) e. CC)
65	57	adantr 425	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ k e. (1...N)) -> t e. CC)
66	7	a1i 8	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ k e. (1...N)) -> 2 e. NN0)
67		mulexp 7836	. . . . . . . . . . . . . . . 16 |- (((X` k) e. CC /\ t e. CC /\ 2 e. NN0) -> (((X` k) x. t)^2) = (((X` k)^2) x. (t^2)))
68	64, 65, 66, 67	syl111anc 1100	. . . . . . . . . . . . . . 15 |- ((t e. RR /\ k e. (1...N)) -> (((X` k) x. t)^2) = (((X` k)^2) x. (t^2)))
69		mul23 6580	. . . . . . . . . . . . . . . . . 18 |- (((X` k) e. CC /\ t e. CC /\ (Y` k) e. CC) -> (((X` k) x. t) x. (Y` k)) = (((X` k) x. (Y` k)) x. t))
70	64, 65, 61, 69	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((t e. RR /\ k e. (1...N)) -> (((X` k) x. t) x. (Y` k)) = (((X` k) x. (Y` k)) x. t))
71	70	opreq2d 4898	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ k e. (1...N)) -> (2 x. (((X` k) x. t) x. (Y` k))) = (2 x. (((X` k) x. (Y` k)) x. t)))
72		2cn 7164	. . . . . . . . . . . . . . . . . 18 |- 2 e. CC
73	72	a1i 8	. . . . . . . . . . . . . . . . 17 |- ((t e. RR /\ k e. (1...N)) -> 2 e. CC)
74	22	recnd 6468	. . . . . . . . . . . . . . . . . 18 |- (k e. (1...N) -> ((X` k) x. (Y` k)) e. CC)
75	74	adantl 424	. . . . . . . . . . . . . . . . 17 |- ((t e. RR /\ k e. (1...N)) -> ((X` k) x. (Y` k)) e. CC)
76		mulass 6461	. . . . . . . . . . . . . . . . 17 |- ((2 e. CC /\ ((X` k) x. (Y` k)) e. CC /\ t e. CC) -> ((2 x. ((X` k) x. (Y` k))) x. t) = (2 x. (((X` k) x. (Y` k)) x. t)))
77	73, 75, 65, 76	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((t e. RR /\ k e. (1...N)) -> ((2 x. ((X` k) x. (Y` k))) x. t) = (2 x. (((X` k) x. (Y` k)) x. t)))
78	71, 77	eqtr4d 1928	. . . . . . . . . . . . . . 15 |- ((t e. RR /\ k e. (1...N)) -> (2 x. (((X` k) x. t) x. (Y` k))) = ((2 x. ((X` k) x. (Y` k))) x. t))
79	68, 78	opreq12d 4900	. . . . . . . . . . . . . 14 |- ((t e. RR /\ k e. (1...N)) -> ((((X` k) x. t)^2) + (2 x. (((X` k) x. t) x. (Y` k)))) = ((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)))
80	79	opreq1d 4897	. . . . . . . . . . . . 13 |- ((t e. RR /\ k e. (1...N)) -> (((((X` k) x. t)^2) + (2 x. (((X` k) x. t) x. (Y` k)))) + ((Y` k)^2)) = (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)))
81	63, 80	eqtrd 1925	. . . . . . . . . . . 12 |- ((t e. RR /\ k e. (1...N)) -> ((((X` k) x. t) + (Y` k))^2) = (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)))
82	54, 81	breqtrd 3361	. . . . . . . . . . 11 |- ((t e. RR /\ k e. (1...N)) -> 0 <_ (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)))
83	46, 82	jca 310	. . . . . . . . . 10 |- ((t e. RR /\ k e. (1...N)) -> ((((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)) e. RR /\ 0 <_ (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2))))
84	83	r19.21aiva 2176	. . . . . . . . 9 |- (t e. RR -> A.k e. (1...N)((((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)) e. RR /\ 0 <_ (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2))))
85	32, 3, 84	sylancr 526	. . . . . . . 8 |- (t e. RR -> 0 <_ sum_k e. (1...N)(((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)))
86		fsumadd 8282	. . . . . . . . . . 11 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)((((X` k)^2) x. (t^2)) e. CC /\ ((2 x. ((X` k) x. (Y` k))) x. t) e. CC)) -> sum_k e. (1...N)((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) = (sum_k e. (1...N)(((X` k)^2) x. (t^2)) + sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t)))
87		mulcl 6456	. . . . . . . . . . . . . . 15 |- ((((X` k)^2) e. CC /\ (t^2) e. CC) -> (((X` k)^2) x. (t^2)) e. CC)
88	8	recnd 6468	. . . . . . . . . . . . . . 15 |- (k e. (1...N) -> ((X` k)^2) e. CC)
89	34	recnd 6468	. . . . . . . . . . . . . . 15 |- (t e. RR -> (t^2) e. CC)
90	87, 88, 89	syl2an 503	. . . . . . . . . . . . . 14 |- ((k e. (1...N) /\ t e. RR) -> (((X` k)^2) x. (t^2)) e. CC)
91	90	ancoms 484	. . . . . . . . . . . . 13 |- ((t e. RR /\ k e. (1...N)) -> (((X` k)^2) x. (t^2)) e. CC)
92		mulcl 6456	. . . . . . . . . . . . . . 15 |- (((2 x. ((X` k) x. (Y` k))) e. CC /\ t e. CC) -> ((2 x. ((X` k) x. (Y` k))) x. t) e. CC)
93	39	recnd 6468	. . . . . . . . . . . . . . 15 |- (k e. (1...N) -> (2 x. ((X` k) x. (Y` k))) e. CC)
94	92, 93, 57	syl2an 503	. . . . . . . . . . . . . 14 |- ((k e. (1...N) /\ t e. RR) -> ((2 x. ((X` k) x. (Y` k))) x. t) e. CC)
95	94	ancoms 484	. . . . . . . . . . . . 13 |- ((t e. RR /\ k e. (1...N)) -> ((2 x. ((X` k) x. (Y` k))) x. t) e. CC)
96	91, 95	jca 310	. . . . . . . . . . . 12 |- ((t e. RR /\ k e. (1...N)) -> ((((X` k)^2) x. (t^2)) e. CC /\ ((2 x. ((X` k) x. (Y` k))) x. t) e. CC))
97	96	r19.21aiva 2176	. . . . . . . . . . 11 |- (t e. RR -> A.k e. (1...N)((((X` k)^2) x. (t^2)) e. CC /\ ((2 x. ((X` k) x. (Y` k))) x. t) e. CC))
98	86, 3, 97	sylancr 526	. . . . . . . . . 10 |- (t e. RR -> sum_k e. (1...N)((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) = (sum_k e. (1...N)(((X` k)^2) x. (t^2)) + sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t)))
99	98	opreq1d 4897	. . . . . . . . 9 |- (t e. RR -> (sum_k e. (1...N)((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)) = ((sum_k e. (1...N)(((X` k)^2) x. (t^2)) + sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)))
100		fsumadd 8282	. . . . . . . . . 10 |- ((N e. (ZZ>=` 1) /\ A.k e. (1...N)(((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. CC /\ ((Y` k)^2) e. CC)) -> sum_k e. (1...N)(((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)) = (sum_k e. (1...N)((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)))
101		addcl 6454	. . . . . . . . . . . . 13 |- (((((X` k)^2) x. (t^2)) e. CC /\ ((2 x. ((X` k) x. (Y` k))) x. t) e. CC) -> ((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. CC)
102	91, 95, 101	syl11anc 524	. . . . . . . . . . . 12 |- ((t e. RR /\ k e. (1...N)) -> ((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. CC)
103	28	recnd 6468	. . . . . . . . . . . . 13 |- (k e. (1...N) -> ((Y` k)^2) e. CC)
104	103	adantl 424	. . . . . . . . . . . 12 |- ((t e. RR /\ k e. (1...N)) -> ((Y` k)^2) e. CC)
105	102, 104	jca 310	. . . . . . . . . . 11 |- ((t e. RR /\ k e. (1...N)) -> (((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. CC /\ ((Y` k)^2) e. CC))
106	105	r19.21aiva 2176	. . . . . . . . . 10 |- (t e. RR -> A.k e. (1...N)(((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) e. CC /\ ((Y` k)^2) e. CC))
107	100, 3, 106	sylancr 526	. . . . . . . . 9 |- (t e. RR -> sum_k e. (1...N)(((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)) = (sum_k e. (1...N)((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)))
108	3	a1i 8	. . . . . . . . . . . 12 |- (t e. RR -> N e. (ZZ>=` 1))
109	88	rgen 2159	. . . . . . . . . . . . 13 |- A.k e. (1...N)((X` k)^2) e. CC
110	109	a1i 8	. . . . . . . . . . . 12 |- (t e. RR -> A.k e. (1...N)((X` k)^2) e. CC)
111		fsummulc2 8294	. . . . . . . . . . . 12 |- ((N e. (ZZ>=` 1) /\ (t^2) e. CC /\ A.k e. (1...N)((X` k)^2) e. CC) -> (sum_k e. (1...N)((X` k)^2) x. (t^2)) = sum_k e. (1...N)(((X` k)^2) x. (t^2)))
112	108, 89, 110, 111	syl111anc 1100	. . . . . . . . . . 11 |- (t e. RR -> (sum_k e. (1...N)((X` k)^2) x. (t^2)) = sum_k e. (1...N)(((X` k)^2) x. (t^2)))
113	72	a1i 8	. . . . . . . . . . . . . 14 |- (t e. RR -> 2 e. CC)
114	74	rgen 2159	. . . . . . . . . . . . . . 15 |- A.k e. (1...N)((X` k) x. (Y` k)) e. CC
115	114	a1i 8	. . . . . . . . . . . . . 14 |- (t e. RR -> A.k e. (1...N)((X` k) x. (Y` k)) e. CC)
116		fsummulc1 8293	. . . . . . . . . . . . . 14 |- ((N e. (ZZ>=` 1) /\ 2 e. CC /\ A.k e. (1...N)((X` k) x. (Y` k)) e. CC) -> (2 x. sum_k e. (1...N)((X` k) x. (Y` k))) = sum_k e. (1...N)(2 x. ((X` k) x. (Y` k))))
117	108, 113, 115, 116	syl111anc 1100	. . . . . . . . . . . . 13 |- (t e. RR -> (2 x. sum_k e. (1...N)((X` k) x. (Y` k))) = sum_k e. (1...N)(2 x. ((X` k) x. (Y` k))))
118	117	opreq1d 4897	. . . . . . . . . . . 12 |- (t e. RR -> ((2 x. sum_k e. (1...N)((X` k) x. (Y` k))) x. t) = (sum_k e. (1...N)(2 x. ((X` k) x. (Y` k))) x. t))
119	93	rgen 2159	. . . . . . . . . . . . . 14 |- A.k e. (1...N)(2 x. ((X` k) x. (Y` k))) e. CC
120	119	a1i 8	. . . . . . . . . . . . 13 |- (t e. RR -> A.k e. (1...N)(2 x. ((X` k) x. (Y` k))) e. CC)
121		fsummulc2 8294	. . . . . . . . . . . . 13 |- ((N e. (ZZ>=` 1) /\ t e. CC /\ A.k e. (1...N)(2 x. ((X` k) x. (Y` k))) e. CC) -> (sum_k e. (1...N)(2 x. ((X` k) x. (Y` k))) x. t) = sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t))
122	108, 57, 120, 121	syl111anc 1100	. . . . . . . . . . . 12 |- (t e. RR -> (sum_k e. (1...N)(2 x. ((X` k) x. (Y` k))) x. t) = sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t))
123	118, 122	eqtrd 1925	. . . . . . . . . . 11 |- (t e. RR -> ((2 x. sum_k e. (1...N)((X` k) x. (Y` k))) x. t) = sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t))
124	112, 123	opreq12d 4900	. . . . . . . . . 10 |- (t e. RR -> ((sum_k e. (1...N)((X` k)^2) x. (t^2)) + ((2 x. sum_k e. (1...N)((X` k) x. (Y` k))) x. t)) = (sum_k e. (1...N)(((X` k)^2) x. (t^2)) + sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t)))
125	124	opreq1d 4897	. . . . . . . . 9 |- (t e. RR -> (((sum_k e. (1...N)((X` k)^2) x. (t^2)) + ((2 x. sum_k e. (1...N)((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)) = ((sum_k e. (1...N)(((X` k)^2) x. (t^2)) + sum_k e. (1...N)((2 x. ((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)))
126	99, 107, 125	3eqtr4rd 1939	. . . . . . . 8 |- (t e. RR -> (((sum_k e. (1...N)((X` k)^2) x. (t^2)) + ((2 x. sum_k e. (1...N)((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)) = sum_k e. (1...N)(((((X` k)^2) x. (t^2)) + ((2 x. ((X` k) x. (Y` k))) x. t)) + ((Y` k)^2)))
127	85, 126	breqtrrd 3363	. . . . . . 7 |- (t e. RR -> 0 <_ (((sum_k e. (1...N)((X` k)^2) x. (t^2)) + ((2 x. sum_k e. (1...N)((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2)))
128	127	rgen 2159	. . . . . 6 |- A.t e. RR 0 <_ (((sum_k e. (1...N)((X` k)^2) x. (t^2)) + ((2 x. sum_k e. (1...N)((X` k) x. (Y` k))) x. t)) + sum_k e. (1...N)((Y` k)^2))
129	17, 26, 31, 128	discrlem 7909	. . . . 5 |- (0 <_ sum_k e. (1...N)((X` k)^2) -> (((2 x. sum_k e. (1...N)((X` k) x. (Y` k)))^2) - (4 x. (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) <_ 0)
130	14, 129	ax-mp 7	. . . 4 |- (((2 x. sum_k e. (1...N)((X` k) x. (Y` k)))^2) - (4 x. (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) <_ 0
131		4re 7166	. . . . . . 7 |- 4 e. RR
132	131	recni 6467	. . . . . 6 |- 4 e. CC
133	25	resqcli 7868	. . . . . . 7 |- (sum_k e. (1...N)((X` k) x. (Y` k))^2) e. RR
134	133	recni 6467	. . . . . 6 |- (sum_k e. (1...N)((X` k) x. (Y` k))^2) e. CC
135	17, 31	remulcli 6488	. . . . . . 7 |- (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)) e. RR
136	135	recni 6467	. . . . . 6 |- (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)) e. CC
137	132, 134, 136	subdii 6592	. . . . 5 |- (4 x. ((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) = ((4 x. (sum_k e. (1...N)((X` k) x. (Y` k))^2)) - (4 x. (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))))
138		sq2 7883	. . . . . . . . 9 |- (2^2) = 4
139	138	eqcomi 1888	. . . . . . . 8 |- 4 = (2^2)
140	139	opreq1i 4892	. . . . . . 7 |- (4 x. (sum_k e. (1...N)((X` k) x. (Y` k))^2)) = ((2^2) x. (sum_k e. (1...N)((X` k) x. (Y` k))^2))
141	25	recni 6467	. . . . . . . 8 |- sum_k e. (1...N)((X` k) x. (Y` k)) e. CC
142	72, 141	sqmuli 7862	. . . . . . 7 |- ((2 x. sum_k e. (1...N)((X` k) x. (Y` k)))^2) = ((2^2) x. (sum_k e. (1...N)((X` k) x. (Y` k))^2))
143	140, 142	eqtr4i 1911	. . . . . 6 |- (4 x. (sum_k e. (1...N)((X` k) x. (Y` k))^2)) = ((2 x. sum_k e. (1...N)((X` k) x. (Y` k)))^2)
144	143	opreq1i 4892	. . . . 5 |- ((4 x. (sum_k e. (1...N)((X` k) x. (Y` k))^2)) - (4 x. (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) = (((2 x. sum_k e. (1...N)((X` k) x. (Y` k)))^2) - (4 x. (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))))
145	137, 144	eqtri 1908	. . . 4 |- (4 x. ((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) = (((2 x. sum_k e. (1...N)((X` k) x. (Y` k)))^2) - (4 x. (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))))
146	132	mul01i 6594	. . . 4 |- (4 x. 0) = 0
147	130, 145, 146	3brtr4i 3365	. . 3 |- (4 x. ((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) <_ (4 x. 0)
148		4pos 7176	. . . 4 |- 0 < 4
149	133, 135	resubcli 6602	. . . . 5 |- ((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))) e. RR
150		0re 6603	. . . . 5 |- 0 e. RR
151	149, 150, 131	lemul2i 7018	. . . 4 |- (0 < 4 -> (((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))) <_ 0 <-> (4 x. ((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) <_ (4 x. 0)))
152	148, 151	ax-mp 7	. . 3 |- (((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))) <_ 0 <-> (4 x. ((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))) <_ (4 x. 0))
153	147, 152	mpbir 207	. 2 |- ((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))) <_ 0
154		suble0 6864	. . 3 |- (((sum_k e. (1...N)((X` k) x. (Y` k))^2) e. RR /\ (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)) e. RR) -> (((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))) <_ 0 <-> (sum_k e. (1...N)((X` k) x. (Y` k))^2) <_ (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))))
155	133, 135, 154	mp2an 761	. 2 |- (((sum_k e. (1...N)((X` k) x. (Y` k))^2) - (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))) <_ 0 <-> (sum_k e. (1...N)((X` k) x. (Y` k))^2) <_ (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2)))
156	153, 155	mpbi 206	1 |- (sum_k e. (1...N)((X` k) x. (Y` k))^2) <_ (sum_k e. (1...N)((X` k)^2) x. sum_k e. (1...N)((Y` k)^2))

Syntax hints:   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105   class class class wbr 3338  -->wf 3994  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385  0cc0 6386  1c1 6387   + caddc 6389   x. cmul 6391   - cmin 6445   <_ cle 6448  NNcn 6449  NN0cn0 6450   < clt 6653  2c2 7145  4c4 7147  ZZ>=cuz 7586  ...cfz 7637  ^cexp 7811  sum_csu 8239

This theorem is referenced by:  trirni 15833

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-div 6892  df-n 7108  df-2 7154  df-3 7155  df-4 7156  df-n0 7309  df-z 7345  df-uz 7587  df-fz 7638  df-seq1 7721  df-shft 7754  df-seqz 7776  df-exp 7812  df-sum 8240

Copyright terms: Public domain