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 28905

Description: Lemma for axsegcon 28907. 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 6840	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
2	1	oveq2d 7385	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) = (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)))
3		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
4	3	oveq2d 7385	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((√‘𝑇) · (𝐴‘𝑘)) = ((√‘𝑇) · (𝐴‘𝑖)))
5	2, 4	oveq12d 7387	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) = ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))))
6	5	oveq1d 7384	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)) = (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)))
7		axsegconlem8.3	. . . . . . . . 9 ⊢ 𝐹 = (𝑘 ∈ (1...𝑁) ↦ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑘)) − ((√‘𝑇) · (𝐴‘𝑘))) / (√‘𝑆)))
8		ovex 7402	. . . . . . . . 9 ⊢ (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)) ∈ V
9	6, 7, 8	fvmpt 6950	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → (𝐹‘𝑖) = (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)))
10	9	adantl 481	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑖) = (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆)))
11	10	oveq2d 7385	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵‘𝑖) − (𝐹‘𝑖)) = ((𝐵‘𝑖) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))))
12		axsegconlem2.1	. . . . . . . . . . . . 13 ⊢ 𝑆 = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)
13	12	axsegconlem4 28900	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (√‘𝑆) ∈ ℝ)
14	13	3adant3 1132	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → (√‘𝑆) ∈ ℝ)
15	14	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑆) ∈ ℝ)
16		simpl2 1193	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
17		fveere 28881	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
18	16, 17	sylan 580	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
19	15, 18	remulcld 11180	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) · (𝐵‘𝑖)) ∈ ℝ)
20	19	recnd 11178	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) · (𝐵‘𝑖)) ∈ ℂ)
21		axsegconlem7.2	. . . . . . . . . . . . . 14 ⊢ 𝑇 = Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2)
22	21	axsegconlem4 28900	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → (√‘𝑇) ∈ ℝ)
23		readdcl 11127	. . . . . . . . . . . . 13 ⊢ (((√‘𝑆) ∈ ℝ ∧ (√‘𝑇) ∈ ℝ) → ((√‘𝑆) + (√‘𝑇)) ∈ ℝ)
24	14, 22, 23	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((√‘𝑆) + (√‘𝑇)) ∈ ℝ)
25	24	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) + (√‘𝑇)) ∈ ℝ)
26	25, 18	remulcld 11180	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) ∈ ℝ)
27	22	ad2antlr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑇) ∈ ℝ)
28		simpl1 1192	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
29		fveere 28881	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
30	28, 29	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
31	27, 30	remulcld 11180	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (𝐴‘𝑖)) ∈ ℝ)
32	26, 31	resubcld 11582	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) ∈ ℝ)
33	32	recnd 11178	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) ∈ ℂ)
34	15	recnd 11178	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑆) ∈ ℂ)
35	12	axsegconlem6 28902	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 0 < (√‘𝑆))
36	35	gt0ne0d 11718	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → (√‘𝑆) ≠ 0)
37	36	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑆) ≠ 0)
38	20, 33, 34, 37	divsubdird 11973	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) / (√‘𝑆)) = ((((√‘𝑆) · (𝐵‘𝑖)) / (√‘𝑆)) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))))
39	26	recnd 11178	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) ∈ ℂ)
40	31	recnd 11178	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (𝐴‘𝑖)) ∈ ℂ)
41	20, 39, 40	subsubd 11537	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) = ((((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))) + ((√‘𝑇) · (𝐴‘𝑖))))
42	27	recnd 11178	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (√‘𝑇) ∈ ℂ)
43	18	renegcld 11581	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(𝐵‘𝑖) ∈ ℝ)
44	43	recnd 11178	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(𝐵‘𝑖) ∈ ℂ)
45	30	recnd 11178	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
46	42, 44, 45	adddid 11174	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (-(𝐵‘𝑖) + (𝐴‘𝑖))) = (((√‘𝑇) · -(𝐵‘𝑖)) + ((√‘𝑇) · (𝐴‘𝑖))))
47	44, 45	addcomd 11352	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (-(𝐵‘𝑖) + (𝐴‘𝑖)) = ((𝐴‘𝑖) + -(𝐵‘𝑖)))
48	18	recnd 11178	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
49	45, 48	negsubd 11515	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) + -(𝐵‘𝑖)) = ((𝐴‘𝑖) − (𝐵‘𝑖)))
50	47, 49	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (-(𝐵‘𝑖) + (𝐴‘𝑖)) = ((𝐴‘𝑖) − (𝐵‘𝑖)))
51	50	oveq2d 7385	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · (-(𝐵‘𝑖) + (𝐴‘𝑖))) = ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))))
52	25	recnd 11178	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) + (√‘𝑇)) ∈ ℂ)
53	52, 34	negsubdi2d 11525	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(((√‘𝑆) + (√‘𝑇)) − (√‘𝑆)) = ((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))))
54	34, 42	pncan2d 11511	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) + (√‘𝑇)) − (√‘𝑆)) = (√‘𝑇))
55	54	negeqd 11391	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → -(((√‘𝑆) + (√‘𝑇)) − (√‘𝑆)) = -(√‘𝑇))
56	53, 55	eqtr3d 2766	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))) = -(√‘𝑇))
57	56	oveq1d 7384	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))) · (𝐵‘𝑖)) = (-(√‘𝑇) · (𝐵‘𝑖)))
58	34, 52, 48	subdird 11611	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) − ((√‘𝑆) + (√‘𝑇))) · (𝐵‘𝑖)) = (((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))))
59		mulneg12 11592	. . . . . . . . . . . . 13 ⊢ (((√‘𝑇) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) → (-(√‘𝑇) · (𝐵‘𝑖)) = ((√‘𝑇) · -(𝐵‘𝑖)))
60	42, 48, 59	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (-(√‘𝑇) · (𝐵‘𝑖)) = ((√‘𝑇) · -(𝐵‘𝑖)))
61	57, 58, 60	3eqtr3rd 2773	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · -(𝐵‘𝑖)) = (((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))))
62	61	oveq1d 7384	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇) · -(𝐵‘𝑖)) + ((√‘𝑇) · (𝐴‘𝑖))) = ((((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))) + ((√‘𝑇) · (𝐴‘𝑖))))
63	46, 51, 62	3eqtr3rd 2773	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) − (((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖))) + ((√‘𝑇) · (𝐴‘𝑖))) = ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))))
64	41, 63	eqtrd 2764	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) = ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))))
65	64	oveq1d 7384	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) − ((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖)))) / (√‘𝑆)) = (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆)))
66	48, 34, 37	divcan3d 11939	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑆) · (𝐵‘𝑖)) / (√‘𝑆)) = (𝐵‘𝑖))
67	66	oveq1d 7384	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑆) · (𝐵‘𝑖)) / (√‘𝑆)) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))) = ((𝐵‘𝑖) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))))
68	38, 65, 67	3eqtr3rd 2773	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵‘𝑖) − (((((√‘𝑆) + (√‘𝑇)) · (𝐵‘𝑖)) − ((√‘𝑇) · (𝐴‘𝑖))) / (√‘𝑆))) = (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆)))
69	11, 68	eqtrd 2764	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵‘𝑖) − (𝐹‘𝑖)) = (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆)))
70	69	oveq1d 7384	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆))↑2))
71	30, 18	resubcld 11582	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) − (𝐵‘𝑖)) ∈ ℝ)
72	27, 71	remulcld 11180	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ∈ ℝ)
73	72	recnd 11178	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) ∈ ℂ)
74	73, 34, 37	sqdivd 14100	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖))) / (√‘𝑆))↑2) = ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) / ((√‘𝑆)↑2)))
75	71	recnd 11178	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐴‘𝑖) − (𝐵‘𝑖)) ∈ ℂ)
76	42, 75	sqmuld 14099	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) = (((√‘𝑇)↑2) · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
77	21	axsegconlem2 28898	. . . . . . . . 9 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → 𝑇 ∈ ℝ)
78	77	ad2antlr 727	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑇 ∈ ℝ)
79	21	axsegconlem3 28899	. . . . . . . . 9 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → 0 ≤ 𝑇)
80	79	ad2antlr 727	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → 0 ≤ 𝑇)
81		resqrtth 15197	. . . . . . . 8 ⊢ ((𝑇 ∈ ℝ ∧ 0 ≤ 𝑇) → ((√‘𝑇)↑2) = 𝑇)
82	78, 80, 81	syl2anc 584	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑇)↑2) = 𝑇)
83	82	oveq1d 7384	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇)↑2) · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
84	76, 83	eqtrd 2764	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) = (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
85	12	axsegconlem2 28898	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 𝑆 ∈ ℝ)
86	12	axsegconlem3 28899	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → 0 ≤ 𝑆)
87		resqrtth 15197	. . . . . . . 8 ⊢ ((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) → ((√‘𝑆)↑2) = 𝑆)
88	85, 86, 87	syl2anc 584	. . . . . . 7 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((√‘𝑆)↑2) = 𝑆)
89	88	3adant3 1132	. . . . . 6 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → ((√‘𝑆)↑2) = 𝑆)
90	89	ad2antrr 726	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((√‘𝑆)↑2) = 𝑆)
91	84, 90	oveq12d 7387	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → ((((√‘𝑇) · ((𝐴‘𝑖) − (𝐵‘𝑖)))↑2) / ((√‘𝑆)↑2)) = ((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
92	70, 74, 91	3eqtrd 2768	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = ((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
93	92	sumeq2dv 15644	. 2 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
94		fzfid 13914	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (1...𝑁) ∈ Fin)
95	77	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑇 ∈ ℝ)
96	95	recnd 11178	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑇 ∈ ℂ)
97	71	resqcld 14066	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
98	97	recnd 11178	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℂ)
99	94, 96, 98	fsummulc2 15726	. . . 4 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = Σ𝑖 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)))
100	99	oveq1d 7384	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = (Σ𝑖 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
101		fveq2 6840	. . . . . . . . 9 ⊢ (𝑝 = 𝑖 → (𝐶‘𝑝) = (𝐶‘𝑖))
102		fveq2 6840	. . . . . . . . 9 ⊢ (𝑝 = 𝑖 → (𝐷‘𝑝) = (𝐷‘𝑖))
103	101, 102	oveq12d 7387	. . . . . . . 8 ⊢ (𝑝 = 𝑖 → ((𝐶‘𝑝) − (𝐷‘𝑝)) = ((𝐶‘𝑖) − (𝐷‘𝑖)))
104	103	oveq1d 7384	. . . . . . 7 ⊢ (𝑝 = 𝑖 → (((𝐶‘𝑝) − (𝐷‘𝑝))↑2) = (((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
105	104	cbvsumv 15638	. . . . . 6 ⊢ Σ𝑝 ∈ (1...𝑁)(((𝐶‘𝑝) − (𝐷‘𝑝))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)
106	21, 105	eqtri 2752	. . . . 5 ⊢ 𝑇 = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)
107		fveq2 6840	. . . . . . . . 9 ⊢ (𝑖 = 𝑝 → (𝐴‘𝑖) = (𝐴‘𝑝))
108		fveq2 6840	. . . . . . . . 9 ⊢ (𝑖 = 𝑝 → (𝐵‘𝑖) = (𝐵‘𝑝))
109	107, 108	oveq12d 7387	. . . . . . . 8 ⊢ (𝑖 = 𝑝 → ((𝐴‘𝑖) − (𝐵‘𝑖)) = ((𝐴‘𝑝) − (𝐵‘𝑝)))
110	109	oveq1d 7384	. . . . . . 7 ⊢ (𝑖 = 𝑝 → (((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = (((𝐴‘𝑝) − (𝐵‘𝑝))↑2))
111	110	cbvsumv 15638	. . . . . 6 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑝 ∈ (1...𝑁)(((𝐴‘𝑝) − (𝐵‘𝑝))↑2)
112	111, 12	eqtr4i 2755	. . . . 5 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = 𝑆
113	106, 112	oveq12i 7381	. . . 4 ⊢ (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = (Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) · 𝑆)
114		eqid 2729	. . . . . . . . . 10 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)
115	114	axsegconlem2 28898	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
116	115	3adant3 1132	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
117	116	adantr 480	. . . . . . 7 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2) ∈ ℝ)
118	95, 117	remulcld 11180	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℝ)
119	118	recnd 11178	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℂ)
120		eqid 2729	. . . . . . . 8 ⊢ Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2)
121	120	axsegconlem2 28898	. . . . . . 7 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ ℝ)
122	121	adantl 481	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ ℝ)
123	122	recnd 11178	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ∈ ℂ)
124	85	3adant3 1132	. . . . . . 7 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 𝑆 ∈ ℝ)
125	124	adantr 480	. . . . . 6 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑆 ∈ ℝ)
126	125	recnd 11178	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑆 ∈ ℂ)
127	86	3adant3 1132	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 0 ≤ 𝑆)
128		sqrt00 15205	. . . . . . . . 9 ⊢ ((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) → ((√‘𝑆) = 0 ↔ 𝑆 = 0))
129	128	necon3bid 2969	. . . . . . . 8 ⊢ ((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) → ((√‘𝑆) ≠ 0 ↔ 𝑆 ≠ 0))
130	124, 127, 129	syl2anc 584	. . . . . . 7 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → ((√‘𝑆) ≠ 0 ↔ 𝑆 ≠ 0))
131	36, 130	mpbid 232	. . . . . 6 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) → 𝑆 ≠ 0)
132	131	adantr 480	. . . . 5 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → 𝑆 ≠ 0)
133	119, 123, 126, 132	divmul3d 11968	. . . 4 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (((𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) ↔ (𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) = (Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2) · 𝑆)))
134	113, 133	mpbiri 258	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ((𝑇 · Σ𝑖 ∈ (1...𝑁)(((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
135	78, 97	remulcld 11180	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℝ)
136	135	recnd 11178	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) ∈ ℂ)
137	94, 126, 136, 132	fsumdivc 15728	. . 3 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → (Σ𝑖 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆))
138	100, 134, 137	3eqtr3rd 2773	. 2 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑖) − (𝐵‘𝑖))↑2)) / 𝑆) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))
139	93, 138	eqtrd 2764	1 ⊢ (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → Σ𝑖 ∈ (1...𝑁)(((𝐵‘𝑖) − (𝐹‘𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶‘𝑖) − (𝐷‘𝑖))↑2))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 class class class wbr 5102 ↦ cmpt 5183 ‘cfv 6499 (class class class)co 7369 ℂcc 11042 ℝcr 11043 0cc0 11044 1c1 11045 + caddc 11047 · cmul 11049 ≤ cle 11185 − cmin 11381 -cneg 11382 / cdiv 11811 2c2 12217 ...cfz 13444 ↑cexp 14002 √csqrt 15175 Σcsu 15628 𝔼cee 28868

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691 ax-inf2 9570 ax-cnex 11100 ax-resscn 11101 ax-1cn 11102 ax-icn 11103 ax-addcl 11104 ax-addrcl 11105 ax-mulcl 11106 ax-mulrcl 11107 ax-mulcom 11108 ax-addass 11109 ax-mulass 11110 ax-distr 11111 ax-i2m1 11112 ax-1ne0 11113 ax-1rid 11114 ax-rnegex 11115 ax-rrecex 11116 ax-cnre 11117 ax-pre-lttri 11118 ax-pre-lttrn 11119 ax-pre-ltadd 11120 ax-pre-mulgt0 11121 ax-pre-sup 11122

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3351 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-int 4907 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6262 df-ord 6323 df-on 6324 df-lim 6325 df-suc 6326 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-om 7823 df-1st 7947 df-2nd 7948 df-frecs 8237 df-wrecs 8268 df-recs 8317 df-rdg 8355 df-1o 8411 df-er 8648 df-map 8778 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-sup 9369 df-oi 9439 df-card 9868 df-pnf 11186 df-mnf 11187 df-xr 11188 df-ltxr 11189 df-le 11190 df-sub 11383 df-neg 11384 df-div 11812 df-nn 12163 df-2 12225 df-3 12226 df-n0 12419 df-z 12506 df-uz 12770 df-rp 12928 df-ico 13288 df-fz 13445 df-fzo 13592 df-seq 13943 df-exp 14003 df-hash 14272 df-cj 15041 df-re 15042 df-im 15043 df-sqrt 15177 df-abs 15178 df-clim 15430 df-sum 15629 df-ee 28871

This theorem is referenced by: axsegcon 28907

W3C validator