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 ⊢ 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 axsegconlem9 ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ A ≠ B ∧ C ∈ 𝔼 ⁡ N ∧ D ∈ 𝔼 ⁡ N → ∑ i = 1 N B ⁡ i − F ⁡ i 2 = ∑ i = 1 N C ⁡ i − D ⁡ i 2

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