Theorem ax5seglem3

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

	Ref	Expression
Assertion	ax5seglem3	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ↑ 2 ) )

Proof

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