ax5seglem3

Description: Lemma for ax5seg . Combine congruences for points on a line. (Contributed by Scott Fenton, 11-Jun-2013)

		Ref	Expression
	Assertion	ax5seglem3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$

Proof

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		elicc01	$⊢ T \in [0, 1] \leftrightarrow (T \in ℝ \land 0 \leq T \land T \leq 1)$
3	2	simp1bi	$⊢ T \in [0, 1] \to T \in ℝ$
4		resubcl	$⊢ (1 \in ℝ \land T \in ℝ) \to 1 - T \in ℝ$
5	1 3 4	sylancr	$⊢ T \in [0, 1] \to 1 - T \in ℝ$
6	5	ad2antrr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to 1 - T \in ℝ$
7	6	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 1 - T \in ℝ$
8		fzfid	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (1 \dots N) \in Fin$
9		ax5seglem3a	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land j \in (1 \dots N)) \to (A (j) - C (j) \in ℝ \land D (j) - F (j) \in ℝ)$
10	9	simpld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land j \in (1 \dots N)) \to A (j) - C (j) \in ℝ$
11	10	resqcld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℝ$
12	8 11	fsumrecl	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} \in ℝ$
13	10	sqge0d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land j \in (1 \dots N)) \to 0 \leq {(A (j) - C (j))}^{2}$
14	8 11 13	fsumge0	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to 0 \leq \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
15	12 14	resqrtcld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} \in ℝ$
16	15	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} \in ℝ$
17	7 16	remulcld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} \in ℝ$
18		elicc01	$⊢ S \in [0, 1] \leftrightarrow (S \in ℝ \land 0 \leq S \land S \leq 1)$
19	18	simp1bi	$⊢ S \in [0, 1] \to S \in ℝ$
20		resubcl	$⊢ (1 \in ℝ \land S \in ℝ) \to 1 - S \in ℝ$
21	1 19 20	sylancr	$⊢ S \in [0, 1] \to 1 - S \in ℝ$
22	21	ad2antlr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to 1 - S \in ℝ$
23	22	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 1 - S \in ℝ$
24	9	simprd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land j \in (1 \dots N)) \to D (j) - F (j) \in ℝ$
25	24	resqcld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land j \in (1 \dots N)) \to {(D (j) - F (j))}^{2} \in ℝ$
26	8 25	fsumrecl	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to \sum_{j = 1}^{N} {(D (j) - F (j))}^{2} \in ℝ$
27	24	sqge0d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land j \in (1 \dots N)) \to 0 \leq {(D (j) - F (j))}^{2}$
28	8 25 27	fsumge0	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to 0 \leq \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
29	26 28	resqrtcld	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \in ℝ$
30	29	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \in ℝ$
31	23 30	remulcld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \in ℝ$
32	2	simp3bi	$⊢ T \in [0, 1] \to T \leq 1$
33		subge0	$⊢ (1 \in ℝ \land T \in ℝ) \to (0 \leq 1 - T \leftrightarrow T \leq 1)$
34	1 3 33	sylancr	$⊢ T \in [0, 1] \to (0 \leq 1 - T \leftrightarrow T \leq 1)$
35	32 34	mpbird	$⊢ T \in [0, 1] \to 0 \leq 1 - T$
36	35	ad2antrr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to 0 \leq 1 - T$
37	36	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq 1 - T$
38	12 14	sqrtge0d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to 0 \leq \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
39	38	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
40	7 16 37 39	mulge0d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq (1 - T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
41	18	simp3bi	$⊢ S \in [0, 1] \to S \leq 1$
42		subge0	$⊢ (1 \in ℝ \land S \in ℝ) \to (0 \leq 1 - S \leftrightarrow S \leq 1)$
43	1 19 42	sylancr	$⊢ S \in [0, 1] \to (0 \leq 1 - S \leftrightarrow S \leq 1)$
44	41 43	mpbird	$⊢ S \in [0, 1] \to 0 \leq 1 - S$
45	44	ad2antlr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to 0 \leq 1 - S$
46	45	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq 1 - S$
47	26 28	sqrtge0d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to 0 \leq \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
48	47	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
49	23 30 46 48	mulge0d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq (1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
50		resqrtth	$⊢ (\sum_{j = 1}^{N} {(A (j) - C (j))}^{2} \in ℝ \land 0 \leq \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}) \to {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
51	12 14 50	syl2anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
52	51	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
53	52	oveq2d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {(1 - T)}^{2} {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = {(1 - T)}^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
54		ax-1cn	$⊢ 1 \in ℂ$
55	3	recnd	$⊢ T \in [0, 1] \to T \in ℂ$
56	55	ad2antrr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to T \in ℂ$
57	56	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to T \in ℂ$
58		subcl	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - T \in ℂ$
59	54 57 58	sylancr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 1 - T \in ℂ$
60	15	recnd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} \in ℂ$
61	60	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} \in ℂ$
62	59 61	sqmuld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {(1 - T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = {(1 - T)}^{2} {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2}$
63		resqrtth	$⊢ (\sum_{j = 1}^{N} {(D (j) - F (j))}^{2} \in ℝ \land 0 \leq \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}) \to {\sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
64	26 28 63	syl2anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to {\sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
65	64	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {\sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
66	65	oveq2d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {(1 - S)}^{2} {\sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = {(1 - S)}^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
67	19	recnd	$⊢ S \in [0, 1] \to S \in ℂ$
68	67	ad2antlr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to S \in ℂ$
69	68	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to S \in ℂ$
70		subcl	$⊢ (1 \in ℂ \land S \in ℂ) \to 1 - S \in ℂ$
71	54 69 70	sylancr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 1 - S \in ℂ$
72	29	recnd	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \in ℂ$
73	72	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \in ℂ$
74	71 73	sqmuld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {(1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = {(1 - S)}^{2} {\sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2}$
75		simp3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨B, C⟩ Cgr ⟨E, F⟩$
76		simp122	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to B \in 𝔼 (N)$
77		simp123	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to C \in 𝔼 (N)$
78		simp132	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to E \in 𝔼 (N)$
79		simp133	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to F \in 𝔼 (N)$
80		brcgr	$⊢ ((B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (⟨B, C⟩ Cgr ⟨E, F⟩ \leftrightarrow \sum_{j = 1}^{N} {(B (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - F (j))}^{2})$
81	76 77 78 79 80	syl22anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (⟨B, C⟩ Cgr ⟨E, F⟩ \leftrightarrow \sum_{j = 1}^{N} {(B (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - F (j))}^{2})$
82	75 81	mpbid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(B (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(E (j) - F (j))}^{2}$
83		simp11	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to N \in ℕ$
84		simp121	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to A \in 𝔼 (N)$
85		simp2ll	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to T \in [0, 1]$
86		simp2rl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i)$
87		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}$
88	83 84 77 85 86 87	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(B (j) - C (j))}^{2} = {(1 - T)}^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
89		simp131	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to D \in 𝔼 (N)$
90		simp2lr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to S \in [0, 1]$
91		simp2rr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i)$
92		ax5seglem2	$⊢ (N \in ℕ \land (D \in 𝔼 (N) \land F \in 𝔼 (N)) \land (S \in [0, 1] \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to \sum_{j = 1}^{N} {(E (j) - F (j))}^{2} = {(1 - S)}^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
93	83 89 79 90 91 92	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(E (j) - F (j))}^{2} = {(1 - S)}^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
94	82 88 93	3eqtr3d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {(1 - T)}^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = {(1 - S)}^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
95	66 74 94	3eqtr4d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {(1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = {(1 - T)}^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
96	53 62 95	3eqtr4d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {(1 - T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = {(1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2}$
97	17 31 40 49 96	sq11d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = (1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
98	3	ad2antrr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to T \in ℝ$
99	98	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to T \in ℝ$
100	99 16	remulcld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to T \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} \in ℝ$
101	19	ad2antlr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to S \in ℝ$
102	101	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to S \in ℝ$
103	102 30	remulcld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \in ℝ$
104	2	simp2bi	$⊢ T \in [0, 1] \to 0 \leq T$
105	104	ad2antrr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to 0 \leq T$
106	105	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq T$
107	99 16 106 39	mulge0d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq T \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
108	18	simp2bi	$⊢ S \in [0, 1] \to 0 \leq S$
109	108	ad2antlr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to 0 \leq S$
110	109	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq S$
111	102 30 110 48	mulge0d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 0 \leq S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
112	51	oveq2d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to T^{2} {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
113	112	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to T^{2} {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
114	57 61	sqmuld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {T \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = T^{2} {\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2}$
115	65	oveq2d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to S^{2} {\sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = S^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
116	69 73	sqmuld	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = S^{2} {\sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2}$
117		simp3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to ⟨A, B⟩ Cgr ⟨D, E⟩$
118		brcgr	$⊢ ((A \in 𝔼 (N) \land B \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N))) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow \sum_{j = 1}^{N} {(A (j) - B (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - E (j))}^{2})$
119	84 76 89 78 118	syl22anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow \sum_{j = 1}^{N} {(A (j) - B (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - E (j))}^{2})$
120	117 119	mpbid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(A (j) - B (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - E (j))}^{2}$
121		ax5seglem1	$⊢ (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} {(A (j) - B (j))}^{2} = T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
122	83 84 77 85 86 121	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(A (j) - B (j))}^{2} = T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
123		ax5seglem1	$⊢ (N \in ℕ \land (D \in 𝔼 (N) \land F \in 𝔼 (N)) \land (S \in [0, 1] \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to \sum_{j = 1}^{N} {(D (j) - E (j))}^{2} = S^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
124	83 89 79 90 91 123	syl122anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(D (j) - E (j))}^{2} = S^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
125	120 122 124	3eqtr3d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = S^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
126	115 116 125	3eqtr4d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2} = T^{2} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}$
127	113 114 126	3eqtr4d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to {T \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}}^{2} = {S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}}^{2}$
128	100 103 107 111 127	sq11d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to T \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
129	97 128	oveq12d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} + T \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = (1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} + S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
130	59 57 61	adddird	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - T + T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = (1 - T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} + T \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
131	71 69 73	adddird	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - S + S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} = (1 - S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} + S \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
132	129 130 131	3eqtr4d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - T + T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = (1 - S + S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
133		npcan	$⊢ (1 \in ℂ \land T \in ℂ) \to 1 - T + T = 1$
134	54 55 133	sylancr	$⊢ T \in [0, 1] \to 1 - T + T = 1$
135	134	adantr	$⊢ (T \in [0, 1] \land S \in [0, 1]) \to 1 - T + T = 1$
136	135	oveq1d	$⊢ (T \in [0, 1] \land S \in [0, 1]) \to (1 - T + T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = 1 \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
137	136	adantr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to (1 - T + T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = 1 \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
138	137	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - T + T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = 1 \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
139	60	mulid2d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to 1 \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
140	139	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 1 \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
141	138 140	eqtrd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - T + T) \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}}$
142		npcan	$⊢ (1 \in ℂ \land S \in ℂ) \to 1 - S + S = 1$
143	54 67 142	sylancr	$⊢ S \in [0, 1] \to 1 - S + S = 1$
144	143	oveq1d	$⊢ S \in [0, 1] \to (1 - S + S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} = 1 \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
145	144	ad2antlr	$⊢ ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \to (1 - S + S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} = 1 \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
146	145	3ad2ant2	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - S + S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} = 1 \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
147	72	mulid2d	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to 1 \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
148	147	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to 1 \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
149	146 148	eqtrd	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (1 - S + S) \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
150	132 141 149	3eqtr3d	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}}$
151		sqrt11	$⊢ ((\sum_{j = 1}^{N} {(A (j) - C (j))}^{2} \in ℝ \land 0 \leq \sum_{j = 1}^{N} {(A (j) - C (j))}^{2}) \land (\sum_{j = 1}^{N} {(D (j) - F (j))}^{2} \in ℝ \land 0 \leq \sum_{j = 1}^{N} {(D (j) - F (j))}^{2})) \to (\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \leftrightarrow \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2})$
152	12 14 26 28 151	syl22anc	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \to (\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \leftrightarrow \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2})$
153	152	3ad2ant1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to (\sqrt{\sum_{j = 1}^{N} {(A (j) - C (j))}^{2}} = \sqrt{\sum_{j = 1}^{N} {(D (j) - F (j))}^{2}} \leftrightarrow \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2})$
154	150 153	mpbid	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N)) \land (D \in 𝔼 (N) \land E \in 𝔼 (N) \land F \in 𝔼 (N))) \land ((T \in [0, 1] \land S \in [0, 1]) \land (\forall i \in (1 \dots N) B (i) = (1 - T) A (i) + T C (i) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))) \land (⟨A, B⟩ Cgr ⟨D, E⟩ \land ⟨B, C⟩ Cgr ⟨E, F⟩)) \to \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$

Metamath Proof Explorer

Theorem ax5seglem3

Proof