Metamath Proof Explorer

Theorem axsegconlem1

Description: Lemma for axsegcon . Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013)

Ref Expression
Assertion axsegconlem1 ( ( 𝐴 = 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )

Proof

Step Hyp Ref Expression
1 fveere ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
2 1 3ad2antl1 ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
3 fveere ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℝ )
4 3 3ad2antl2 ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℝ )
5 fveere ⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ ℝ )
6 5 3ad2antl3 ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ ℝ )
7 4 6 resubcld ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ∈ ℝ )
8 2 7 resubcld ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℝ )
9 8 ralrimiva ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℝ )
10 eleenn ⊢ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
11 mptelee ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℝ ) )
12 10 11 syl ⊢ ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℝ ) )
13 12 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ∈ ℝ ) )
14 9 13 mpbird ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
15 fveecn ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
16 15 3ad2antl1 ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
17 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
18 17 3ad2antl2 ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
19 fveecn ⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑖 ) ∈ ℂ )
20 19 3ad2antl3 ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐷 ‘ 𝑖 ) ∈ ℂ )
21 1m0e1 ⊢ ( 1 − 0 ) = 1
22 21 oveq1i ⊢ ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) = ( 1 · ( 𝐵 ‘ 𝑖 ) )
23 mulid2 ⊢ ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝐵 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
24 23 3ad2ant1 ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( 1 · ( 𝐵 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
25 22 24 eqtrid ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
26 subcl ⊢ ( ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ∈ ℂ )
27 subcl ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ∈ ℂ ) → ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ∈ ℂ )
28 26 27 sylan2 ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ∈ ℂ )
29 28 3impb ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ∈ ℂ )
30 29 mul02d ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) = 0 )
31 25 30 oveq12d ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) = ( ( 𝐵 ‘ 𝑖 ) + 0 ) )
32 addid1 ⊢ ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ → ( ( 𝐵 ‘ 𝑖 ) + 0 ) = ( 𝐵 ‘ 𝑖 ) )
33 32 3ad2ant1 ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝐵 ‘ 𝑖 ) + 0 ) = ( 𝐵 ‘ 𝑖 ) )
34 31 33 eqtr2d ⊢ ( ( ( 𝐵 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℂ ) → ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) )
35 16 18 20 34 syl3anc ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) )
36 35 ralrimiva ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) )
37 18 20 subcld ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ∈ ℂ )
38 16 37 nncand ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) = ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) )
39 38 oveq1d ⊢ ( ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
40 39 sumeq2dv ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
41 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
42 fveq1 ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) )
43 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑖 ) )
44 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑖 ) )
45 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐷 ‘ 𝑘 ) = ( 𝐷 ‘ 𝑖 ) )
46 44 45 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) = ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) )
47 43 46 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) )
48 eqid ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) )
49 ovex ⊢ ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ∈ V
50 47 48 49 fvmpt ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) )
51 42 50 sylan9eq ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) )
52 51 oveq2d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) )
53 52 oveq2d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) )
54 53 eqeq2d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ) )
55 54 ralbidva ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ) )
56 51 oveq2d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) )
57 56 oveq1d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) )
58 57 sumeq2dv ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) )
59 58 eqeq1d ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
60 55 59 anbi12d ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
61 oveq2 ⊢ ( 𝑡 = 0 → ( 1 − 𝑡 ) = ( 1 − 0 ) )
62 61 oveq1d ⊢ ( 𝑡 = 0 → ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) = ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) )
63 oveq1 ⊢ ( 𝑡 = 0 → ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) = ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) )
64 62 63 oveq12d ⊢ ( 𝑡 = 0 → ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) )
65 64 eqeq2d ⊢ ( 𝑡 = 0 → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ) )
66 65 ralbidv ⊢ ( 𝑡 = 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ) )
67 66 anbi1d ⊢ ( 𝑡 = 0 → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
68 60 67 rspc2ev ⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ 0 ∈ ( 0 [,] 1 ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
69 41 68 mp3an2 ⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( 𝐵 ‘ 𝑘 ) − ( ( 𝐶 ‘ 𝑘 ) − ( 𝐷 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 0 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 0 · ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐵 ‘ 𝑖 ) − ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
70 14 36 40 69 syl12anc ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
71 70 3expb ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
72 71 adantll ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )
73 fveq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑖 ) )
74 73 oveq2d ⊢ ( 𝐴 = 𝐵 → ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) )
75 74 oveq1d ⊢ ( 𝐴 = 𝐵 → ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) )
76 75 eqeq2d ⊢ ( 𝐴 = 𝐵 → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
77 76 ralbidv ⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
78 77 anbi1d ⊢ ( 𝐴 = 𝐵 → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
79 78 2rexbidv ⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
80 72 79 syl5ibr ⊢ ( 𝐴 = 𝐵 → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) ) )
81 80 imp ⊢ ( ( 𝐴 = 𝐵 ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑡 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝑥 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ) )