ax5seglem6

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

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

Proof

Step	Hyp	Ref	Expression
1		simp22l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝑇 ∈ ( 0 [,] 1 ) )
2		elicc01	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) ↔ ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ∧ 𝑇 ≤ 1 ) )
3	2	simp1bi	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 𝑇 ∈ ℝ )
4		resqcl	⊢ ( 𝑇 ∈ ℝ → ( 𝑇 ↑ 2 ) ∈ ℝ )
5	4	recnd	⊢ ( 𝑇 ∈ ℝ → ( 𝑇 ↑ 2 ) ∈ ℂ )
6	1 3 5	3syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝑇 ↑ 2 ) ∈ ℂ )
7		simp22r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝑆 ∈ ( 0 [,] 1 ) )
8		elicc01	⊢ ( 𝑆 ∈ ( 0 [,] 1 ) ↔ ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ∧ 𝑆 ≤ 1 ) )
9	8	simp1bi	⊢ ( 𝑆 ∈ ( 0 [,] 1 ) → 𝑆 ∈ ℝ )
10		resqcl	⊢ ( 𝑆 ∈ ℝ → ( 𝑆 ↑ 2 ) ∈ ℝ )
11	10	recnd	⊢ ( 𝑆 ∈ ℝ → ( 𝑆 ↑ 2 ) ∈ ℂ )
12	7 9 11	3syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝑆 ↑ 2 ) ∈ ℂ )
13		fzfid	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 1 ... 𝑁 ) ∈ Fin )
14		simprl1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
15	14	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
16		fveecn	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
17	15 16	sylan	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) ∈ ℂ )
18		simprl3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
19	18	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
20		fveecn	⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
21	19 20	sylan	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑗 ) ∈ ℂ )
22	17 21	subcld	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ∈ ℂ )
23	22	sqcld	⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) ∧ 𝑗 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
24	13 23	fsumcl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ∈ ℂ )
25		simp1l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝑁 ∈ ℕ )
26		simp1rl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) )
27		simp21	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝐴 ≠ 𝐵 )
28		simp23l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) )
29		ax5seglem5	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ≠ 0 )
30	25 26 27 1 28 29	syl23anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ≠ 0 )
31		simp3l	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ )
32		simprl2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
33		simprr1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
34		simprr2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
35		brcgr	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ↔ Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐸 ‘ 𝑗 ) ) ↑ 2 ) ) )
36	14 32 33 34 35	syl22anc	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ↔ Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐸 ‘ 𝑗 ) ) ↑ 2 ) ) )
37	36	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ↔ Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐸 ‘ 𝑗 ) ) ↑ 2 ) ) )
38	31 37	mpbid	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐸 ‘ 𝑗 ) ) ↑ 2 ) )
39		ax5seglem1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
40	25 15 19 1 28 39	syl122anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐵 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑇 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
41	33	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
42		simprr3	⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
43	42	3ad2ant1	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
44		simp23r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) )
45		ax5seglem1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑆 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐸 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ↑ 2 ) ) )
46	25 41 43 7 44 45	syl122anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐸 ‘ 𝑗 ) ) ↑ 2 ) = ( ( 𝑆 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ↑ 2 ) ) )
47	38 40 46	3eqtr3d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( ( 𝑇 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) = ( ( 𝑆 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ↑ 2 ) ) )
48		simp1rr	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) )
49		simp22	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) )
50		simp23	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) )
51		simp3r	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ )
52		ax5seglem3	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ↑ 2 ) )
53	25 26 48 49 50 31 51 52	syl322anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ↑ 2 ) )
54	53	oveq2d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( ( 𝑆 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) = ( ( 𝑆 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐷 ‘ 𝑗 ) − ( 𝐹 ‘ 𝑗 ) ) ↑ 2 ) ) )
55	47 54	eqtr4d	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( ( 𝑇 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) = ( ( 𝑆 ↑ 2 ) · Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑗 ) − ( 𝐶 ‘ 𝑗 ) ) ↑ 2 ) ) )
56	6 12 24 30 55	mulcan2ad	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝑇 ↑ 2 ) = ( 𝑆 ↑ 2 ) )
57	2	simp2bi	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑇 )
58	3 57	jca	⊢ ( 𝑇 ∈ ( 0 [,] 1 ) → ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ) )
59	1 58	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ) )
60	8	simp2bi	⊢ ( 𝑆 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑆 )
61	9 60	jca	⊢ ( 𝑆 ∈ ( 0 [,] 1 ) → ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) )
62	7 61	syl	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) )
63		sq11	⊢ ( ( ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ) ∧ ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) ) → ( ( 𝑇 ↑ 2 ) = ( 𝑆 ↑ 2 ) ↔ 𝑇 = 𝑆 ) )
64	59 62 63	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → ( ( 𝑇 ↑ 2 ) = ( 𝑆 ↑ 2 ) ↔ 𝑇 = 𝑆 ) )
65	56 64	mpbid	⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ ( 𝑇 ∈ ( 0 [,] 1 ) ∧ 𝑆 ∈ ( 0 [,] 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑇 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑆 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑆 · ( 𝐹 ‘ 𝑖 ) ) ) ) ) ∧ ( ⟨ 𝐴 , 𝐵 ⟩ Cgr ⟨ 𝐷 , 𝐸 ⟩ ∧ ⟨ 𝐵 , 𝐶 ⟩ Cgr ⟨ 𝐸 , 𝐹 ⟩ ) ) → 𝑇 = 𝑆 )

Metamath Proof Explorer

Theorem ax5seglem6

Proof