Metamath Proof Explorer

Theorem axsegconlem10

Description: Lemma for axsegcon . Show that the scaling constant from axsegconlem7 produces the betweenness condition for A , B and F . (Contributed by Scott Fenton, 21-Sep-2013)

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

Proof

Step Hyp Ref Expression
1 axsegconlem2.1 ⊢ 𝑆 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐴 ‘ 𝑝 ) − ( 𝐵 ‘ 𝑝 ) ) ↑ 2 )
2 axsegconlem7.2 ⊢ 𝑇 = Σ 𝑝 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐶 ‘ 𝑝 ) − ( 𝐷 ‘ 𝑝 ) ) ↑ 2 )
3 axsegconlem8.3 ⊢ 𝐹 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) )
4 2 axsegconlem4 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℝ )
5 4 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℝ )
6 simpl1 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
7 fveere ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
8 6 7 sylan ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
9 5 8 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
10 9 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
11 1 axsegconlem4 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
12 11 3adant3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ∈ ℝ )
13 12 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
14 1 2 3 axsegconlem8 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) )
15 fveere ⊢ ( ( 𝐹 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
16 14 15 sylan ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℝ )
17 13 16 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ∈ ℝ )
18 17 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ∈ ℂ )
19 readdcl ⊢ ( ( ( √ ‘ 𝑆 ) ∈ ℝ ∧ ( √ ‘ 𝑇 ) ∈ ℝ ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
20 12 4 19 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
21 20 adantr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℝ )
22 21 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ∈ ℂ )
23 0red ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 ∈ ℝ )
24 12 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( √ ‘ 𝑆 ) ∈ ℝ )
25 1 axsegconlem6 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → 0 < ( √ ‘ 𝑆 ) )
26 25 adantr ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 < ( √ ‘ 𝑆 ) )
27 2 axsegconlem5 ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → 0 ≤ ( √ ‘ 𝑇 ) )
28 27 adantl ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 ≤ ( √ ‘ 𝑇 ) )
29 addge01 ⊢ ( ( ( √ ‘ 𝑆 ) ∈ ℝ ∧ ( √ ‘ 𝑇 ) ∈ ℝ ) → ( 0 ≤ ( √ ‘ 𝑇 ) ↔ ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
30 12 4 29 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 0 ≤ ( √ ‘ 𝑇 ) ↔ ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
31 28 30 mpbid ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( √ ‘ 𝑆 ) ≤ ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) )
32 23 24 20 26 31 ltletrd ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 0 < ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) )
33 32 gt0ne0d ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ≠ 0 )
34 33 adantr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ≠ 0 )
35 10 18 22 34 divdird ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) + ( ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) )
36 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑖 ) )
37 36 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) = ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) )
38 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑖 ) )
39 38 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) = ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) )
40 37 39 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) = ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
41 40 oveq1d ⊢ ( 𝑘 = 𝑖 → ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑘 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑘 ) ) ) / ( √ ‘ 𝑆 ) ) = ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
42 ovex ⊢ ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ∈ V
43 41 3 42 fvmpt ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( 𝐹 ‘ 𝑖 ) = ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
44 43 adantl ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) )
45 44 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) = ( ( √ ‘ 𝑆 ) · ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ) )
46 simpl2 ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
47 fveere ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
48 46 47 sylan ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
49 21 48 remulcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
50 49 9 resubcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℝ )
51 50 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ )
52 13 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ∈ ℂ )
53 25 gt0ne0d ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ≠ 0 )
54 53 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑆 ) ≠ 0 )
55 51 52 54 divcan2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) · ( ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) / ( √ ‘ 𝑆 ) ) ) = ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
56 45 55 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) = ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
57 56 oveq2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) = ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) )
58 49 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
59 10 58 pncan3d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) − ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) = ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) )
60 57 59 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) = ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) )
61 9 17 readdcld ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℝ )
62 61 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) ∈ ℂ )
63 48 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
64 62 63 22 34 divmul2d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( 𝐵 ‘ 𝑖 ) ↔ ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) = ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) )
65 60 64 mpbird ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( 𝐵 ‘ 𝑖 ) )
66 4 recnd ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℂ )
67 66 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( √ ‘ 𝑇 ) ∈ ℂ )
68 8 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
69 67 68 22 34 div23d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( ( ( √ ‘ 𝑇 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐴 ‘ 𝑖 ) ) )
70 22 52 22 34 divsubdird ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) )
71 12 recnd ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) → ( √ ‘ 𝑆 ) ∈ ℂ )
72 pncan2 ⊢ ( ( ( √ ‘ 𝑆 ) ∈ ℂ ∧ ( √ ‘ 𝑇 ) ∈ ℂ ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) = ( √ ‘ 𝑇 ) )
73 71 66 72 syl2an ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) = ( √ ‘ 𝑇 ) )
74 73 adantr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) = ( √ ‘ 𝑇 ) )
75 74 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) − ( √ ‘ 𝑆 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( ( √ ‘ 𝑇 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) )
76 22 34 dividd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = 1 )
77 76 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) = ( 1 − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) )
78 70 75 77 3eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( √ ‘ 𝑇 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( 1 − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) )
79 78 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) )
80 69 79 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( ( 1 − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) )
81 16 recnd ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) ∈ ℂ )
82 52 81 22 34 div23d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) = ( ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐹 ‘ 𝑖 ) ) )
83 80 82 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( √ ‘ 𝑇 ) · ( 𝐴 ‘ 𝑖 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) + ( ( ( √ ‘ 𝑆 ) · ( 𝐹 ‘ 𝑖 ) ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) = ( ( ( 1 − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐹 ‘ 𝑖 ) ) ) )
84 35 65 83 3eqtr3d ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐹 ‘ 𝑖 ) ) ) )
85 84 ralrimiva ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( √ ‘ 𝑆 ) / ( ( √ ‘ 𝑆 ) + ( √ ‘ 𝑇 ) ) ) · ( 𝐹 ‘ 𝑖 ) ) ) )