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 ⊢ S = ∑ p = 1 N A ⁡ p − B ⁡ p 2
axsegconlem7.2 ⊢ T = ∑ p = 1 N C ⁡ p − D ⁡ p 2
axsegconlem8.3 ⊢ F = k ∈ 1 … N ⟼ S + T ⁢ B ⁡ k − T ⁢ A ⁡ k S
Assertion axsegconlem10 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∀ i ∈ 1 … N B ⁡ i = 1 − S S + T ⁢ A ⁡ i + S S + T ⁢ F ⁡ i

Proof

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