Theorem ax5seglem2 25772

Description: Lemma for ax5seg 25781. Rexpress another congruence sum given betweenness. (Contributed by Scott Fenton, 11-Jun-2013.)

Assertion

Ref	Expression
ax5seglem2	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )

Distinct variable groups:   A, i, j   B, i, j   C, i, j   i, N, j   T, i, j

Proof of Theorem ax5seglem2

Step	Hyp	Ref	Expression
1		simpl2l 1010	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> A e. ( EE ` N ) )
2		fveecn 25745	. . . . 5 |- ( ( A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
3	1, 2	sylancom 649	. . . 4 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
4		simpl2r 1011	. . . . 5 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> C e. ( EE ` N ) )
5		fveecn 25745	. . . . 5 |- ( ( C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
6	4, 5	sylancom 649	. . . 4 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
7		0re 9047	. . . . . . . . . 10 |- 0 e. RR
8		1re 9046	. . . . . . . . . 10 |- 1 e. RR
9	7, 8	elicc2i 10932	. . . . . . . . 9 |- ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
10	9	simp1bi 972	. . . . . . . 8 |- ( T e. ( 0 [,] 1 ) -> T e. RR )
11	10	recnd 9070	. . . . . . 7 |- ( T e. ( 0 [,] 1 ) -> T e. CC )
12	11	adantr 452	. . . . . 6 |- ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> T e. CC )
13	12	3ad2ant3 980	. . . . 5 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> T e. CC )
14	13	adantr 452	. . . 4 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> T e. CC )
15		fveq2 5687	. . . . . . . 8 |- ( i = j -> ( B ` i ) = ( B ` j ) )
16		fveq2 5687	. . . . . . . . . 10 |- ( i = j -> ( A ` i ) = ( A ` j ) )
17	16	oveq2d 6056	. . . . . . . . 9 |- ( i = j -> ( ( 1 - T ) x. ( A ` i ) ) = ( ( 1 - T ) x. ( A ` j ) ) )
18		fveq2 5687	. . . . . . . . . 10 |- ( i = j -> ( C ` i ) = ( C ` j ) )
19	18	oveq2d 6056	. . . . . . . . 9 |- ( i = j -> ( T x. ( C ` i ) ) = ( T x. ( C ` j ) ) )
20	17, 19	oveq12d 6058	. . . . . . . 8 |- ( i = j -> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
21	15, 20	eqeq12d 2418	. . . . . . 7 |- ( i = j -> ( ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) <-> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) )
22	21	rspccva 3011	. . . . . 6 |- ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
23	22	adantll 695	. . . . 5 |- ( ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
24	23	3ad2antl3 1121	. . . 4 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) )
25		oveq1 6047	. . . . . 6 |- ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( B ` j ) - ( C ` j ) ) = ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) )
26	25	oveq1d 6055	. . . . 5 |- ( ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) -> ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) ^ 2 ) )
27		ax-1cn 9004	. . . . . . . . . . . 12 |- 1 e. CC
28		subcl 9261	. . . . . . . . . . . 12 |- ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
29	27, 28	mpan 652	. . . . . . . . . . 11 |- ( T e. CC -> ( 1 - T ) e. CC )
30	29	3ad2ant3 980	. . . . . . . . . 10 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
31		simp1 957	. . . . . . . . . 10 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( A ` j ) e. CC )
32	30, 31	mulcld 9064	. . . . . . . . 9 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( A ` j ) ) e. CC )
33		simp3 959	. . . . . . . . . 10 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> T e. CC )
34		simp2 958	. . . . . . . . . 10 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( C ` j ) e. CC )
35	33, 34	mulcld 9064	. . . . . . . . 9 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( T x. ( C ` j ) ) e. CC )
36	32, 35, 34	addsubassd 9387	. . . . . . . 8 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( ( T x. ( C ` j ) ) - ( C ` j ) ) ) )
37		subdi 9423	. . . . . . . . . . 11 |- ( ( ( 1 - T ) e. CC /\ ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) )
38	29, 37	syl3an1 1217	. . . . . . . . . 10 |- ( ( T e. CC /\ ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) )
39	38	3coml 1160	. . . . . . . . 9 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) )
40		subdir 9424	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ T e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) )
41	27, 40	mp3an1 1266	. . . . . . . . . . . . 13 |- ( ( T e. CC /\ ( C ` j ) e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) )
42	41	ancoms 440	. . . . . . . . . . . 12 |- ( ( ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) )
43	42	3adant1 975	. . . . . . . . . . 11 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) )
44		mulid2 9045	. . . . . . . . . . . . 13 |- ( ( C ` j ) e. CC -> ( 1 x. ( C ` j ) ) = ( C ` j ) )
45	44	oveq1d 6055	. . . . . . . . . . . 12 |- ( ( C ` j ) e. CC -> ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) = ( ( C ` j ) - ( T x. ( C ` j ) ) ) )
46	45	3ad2ant2 979	. . . . . . . . . . 11 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 x. ( C ` j ) ) - ( T x. ( C ` j ) ) ) = ( ( C ` j ) - ( T x. ( C ` j ) ) ) )
47	43, 46	eqtrd 2436	. . . . . . . . . 10 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( C ` j ) ) = ( ( C ` j ) - ( T x. ( C ` j ) ) ) )
48	47	oveq2d 6056	. . . . . . . . 9 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( 1 - T ) x. ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( C ` j ) - ( T x. ( C ` j ) ) ) ) )
49	32, 34, 35	subsub2d 9396	. . . . . . . . 9 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) x. ( A ` j ) ) - ( ( C ` j ) - ( T x. ( C ` j ) ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( ( T x. ( C ` j ) ) - ( C ` j ) ) ) )
50	39, 48, 49	3eqtrd 2440	. . . . . . . 8 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( ( T x. ( C ` j ) ) - ( C ` j ) ) ) )
51	36, 50	eqtr4d 2439	. . . . . . 7 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) = ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) )
52	51	oveq1d 6055	. . . . . 6 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) ^ 2 ) )
53		subcl 9261	. . . . . . . 8 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
54	53	3adant3 977	. . . . . . 7 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
55	30, 54	sqmuld 11490	. . . . . 6 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) x. ( ( A ` j ) - ( C ` j ) ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
56	52, 55	eqtrd 2436	. . . . 5 |- ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) -> ( ( ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
57	26, 56	sylan9eqr 2458	. . . 4 |- ( ( ( ( A ` j ) e. CC /\ ( C ` j ) e. CC /\ T e. CC ) /\ ( B ` j ) = ( ( ( 1 - T ) x. ( A ` j ) ) + ( T x. ( C ` j ) ) ) ) -> ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
58	3, 6, 14, 24, 57	syl31anc 1187	. . 3 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
59	58	sumeq2dv 12452	. 2 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = sum_ j e. ( 1 ... N ) ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
60		fzfid 11267	. . 3 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( 1 ... N ) e. Fin )
61		resubcl 9321	. . . . . . . 8 |- ( ( 1 e. RR /\ T e. RR ) -> ( 1 - T ) e. RR )
62	8, 10, 61	sylancr 645	. . . . . . 7 |- ( T e. ( 0 [,] 1 ) -> ( 1 - T ) e. RR )
63	62	resqcld 11504	. . . . . 6 |- ( T e. ( 0 [,] 1 ) -> ( ( 1 - T ) ^ 2 ) e. RR )
64	63	recnd 9070	. . . . 5 |- ( T e. ( 0 [,] 1 ) -> ( ( 1 - T ) ^ 2 ) e. CC )
65	64	adantr 452	. . . 4 |- ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> ( ( 1 - T ) ^ 2 ) e. CC )
66	65	3ad2ant3 980	. . 3 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( ( 1 - T ) ^ 2 ) e. CC )
67	2	3adant1 975	. . . . . . . 8 |- ( ( N e. NN /\ A e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
68	67	3adant2r 1179	. . . . . . 7 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( A ` j ) e. CC )
69	5	3adant1 975	. . . . . . . 8 |- ( ( N e. NN /\ C e. ( EE ` N ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
70	69	3adant2l 1178	. . . . . . 7 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( C ` j ) e. CC )
71	68, 70	subcld 9367	. . . . . 6 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( ( A ` j ) - ( C ` j ) ) e. CC )
72	71	sqcld 11476	. . . . 5 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
73	72	3expa 1153	. . . 4 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
74	73	3adantl3 1115	. . 3 |- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) /\ j e. ( 1 ... N ) ) -> ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) e. CC )
75	60, 66, 74	fsummulc2 12522	. 2 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) = sum_ j e. ( 1 ... N ) ( ( ( 1 - T ) ^ 2 ) x. ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )
76	59, 75	eqtr4d 2439	1 |- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( B ` j ) - ( C ` j ) ) ^ 2 ) = ( ( ( 1 - T ) ^ 2 ) x. sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) ) )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   class class class wbr 4172   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   <_ cle 9077   - cmin 9247   NNcn 9956   2c2 10005   [,]cicc 10875   ...cfz 10999   ^cexp 11337   sum_csu 12434   EEcee 25731

This theorem is referenced by:  ax5seglem3  25774

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-icc 10879  df-fz 11000  df-fzo 11091  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435  df-ee 25734