Metamath Proof Explorer

Theorem axsegconlem9

Description: Lemma for axsegcon . Show that B F is congruent to C D . (Contributed by Scott Fenton, 19-Sep-2013)

Ref Expression
Hypotheses axsegconlem2.1 ⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
axsegconlem7.2 ⊢ 𝑇 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
axsegconlem8.3 ⊢ 𝐹 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) )
Assertion axsegconlem9 ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
2 axsegconlem7.2 ⊢ 𝑇 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
3 axsegconlem8.3 ⊢ 𝐹 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) )
4 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑖 ) )
5 4 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) = ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) )
6 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑖 ) )
7 6 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) = ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) )
8 5 7 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) = ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
9 8 oveq1d ⊢ ( 𝑘 = 𝑖 → ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) = ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
10 ovex ⊢ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ∈ V
11 9 3 10 fvmpt ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( 𝐹 ‘ 𝑖 ) = ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
12 11 adantl ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
13 12 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ) )
14 1 axsegconlem4 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
15 14 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ∈ ℝ )
16 15 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
17 simpl2 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
18 fveere ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
19 17 18 sylan ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
20 16 19 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
21 20 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
22 2 axsegconlem4 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℝ )
23 readdcl ⊢ ( ( ( √ ‘ 𝑆 ) ∈ ℝ ∧ ( √ ‘ 𝑇 ) ∈ ℝ ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
24 15 22 23 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
25 24 adantr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
26 25 19 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
27 22 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℝ )
28 simpl1 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
29 fveere ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
30 28 29 sylan ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
31 27 30 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
32 26 31 resubcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℝ )
33 32 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ )
34 16 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℂ )
35 1 axsegconlem6 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 0 < ( √ ‘ 𝑆 ) )
36 35 gt0ne0d ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ≠ 0 )
37 36 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ≠ 0 )
38 21 33 34 37 divsubdird ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) / ( √ ‘ 𝑆 ) ) = ( ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) / ( √ ‘ 𝑆 ) ) − ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ) )
39 26 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
40 31 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
41 21 39 40 subsubd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) = ( ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
42 27 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℂ )
43 19 renegcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
44 43 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
45 30 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
46 42 44 45 adddid ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( - ( 𝐵 ‘ 𝑖 ) + ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( √ ‘ 𝑇 ) · - ( 𝐵 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
47 44 45 addcomd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( 𝐵 ‘ 𝑖 ) + ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) + - ( 𝐵 ‘ 𝑖 ) ) )
48 19 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
49 45 48 negsubd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) + - ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) )
50 47 49 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( 𝐵 ‘ 𝑖 ) + ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) )
51 50 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( - ( 𝐵 ‘ 𝑖 ) + ( 𝐴 ‘ 𝑖 ) ) ) = ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) )
52 25 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℂ )
53 52 34 negsubdi2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) = ( ( √ ‘ 𝑆 ) − ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
54 34 42 pncan2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) = ( √ ‘ 𝑇 ) )
55 54 negeqd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) = - ( √ ‘ 𝑇 ) )
56 53 55 eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) − ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = - ( √ ‘ 𝑇 ) )
57 56 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) − ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐵 ‘ 𝑖 ) ) = ( - ( √ ‘ 𝑇 ) · ( 𝐵 ‘ 𝑖 ) ) )
58 34 52 48 subdird ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) − ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐵 ‘ 𝑖 ) ) = ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) )
59 mulneg12 ⊢ ( ( ( √ ‘ 𝑇 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) → ( - ( √ ‘ 𝑇 ) · ( 𝐵 ‘ 𝑖 ) ) = ( ( √ ‘ 𝑇 ) · - ( 𝐵 ‘ 𝑖 ) ) )
60 42 48 59 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( √ ‘ 𝑇 ) · ( 𝐵 ‘ 𝑖 ) ) = ( ( √ ‘ 𝑇 ) · - ( 𝐵 ‘ 𝑖 ) ) )
61 57 58 60 3eqtr3rd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · - ( 𝐵 ‘ 𝑖 ) ) = ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) )
62 61 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · - ( 𝐵 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
63 46 51 62 3eqtr3rd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) )
64 41 63 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) = ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) )
65 64 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) / ( √ ‘ 𝑆 ) ) = ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
66 48 34 37 divcan3d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) / ( √ ‘ 𝑆 ) ) = ( 𝐵 ‘ 𝑖 ) )
67 66 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) · ( 𝐵 ‘ 𝑖 ) ) / ( √ ‘ 𝑆 ) ) − ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ) = ( ( 𝐵 ‘ 𝑖 ) − ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ) )
68 38 65 67 3eqtr3rd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ) = ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
69 13 68 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) = ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
70 69 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ↑ 2 ) )
71 30 19 resubcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
72 27 71 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ∈ ℝ )
73 72 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ∈ ℂ )
74 73 34 37 sqdivd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ↑ 2 ) = ( ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↑ 2 ) / ( ( √ ‘ 𝑆 ) ↑ 2 ) ) )
75 71 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
76 42 75 sqmuld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↑ 2 ) = ( ( ( √ ‘ 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) )
77 2 axsegconlem2 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑇 ∈ ℝ )
78 77 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑇 ∈ ℝ )
79 2 axsegconlem3 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ 𝑇 )
80 79 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ 𝑇 )
81 resqrtth ⊢ ( ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ) → ( ( √ ‘ 𝑇 ) ↑ 2 ) = 𝑇 )
82 78 80 81 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) ↑ 2 ) = 𝑇 )
83 82 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) ↑ 2 ) · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) = ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) )
84 76 83 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↑ 2 ) = ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) )
85 1 axsegconlem2 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑆 ∈ ℝ )
86 1 axsegconlem3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ 𝑆 )
87 resqrtth ⊢ ( ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) → ( ( √ ‘ 𝑆 ) ↑ 2 ) = 𝑆 )
88 85 86 87 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( √ ‘ 𝑆 ) ↑ 2 ) = 𝑆 )
89 88 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( √ ‘ 𝑆 ) ↑ 2 ) = 𝑆 )
90 89 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) ↑ 2 ) = 𝑆 )
91 84 90 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑇 ) · ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ) ↑ 2 ) / ( ( √ ‘ 𝑆 ) ↑ 2 ) ) = ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) )
92 70 74 91 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ↑ 2 ) = ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) )
93 92 sumeq2dv ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) )
94 fzfid ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
95 77 adantl ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑇 ∈ ℝ )
96 95 recnd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑇 ∈ ℂ )
97 71 resqcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
98 97 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℂ )
99 94 96 98 fsummulc2 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) )
100 99 oveq1d ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) )
101 fveq2 ⊢ ( 𝑝 = 𝑖 → ( 𝐶 ‘ 𝑝 ) = ( 𝐶 ‘ 𝑖 ) )
102 fveq2 ⊢ ( 𝑝 = 𝑖 → ( 𝐷 ‘ 𝑝 ) = ( 𝐷 ‘ 𝑖 ) )
103 101 102 oveq12d ⊢ ( 𝑝 = 𝑖 → ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) = ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) )
104 103 oveq1d ⊢ ( 𝑝 = 𝑖 → ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) = ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
105 104 cbvsumv ⊢ Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 )
106 2 105 eqtri ⊢ 𝑇 = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 )
107 fveq2 ⊢ ( 𝑖 = 𝑝 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑝 ) )
108 fveq2 ⊢ ( 𝑖 = 𝑝 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 𝑝 ) )
109 107 108 oveq12d ⊢ ( 𝑖 = 𝑝 → ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) = ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) )
110 109 oveq1d ⊢ ( 𝑖 = 𝑝 → ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 ) )
111 110 cbvsumv ⊢ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
112 111 1 eqtr4i ⊢ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = 𝑆
113 106 112 oveq12i ⊢ ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) · 𝑆 )
114 eqid ⊢ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 )
115 114 axsegconlem2 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
116 115 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
117 116 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
118 95 117 remulcld ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
119 118 recnd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℂ )
120 eqid ⊢ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 )
121 120 axsegconlem2 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
122 121 adantl ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℝ )
123 122 recnd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ∈ ℂ )
124 85 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑆 ∈ ℝ )
125 124 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑆 ∈ ℝ )
126 125 recnd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑆 ∈ ℂ )
127 86 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 0 ≤ 𝑆 )
128 sqrt00 ⊢ ( ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) → ( ( √ ‘ 𝑆 ) = 0 ↔ 𝑆 = 0 ) )
129 128 necon3bid ⊢ ( ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) → ( ( √ ‘ 𝑆 ) ≠ 0 ↔ 𝑆 ≠ 0 ) )
130 124 127 129 syl2anc ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( ( √ ‘ 𝑆 ) ≠ 0 ↔ 𝑆 ≠ 0 ) )
131 36 130 mpbid ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 𝑆 ≠ 0 )
132 131 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑆 ≠ 0 )
133 119 123 126 132 divmul3d ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) ↔ ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) = ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) · 𝑆 ) ) )
134 113 133 mpbiri ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑇 · Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
135 78 97 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℝ )
136 135 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) ∈ ℂ )
137 94 126 136 132 fsumdivc ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) )
138 100 134 137 3eqtr3rd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑇 · ( ( ( 𝐴 ‘ 𝑖 ) − ( 𝐵 ‘ 𝑖 ) ) ↑ 2 ) ) / 𝑆 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )
139 93 138 eqtrd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐵 ‘ 𝑖 ) − ( 𝐹 ‘ 𝑖 ) ) ↑ 2 ) = Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑖 ) − ( 𝐷 ‘ 𝑖 ) ) ↑ 2 ) )