ax5seglem2

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

		Ref	Expression
	Assertion	ax5seglem2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} {(B (j) - C (j))}^{2} = {(1 - T)}^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$

Proof

Step	Hyp	Ref	Expression
1		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to A \in 𝔼 (N)$
2		fveecn	$⊢ (A \in 𝔼 (N) \land j \in (1 \dots N)) \to A (j) \in ℂ$
3	1 2	sylancom	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to A (j) \in ℂ$
4		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to C \in 𝔼 (N)$
5		fveecn	$⊢ (C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℂ$
6	4 5	sylancom	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to C (j) \in ℂ$
7		elicc01	$⊢ T \in [0, 1] \leftrightarrow (T \in ℝ \land 0 \leq T \land T \leq 1)$
8	7	simp1bi	$⊢ T \in [0, 1] \to T \in ℝ$
9	8	recnd	$⊢ T \in [0, 1] \to T \in ℂ$
10	9	adantr	$⊢ (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i)) \to T \in ℂ$
11	10	3ad2ant3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to T \in ℂ$
12	11	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to T \in ℂ$
13		fveq2	$⊢ i = j \to B (i) = B (j)$
14		fveq2	$⊢ i = j \to A (i) = A (j)$
15	14	oveq2d	$⊢ i = j \to (1 - T) A (i) = (1 - T) A (j)$
16		fveq2	$⊢ i = j \to C (i) = C (j)$
17	16	oveq2d	$⊢ i = j \to T C (i) = T C (j)$
18	15 17	oveq12d	$⊢ i = j \to (1 - T) A (i) + T C (i) = (1 - T) A (j) + T C (j)$
19	13 18	eqeq12d	$⊢ i = j \to (B (i) = (1 - T) A (i) + T C (i) \leftrightarrow B (j) = (1 - T) A (j) + T C (j))$
20	19	rspccva	$⊢ (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land j \in (1 \dots N)) \to B (j) = (1 - T) A (j) + T C (j)$
21	20	adantll	$⊢ ((T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i)) \land j \in (1 \dots N)) \to B (j) = (1 - T) A (j) + T C (j)$
22	21	3ad2antl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to B (j) = (1 - T) A (j) + T C (j)$
23		oveq1	$⊢ B (j) = (1 - T) A (j) + T C (j) \to B (j) - C (j) = (1 - T) A (j) + T C (j) - C (j)$
24	23	oveq1d	$⊢ B (j) = (1 - T) A (j) + T C (j) \to {(B (j) - C (j))}^{2} = {((1 - T) A (j) + T C (j) - C (j))}^{2}$
25		ax-1cn	$⊢ 1 \in ℂ$
26		subcl	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - T \in ℂ$
27	25 26	mpan	$⊢ T \in ℂ \to 1 - T \in ℂ$
28	27	3ad2ant3	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to 1 - T \in ℂ$
29		simp1	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to A (j) \in ℂ$
30	28 29	mulcld	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) A (j) \in ℂ$
31		simp3	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to T \in ℂ$
32		simp2	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to C (j) \in ℂ$
33	31 32	mulcld	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to T C (j) \in ℂ$
34	30 33 32	addsubassd	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) A (j) + T C (j) - C (j) = (1 - T) A (j) + T C (j) - C (j)$
35		subdi	$⊢ (1 - T \in ℂ \land A (j) \in ℂ \land C (j) \in ℂ) \to (1 - T) (A (j) - C (j)) = (1 - T) A (j) - (1 - T) C (j)$
36	27 35	syl3an1	$⊢ (T \in ℂ \land A (j) \in ℂ \land C (j) \in ℂ) \to (1 - T) (A (j) - C (j)) = (1 - T) A (j) - (1 - T) C (j)$
37	36	3coml	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) (A (j) - C (j)) = (1 - T) A (j) - (1 - T) C (j)$
38		subdir	$⊢ (1 \in ℂ \land T \in ℂ \land C (j) \in ℂ) \to (1 - T) C (j) = 1 C (j) - T C (j)$
39	25 38	mp3an1	$⊢ (T \in ℂ \land C (j) \in ℂ) \to (1 - T) C (j) = 1 C (j) - T C (j)$
40	39	ancoms	$⊢ (C (j) \in ℂ \land T \in ℂ) \to (1 - T) C (j) = 1 C (j) - T C (j)$
41	40	3adant1	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) C (j) = 1 C (j) - T C (j)$
42		mullid	$⊢ C (j) \in ℂ \to 1 C (j) = C (j)$
43	42	oveq1d	$⊢ C (j) \in ℂ \to 1 C (j) - T C (j) = C (j) - T C (j)$
44	43	3ad2ant2	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to 1 C (j) - T C (j) = C (j) - T C (j)$
45	41 44	eqtrd	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) C (j) = C (j) - T C (j)$
46	45	oveq2d	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) A (j) - (1 - T) C (j) = (1 - T) A (j) - (C (j) - T C (j))$
47	30 32 33	subsub2d	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) A (j) - (C (j) - T C (j)) = (1 - T) A (j) + T C (j) - C (j)$
48	37 46 47	3eqtrd	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) (A (j) - C (j)) = (1 - T) A (j) + T C (j) - C (j)$
49	34 48	eqtr4d	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to (1 - T) A (j) + T C (j) - C (j) = (1 - T) (A (j) - C (j))$
50	49	oveq1d	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to {((1 - T) A (j) + T C (j) - C (j))}^{2} = {(1 - T) (A (j) - C (j))}^{2}$
51		subcl	$⊢ (A (j) \in ℂ \land C (j) \in ℂ) \to A (j) - C (j) \in ℂ$
52	51	3adant3	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to A (j) - C (j) \in ℂ$
53	28 52	sqmuld	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to {(1 - T) (A (j) - C (j))}^{2} = {(1 - T)}^{2} {(A (j) - C (j))}^{2}$
54	50 53	eqtrd	$⊢ (A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \to {((1 - T) A (j) + T C (j) - C (j))}^{2} = {(1 - T)}^{2} {(A (j) - C (j))}^{2}$
55	24 54	sylan9eqr	$⊢ ((A (j) \in ℂ \land C (j) \in ℂ \land T \in ℂ) \land B (j) = (1 - T) A (j) + T C (j)) \to {(B (j) - C (j))}^{2} = {(1 - T)}^{2} {(A (j) - C (j))}^{2}$
56	3 6 12 22 55	syl31anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to {(B (j) - C (j))}^{2} = {(1 - T)}^{2} {(A (j) - C (j))}^{2}$
57	56	sumeq2dv	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} {(B (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(1 - T)}^{2} {(A (j) - C (j))}^{2}$
58		fzfid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to (1 \dots N) \in Fin$
59		1re	$⊢ 1 \in ℝ$
60		resubcl	$⊢ (1 \in ℝ \land T \in ℝ) \to 1 - T \in ℝ$
61	59 8 60	sylancr	$⊢ T \in [0, 1] \to 1 - T \in ℝ$
62	61	resqcld	$⊢ T \in [0, 1] \to {(1 - T)}^{2} \in ℝ$
63	62	recnd	$⊢ T \in [0, 1] \to {(1 - T)}^{2} \in ℂ$
64	63	adantr	$⊢ (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i)) \to {(1 - T)}^{2} \in ℂ$
65	64	3ad2ant3	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to {(1 - T)}^{2} \in ℂ$
66	2	3adant1	$⊢ (N \in ℕ \land A \in 𝔼 (N) \land j \in (1 \dots N)) \to A (j) \in ℂ$
67	66	3adant2r	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to A (j) \in ℂ$
68	5	3adant1	$⊢ (N \in ℕ \land C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℂ$
69	68	3adant2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to C (j) \in ℂ$
70	67 69	subcld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to A (j) - C (j) \in ℂ$
71	70	sqcld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℂ$
72	71	3expa	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N))) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℂ$
73	72	3adantl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℂ$
74	58 65 73	fsummulc2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to {(1 - T)}^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(1 - T)}^{2} {(A (j) - C (j))}^{2}$
75	57 74	eqtr4d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land C \in 𝔼 (N)) \land (T \in [0, 1] \land \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i))) \to \sum_{j = 1}^{N} {(B (j) - C (j))}^{2} = {(1 - T)}^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$

Metamath Proof Explorer

Theorem ax5seglem2

Proof