axsegconlem9 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axsegconlem9		Structured version Visualization version GIF version

Theorem axsegconlem9 26705

Description: Lemma for axsegcon 26707. Show that 𝐵𝐹 is congruent to 𝐶𝐷. (Contributed by Scott Fenton, 19-Sep-2013.)

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

**Assertion**
Ref	Expression
axsegconlem9	⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))

Distinct variable groups: 𝐴,𝑝 𝐵,𝑝 𝐶,𝑝 𝐷,𝑝 𝑁,𝑝 𝐴,𝑖,𝑘 𝐵,𝑖,𝑘 𝐶,𝑖,𝑘 𝐷,𝑖,𝑘 𝑖,𝑁,𝑘 𝑆,𝑖,𝑘 𝑇,𝑖,𝑘 𝑖,𝑝 Allowed substitution hints: 𝑆(𝑝) 𝑇(𝑝) 𝐹(𝑖,𝑘,𝑝)

**Proof of Theorem axsegconlem9**
Step	Hyp	Ref	Expression
1		fveq2 6665	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
2	1	oveq2d 7166	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) = (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)))
3		fveq2 6665	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
4	3	oveq2d 7166	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((√‘𝑇) · (𝐴‘𝑘)) = ((√‘𝑇) · (𝐴‘𝑖)))
5	2, 4	oveq12d 7168	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) = ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))))
6	5	oveq1d 7165	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)) = (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)))
7		axsegconlem8.3	. . . . . . . . 9 ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))
8		ovex 7183	. . . . . . . . 9 ⊢ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)) ∈ V
9	6, 7, 8	fvmpt 6763	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → (𝐹‘𝑖) = (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)))
10	9	adantl 484	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)))
11	10	oveq2d 7166	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵‘𝑖) − (𝐹‘𝑖)) = ((𝐵‘𝑖) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))))
12		axsegconlem2.1	. . . . . . . . . . . . 13 ⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)
13	12	axsegconlem4 26700	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (√‘𝑆) ∈ ℝ)
14	13	3adant3 1128	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → (√‘𝑆) ∈ ℝ)
15	14	ad2antrr 724	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑆) ∈ ℝ)
16		simpl2 1188	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
17		fveere 26681	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
18	16, 17	sylan 582	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
19	15, 18	remulcld 10665	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) · (𝐵‘𝑖)) ∈ ℝ)
20	19	recnd 10663	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) · (𝐵‘𝑖)) ∈ ℂ)
21		axsegconlem7.2	. . . . . . . . . . . . . 14 ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)
22	21	axsegconlem4 26700	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → (√‘𝑇) ∈ ℝ)
23		readdcl 10614	. . . . . . . . . . . . 13 ⊢ (((√‘𝑆) ∈ ℝ ∧ (√‘𝑇) ∈ ℝ) → ((√‘𝑆) + (√‘𝑇)) ∈ ℝ)
24	14, 22, 23	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((√‘𝑆) + (√‘𝑇)) ∈ ℝ)
25	24	adantr 483	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) + (√‘𝑇)) ∈ ℝ)
26	25, 18	remulcld 10665	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) ∈ ℝ)
27	22	ad2antlr 725	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑇) ∈ ℝ)
28		simpl1 1187	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
29		fveere 26681	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
30	28, 29	sylan 582	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
31	27, 30	remulcld 10665	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (𝐴‘𝑖)) ∈ ℝ)
32	26, 31	resubcld 11062	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) ∈ ℝ)
33	32	recnd 10663	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) ∈ ℂ)
34	15	recnd 10663	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑆) ∈ ℂ)
35	12	axsegconlem6 26702	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 0 < (√‘𝑆))
36	35	gt0ne0d 11198	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → (√‘𝑆) ≠ 0)
37	36	ad2antrr 724	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑆) ≠ 0)
38	20, 33, 34, 37	divsubdird 11449	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) / (√‘𝑆)) = ((((√‘𝑆) · (𝐵‘𝑖)) / (√‘𝑆)) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))))
39	26	recnd 10663	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) ∈ ℂ)
40	31	recnd 10663	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (𝐴‘𝑖)) ∈ ℂ)
41	20, 39, 40	subsubd 11019	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) = ((((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))) + ((√‘𝑇) · (𝐴‘𝑖))))
42	27	recnd 10663	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑇) ∈ ℂ)
43	18	renegcld 11061	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(𝐵‘𝑖) ∈ ℝ)
44	43	recnd 10663	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(𝐵‘𝑖) ∈ ℂ)
45	30	recnd 10663	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
46	42, 44, 45	adddid 10659	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (-(𝐵‘𝑖) + (𝐴‘𝑖))) = (((√‘𝑇) · -(𝐵‘𝑖)) + ((√‘𝑇) · (𝐴‘𝑖))))
47	44, 45	addcomd 10836	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (-(𝐵‘𝑖) + (𝐴‘𝑖)) = ((𝐴‘𝑖) + -(𝐵‘𝑖)))
48	18	recnd 10663	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
49	45, 48	negsubd 10997	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) + -(𝐵‘𝑖)) = ((𝐴‘𝑖) − (𝐵‘𝑖)))
50	47, 49	eqtrd 2856	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (-(𝐵‘𝑖) + (𝐴‘𝑖)) = ((𝐴‘𝑖) − (𝐵‘𝑖)))
51	50	oveq2d 7166	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (-(𝐵‘𝑖) + (𝐴‘𝑖))) = ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))))
52	25	recnd 10663	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) + (√‘𝑇)) ∈ ℂ)
53	52, 34	negsubdi2d 11007	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(((√‘𝑆) + (√‘𝑇)) − (√‘𝑆)) = ((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))))
54	34, 42	pncan2d 10993	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) + (√‘𝑇)) − (√‘𝑆)) = (√‘𝑇))
55	54	negeqd 10874	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(((√‘𝑆) + (√‘𝑇)) − (√‘𝑆)) = -(√‘𝑇))
56	53, 55	eqtr3d 2858	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))) = -(√‘𝑇))
57	56	oveq1d 7165	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))) · (𝐵‘𝑖)) = (-(√‘𝑇) · (𝐵‘𝑖)))
58	34, 52, 48	subdird 11091	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))) · (𝐵‘𝑖)) = (((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))))
59		mulneg12 11072	. . . . . . . . . . . . 13 ⊢ (((√‘𝑇) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) → (-(√‘𝑇) · (𝐵‘𝑖)) = ((√‘𝑇) · -(𝐵‘𝑖)))
60	42, 48, 59	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (-(√‘𝑇) · (𝐵‘𝑖)) = ((√‘𝑇) · -(𝐵‘𝑖)))
61	57, 58, 60	3eqtr3rd 2865	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · -(𝐵‘𝑖)) = (((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))))
62	61	oveq1d 7165	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇) · -(𝐵‘𝑖)) + ((√‘𝑇) · (𝐴‘𝑖))) = ((((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))) + ((√‘𝑇) · (𝐴‘𝑖))))
63	46, 51, 62	3eqtr3rd 2865	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))) + ((√‘𝑇) · (𝐴‘𝑖))) = ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))))
64	41, 63	eqtrd 2856	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) = ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))))
65	64	oveq1d 7165	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) / (√‘𝑆)) = (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆)))
66	48, 34, 37	divcan3d 11415	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) · (𝐵‘𝑖)) / (√‘𝑆)) = (𝐵‘𝑖))
67	66	oveq1d 7165	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) / (√‘𝑆)) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))) = ((𝐵‘𝑖) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))))
68	38, 65, 67	3eqtr3rd 2865	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵‘𝑖) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))) = (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆)))
69	11, 68	eqtrd 2856	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵‘𝑖) − (𝐹‘𝑖)) = (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆)))
70	69	oveq1d 7165	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆))↑2))
71	30, 18	resubcld 11062	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) − (𝐵‘𝑖)) ∈ ℝ)
72	27, 71	remulcld 10665	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ∈ ℝ)
73	72	recnd 10663	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ∈ ℂ)
74	73, 34, 37	sqdivd 13517	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆))↑2) = ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) / ((√‘𝑆)↑2)))
75	71	recnd 10663	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) − (𝐵‘𝑖)) ∈ ℂ)
76	42, 75	sqmuld 13516	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) = (((√‘𝑇)↑2) · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
77	21	axsegconlem2 26698	. . . . . . . . 9 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → 𝑇 ∈ ℝ)
78	77	ad2antlr 725	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑇 ∈ ℝ)
79	21	axsegconlem3 26699	. . . . . . . . 9 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → 0 ≤ 𝑇)
80	79	ad2antlr 725	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ 𝑇)
81		resqrtth 14609	. . . . . . . 8 ⊢ ((𝑇 ∈ ℝ ∧ 0 ≤ 𝑇) → ((√‘𝑇)↑2) = 𝑇)
82	78, 80, 81	syl2anc 586	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇)↑2) = 𝑇)
83	82	oveq1d 7165	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇)↑2) · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
84	76, 83	eqtrd 2856	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) = (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
85	12	axsegconlem2 26698	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝑆 ∈ ℝ)
86	12	axsegconlem3 26699	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 0 ≤ 𝑆)
87		resqrtth 14609	. . . . . . . 8 ⊢ ((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) → ((√‘𝑆)↑2) = 𝑆)
88	85, 86, 87	syl2anc 586	. . . . . . 7 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((√‘𝑆)↑2) = 𝑆)
89	88	3adant3 1128	. . . . . 6 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → ((√‘𝑆)↑2) = 𝑆)
90	89	ad2antrr 724	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆)↑2) = 𝑆)
91	84, 90	oveq12d 7168	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) / ((√‘𝑆)↑2)) = ((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
92	70, 74, 91	3eqtrd 2860	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = ((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
93	92	sumeq2dv 15054	. 2 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
94		fzfid 13335	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (1...𝑁) ∈ Fin)
95	77	adantl 484	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑇 ∈ ℝ)
96	95	recnd 10663	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑇 ∈ ℂ)
97	71	resqcld 13605	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
98	97	recnd 10663	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℂ)
99	94, 96, 98	fsummulc2 15133	. . . 4 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = Σ𝑖 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
100	99	oveq1d 7165	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = (Σ𝑖 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
101		fveq2 6665	. . . . . . . . 9 ⊢ (𝑝 = 𝑖 → (𝐶‘𝑝) = (𝐶‘𝑖))
102		fveq2 6665	. . . . . . . . 9 ⊢ (𝑝 = 𝑖 → (𝐷‘𝑝) = (𝐷‘𝑖))
103	101, 102	oveq12d 7168	. . . . . . . 8 ⊢ (𝑝 = 𝑖 → ((𝐶‘𝑝) − (𝐷‘𝑝)) = ((𝐶‘𝑖) − (𝐷‘𝑖)))
104	103	oveq1d 7165	. . . . . . 7 ⊢ (𝑝 = 𝑖 → (((𝐶‘𝑝) − (𝐷‘𝑝))↑2) = (((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
105	104	cbvsumv 15047	. . . . . 6 ⊢ Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)
106	21, 105	eqtri 2844	. . . . 5 ⊢ 𝑇 = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)
107		fveq2 6665	. . . . . . . . 9 ⊢ (𝑖 = 𝑝 → (𝐴‘𝑖) = (𝐴‘𝑝))
108		fveq2 6665	. . . . . . . . 9 ⊢ (𝑖 = 𝑝 → (𝐵‘𝑖) = (𝐵‘𝑝))
109	107, 108	oveq12d 7168	. . . . . . . 8 ⊢ (𝑖 = 𝑝 → ((𝐴‘𝑖) − (𝐵‘𝑖)) = ((𝐴‘𝑝) − (𝐵‘𝑝)))
110	109	oveq1d 7165	. . . . . . 7 ⊢ (𝑖 = 𝑝 → (((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = (((𝐴‘𝑝) − (𝐵‘𝑝))↑2))
111	110	cbvsumv 15047	. . . . . 6 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)
112	111, 12	eqtr4i 2847	. . . . 5 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = 𝑆
113	106, 112	oveq12i 7162	. . . 4 ⊢ (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = (Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) · 𝑆)
114		eqid 2821	. . . . . . . . . 10 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)
115	114	axsegconlem2 26698	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
116	115	3adant3 1128	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
117	116	adantr 483	. . . . . . 7 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
118	95, 117	remulcld 10665	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℝ)
119	118	recnd 10663	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℂ)
120		eqid 2821	. . . . . . . 8 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)
121	120	axsegconlem2 26698	. . . . . . 7 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ ℝ)
122	121	adantl 484	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ ℝ)
123	122	recnd 10663	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ ℂ)
124	85	3adant3 1128	. . . . . . 7 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 𝑆 ∈ ℝ)
125	124	adantr 483	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑆 ∈ ℝ)
126	125	recnd 10663	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑆 ∈ ℂ)
127	86	3adant3 1128	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 0 ≤ 𝑆)
128		sqrt00 14617	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) → ((√‘𝑆) = 0 ↔ 𝑆 = 0))
129	128	necon3bid 3060	. . . . . . . 8 ⊢ ((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) → ((√‘𝑆) ≠ 0 ↔ 𝑆 ≠ 0))
130	124, 127, 129	syl2anc 586	. . . . . . 7 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → ((√‘𝑆) ≠ 0 ↔ 𝑆 ≠ 0))
131	36, 130	mpbid 234	. . . . . 6 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 𝑆 ≠ 0)
132	131	adantr 483	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑆 ≠ 0)
133	119, 123, 126, 132	divmul3d 11444	. . . 4 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (((𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ↔ (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = (Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) · 𝑆)))
134	113, 133	mpbiri 260	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
135	78, 97	remulcld 10665	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℝ)
136	135	recnd 10663	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℂ)
137	94, 126, 136, 132	fsumdivc 15135	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (Σ𝑖 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
138	100, 134, 137	3eqtr3rd 2865	. 2 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
139	93, 138	eqtrd 2856	1 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 class class class wbr 5059 ↦ cmpt 5139 ‘cfv 6350 (class class class)co 7150 ℂcc 10529 ℝcr 10530 0cc0 10531 1c1 10532 + caddc 10534 · cmul 10536 ≤ cle 10670 − cmin 10864 -cneg 10865 / cdiv 11291 2c2 11686 ...cfz 12886 ↑cexp 13423 √csqrt 14586 Σcsu 15036 𝔼cee 26668

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455 ax-inf2 9098 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-fal 1546 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3497 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-se 5510 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-isom 6359 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-oi 8968 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-div 11292 df-nn 11633 df-2 11694 df-3 11695 df-n0 11892 df-z 11976 df-uz 12238 df-rp 12384 df-ico 12738 df-fz 12887 df-fzo 13028 df-seq 13364 df-exp 13424 df-hash 13685 df-cj 14452 df-re 14453 df-im 14454 df-sqrt 14588 df-abs 14589 df-clim 14839 df-sum 15037 df-ee 26671

This theorem is referenced by: axsegcon 26707

W3C validator