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 syl5eq ( ( ( 𝐵𝑖 ) ∈ ℂ ∧ ( 𝐶𝑖 ) ∈ ℂ ∧ ( 𝐷𝑖 ) ∈ ℂ ) → ( ( 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 ) ) )