Theorem axsegcon

Description: Any segment A B can be extended to a point x such that B x is congruent to C D . Axiom A4 of Schwabhauser p. 11. (Contributed by Scott Fenton, 4-Jun-2013)

	Ref	Expression
Assertion	axsegcon	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		axsegconlem1	⊢ ( ( 𝐴 = 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
2	1	ex	⊢ ( 𝐴 = 𝐵 → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
3		simprll	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
4		simprlr	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
5		simpl	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → 𝐴 ≠ 𝐵 )
6		simprr	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) )
7		eqid	⊢ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
8		eqid	⊢ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
9		eqid	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) )
10	7 8 9	axsegconlem8	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
11	7 8	axsegconlem7	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ∈ ( 0 [,] 1 ) )
12	7 8 9	axsegconlem10	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) )
13	7 8 9	axsegconlem9	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
14		fveq1	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) )
15	14	oveq2d	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) )
16	15	oveq2d	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) )
17	16	eqeq2d	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ) )
18	17	ralbidv	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ) )
19	14	oveq2d	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) )
20	19	oveq1d	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) )
21	20	sumeq2sdv	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) )
22	21	eqeq1d	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
23	18 22	anbi12d	⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
24		oveq2	⊢ ( 𝑡 = ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( 1 − 𝑡 ) = ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) )
25	24	oveq1d	⊢ ( 𝑡 = ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) )
26		oveq1	⊢ ( 𝑡 = ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) = ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) )
27	25 26	oveq12d	⊢ ( 𝑡 = ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) = ( ( ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) )
28	27	eqeq2d	⊢ ( 𝑡 = ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ) )
29	28	ralbidv	⊢ ( 𝑡 = ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ) )
30	29	anbi1d	⊢ ( 𝑡 = ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
31	23 30	rspc2ev	⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ∈ ( 0 [,] 1 ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) / ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) + ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) ) ) ) ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
32	10 11 12 13 31	syl112anc	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
33	3 4 5 6 32	syl31anc	⊢ ( ( 𝐴 ≠ 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
34	33	ex	⊢ ( 𝐴 ≠ 𝐵 → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
35	2 34	pm2.61ine	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
36		simpllr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
37		simplll	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
38		simpr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
39		brbtwn	⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
40	36 37 38 39	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
41		simplrl	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
42		simplrr	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
43		brcgr	⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
44	36 38 41 42 43	syl22anc	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
45	40 44	anbi12d	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
46		r19.41v	⊢ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
47	45 46	bitr4di	⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
48	47	rexbidva	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
49	35 48	mpbird	⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )
50	49	3adant1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝐵 Btwn ⟨ 𝐴 , 𝑥 ⟩ ∧ ⟨ 𝐵 , 𝑥 ⟩ Cgr ⟨ 𝐶 , 𝐷 ⟩ ) )