ax5seglem6

Description: Lemma for ax5seg . Given two line segments that are divided into pieces, if the pieces are congruent, then the scaling constant is the same. (Contributed by Scott Fenton, 12-Jun-2013)

		Ref	Expression
	Assertion	ax5seglem6	$⊢ ((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 (A \neq B \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 = S$

Proof

Step	Hyp	Ref	Expression
1		simp22l	$⊢ ((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 (A \neq B \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]$
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		resqcl	$⊢ T \in ℝ \to T^{2} \in ℝ$
5	4	recnd	$⊢ T \in ℝ \to T^{2} \in ℂ$
6	1 3 5	3syl	$⊢ ((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 (A \neq B \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} \in ℂ$
7		simp22r	$⊢ ((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 (A \neq B \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]$
8		elicc01	$⊢ S \in [0, 1] \leftrightarrow (S \in ℝ \land 0 \leq S \land S \leq 1)$
9	8	simp1bi	$⊢ S \in [0, 1] \to S \in ℝ$
10		resqcl	$⊢ S \in ℝ \to S^{2} \in ℝ$
11	10	recnd	$⊢ S \in ℝ \to S^{2} \in ℂ$
12	7 9 11	3syl	$⊢ ((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 (A \neq B \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} \in ℂ$
13		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)))) \land (A \neq B \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 \dots N) \in Fin$
14		simprl1	$⊢ (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 A \in 𝔼 (N)$
15	14	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 (A \neq B \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)$
16		fveecn	$⊢ (A \in 𝔼 (N) \land j \in (1 \dots N)) \to A (j) \in ℂ$
17	15 16	sylan	$⊢ (((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 (A \neq B \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⟩)) \land j \in (1 \dots N)) \to A (j) \in ℂ$
18		simprl3	$⊢ (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 C \in 𝔼 (N)$
19	18	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 (A \neq B \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)$
20		fveecn	$⊢ (C \in 𝔼 (N) \land j \in (1 \dots N)) \to C (j) \in ℂ$
21	19 20	sylan	$⊢ (((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 (A \neq B \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⟩)) \land j \in (1 \dots N)) \to C (j) \in ℂ$
22	17 21	subcld	$⊢ (((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 (A \neq B \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⟩)) \land j \in (1 \dots N)) \to A (j) - C (j) \in ℂ$
23	22	sqcld	$⊢ (((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 (A \neq B \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⟩)) \land j \in (1 \dots N)) \to {(A (j) - C (j))}^{2} \in ℂ$
24	13 23	fsumcl	$⊢ ((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 (A \neq B \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} \in ℂ$
25		simp1l	$⊢ ((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 (A \neq B \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 ℕ$
26		simp1rl	$⊢ ((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 (A \neq B \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) \land B \in 𝔼 (N) \land C \in 𝔼 (N))$
27		simp21	$⊢ ((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 (A \neq B \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 \neq B$
28		simp23l	$⊢ ((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 (A \neq B \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)$
29		ax5seglem5	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (A \neq B \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) - C (j))}^{2} \neq 0$
30	25 26 27 1 28 29	syl23anc	$⊢ ((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 (A \neq B \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} \neq 0$
31		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 (A \neq B \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⟩$
32		simprl2	$⊢ (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 B \in 𝔼 (N)$
33		simprr1	$⊢ (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 D \in 𝔼 (N)$
34		simprr2	$⊢ (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 E \in 𝔼 (N)$
35		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})$
36	14 32 33 34 35	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 (⟨A, B⟩ Cgr ⟨D, E⟩ \leftrightarrow \sum_{j = 1}^{N} {(A (j) - B (j))}^{2} = \sum_{j = 1}^{N} {(D (j) - E (j))}^{2})$
37	36	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 (A \neq B \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})$
38	31 37	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 (A \neq B \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}$
39		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}$
40	25 15 19 1 28 39	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 (A \neq B \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}$
41	33	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 (A \neq B \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)$
42		simprr3	$⊢ (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 F \in 𝔼 (N)$
43	42	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 (A \neq B \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)$
44		simp23r	$⊢ ((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 (A \neq B \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)$
45		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}$
46	25 41 43 7 44 45	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 (A \neq B \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}$
47	38 40 46	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 (A \neq B \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}$
48		simp1rr	$⊢ ((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 (A \neq B \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) \land E \in 𝔼 (N) \land F \in 𝔼 (N))$
49		simp22	$⊢ ((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 (A \neq B \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] \land S \in [0, 1])$
50		simp23	$⊢ ((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 (A \neq B \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) \land \forall i \in (1 \dots N) E (i) = (1 - S) D (i) + S F (i))$
51		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 (A \neq B \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⟩$
52		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}$
53	25 26 48 49 50 31 51 52	syl322anc	$⊢ ((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 (A \neq B \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}$
54	53	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 (A \neq B \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} \sum_{j = 1}^{N} {(A (j) - C (j))}^{2} = S^{2} \sum_{j = 1}^{N} {(D (j) - F (j))}^{2}$
55	47 54	eqtr4d	$⊢ ((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 (A \neq B \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} {(A (j) - C (j))}^{2}$
56	6 12 24 30 55	mulcan2ad	$⊢ ((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 (A \neq B \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} = S^{2}$
57	2	simp2bi	$⊢ T \in [0, 1] \to 0 \leq T$
58	3 57	jca	$⊢ T \in [0, 1] \to (T \in ℝ \land 0 \leq T)$
59	1 58	syl	$⊢ ((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 (A \neq B \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 ℝ \land 0 \leq T)$
60	8	simp2bi	$⊢ S \in [0, 1] \to 0 \leq S$
61	9 60	jca	$⊢ S \in [0, 1] \to (S \in ℝ \land 0 \leq S)$
62	7 61	syl	$⊢ ((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 (A \neq B \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 ℝ \land 0 \leq S)$
63		sq11	$⊢ ((T \in ℝ \land 0 \leq T) \land (S \in ℝ \land 0 \leq S)) \to (T^{2} = S^{2} \leftrightarrow T = S)$
64	59 62 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)))) \land (A \neq B \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} = S^{2} \leftrightarrow T = S)$
65	56 64	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 (A \neq B \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 = S$

Metamath Proof Explorer

Theorem ax5seglem6

Proof