Metamath Proof Explorer

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 ) )