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

Theorem axsegconlem1 26697
Description: Lemma for axsegcon 26707. Handle the degenerate case. (Contributed by Scott Fenton, 7-Jun-2013.)
Assertion
Ref Expression
axsegconlem1 ((𝐴 = 𝐵 ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)))
Distinct variable groups:   𝑡,𝑁,𝑖,𝑥   𝑡,𝐴,𝑖,𝑥   𝑡,𝐵,𝑖,𝑥   𝑡,𝐶,𝑖,𝑥   𝑡,𝐷,𝑖,𝑥

Proof of Theorem axsegconlem1
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 fveere 26681 . . . . . . . . . 10 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) ∈ ℝ)
213ad2antl1 1181 . . . . . . . . 9 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) ∈ ℝ)
3 fveere 26681 . . . . . . . . . . 11 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶𝑘) ∈ ℝ)
433ad2antl2 1182 . . . . . . . . . 10 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶𝑘) ∈ ℝ)
5 fveere 26681 . . . . . . . . . . 11 ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐷𝑘) ∈ ℝ)
653ad2antl3 1183 . . . . . . . . . 10 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑘 ∈ (1...𝑁)) → (𝐷𝑘) ∈ ℝ)
74, 6resubcld 11062 . . . . . . . . 9 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐶𝑘) − (𝐷𝑘)) ∈ ℝ)
82, 7resubcld 11062 . . . . . . . 8 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑘 ∈ (1...𝑁)) → ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))) ∈ ℝ)
98ralrimiva 3182 . . . . . . 7 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → ∀𝑘 ∈ (1...𝑁)((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))) ∈ ℝ)
10 eleenn 26676 . . . . . . . . 9 (𝐵 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
11 mptelee 26675 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))) ∈ ℝ))
1210, 11syl 17 . . . . . . . 8 (𝐵 ∈ (𝔼‘𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))) ∈ ℝ))
13123ad2ant1 1129 . . . . . . 7 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → ((𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))) ∈ ℝ))
149, 13mpbird 259 . . . . . 6 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∈ (𝔼‘𝑁))
15 fveecn 26682 . . . . . . . . 9 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
16153ad2antl1 1181 . . . . . . . 8 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
17 fveecn 26682 . . . . . . . . 9 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
18173ad2antl2 1182 . . . . . . . 8 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
19 fveecn 26682 . . . . . . . . 9 ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐷𝑖) ∈ ℂ)
20193ad2antl3 1183 . . . . . . . 8 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐷𝑖) ∈ ℂ)
21 1m0e1 11752 . . . . . . . . . . . 12 (1 − 0) = 1
2221oveq1i 7160 . . . . . . . . . . 11 ((1 − 0) · (𝐵𝑖)) = (1 · (𝐵𝑖))
23 mulid2 10634 . . . . . . . . . . . 12 ((𝐵𝑖) ∈ ℂ → (1 · (𝐵𝑖)) = (𝐵𝑖))
24233ad2ant1 1129 . . . . . . . . . . 11 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → (1 · (𝐵𝑖)) = (𝐵𝑖))
2522, 24syl5eq 2868 . . . . . . . . . 10 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → ((1 − 0) · (𝐵𝑖)) = (𝐵𝑖))
26 subcl 10879 . . . . . . . . . . . . 13 (((𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → ((𝐶𝑖) − (𝐷𝑖)) ∈ ℂ)
27 subcl 10879 . . . . . . . . . . . . 13 (((𝐵𝑖) ∈ ℂ ∧ ((𝐶𝑖) − (𝐷𝑖)) ∈ ℂ) → ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))) ∈ ℂ)
2826, 27sylan2 594 . . . . . . . . . . . 12 (((𝐵𝑖) ∈ ℂ ∧ ((𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ)) → ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))) ∈ ℂ)
29283impb 1111 . . . . . . . . . . 11 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))) ∈ ℂ)
3029mul02d 10832 . . . . . . . . . 10 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))) = 0)
3125, 30oveq12d 7168 . . . . . . . . 9 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) = ((𝐵𝑖) + 0))
32 addid1 10814 . . . . . . . . . 10 ((𝐵𝑖) ∈ ℂ → ((𝐵𝑖) + 0) = (𝐵𝑖))
33323ad2ant1 1129 . . . . . . . . 9 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → ((𝐵𝑖) + 0) = (𝐵𝑖))
3431, 33eqtr2d 2857 . . . . . . . 8 (((𝐵𝑖) ∈ ℂ ∧ (𝐶𝑖) ∈ ℂ ∧ (𝐷𝑖) ∈ ℂ) → (𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))))
3516, 18, 20, 34syl3anc 1367 . . . . . . 7 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))))
3635ralrimiva 3182 . . . . . 6 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → ∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))))
3718, 20subcld 10991 . . . . . . . . 9 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐶𝑖) − (𝐷𝑖)) ∈ ℂ)
3816, 37nncand 10996 . . . . . . . 8 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))) = ((𝐶𝑖) − (𝐷𝑖)))
3938oveq1d 7165 . . . . . . 7 (((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = (((𝐶𝑖) − (𝐷𝑖))↑2))
4039sumeq2dv 15054 . . . . . 6 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))
41 0elunit 12849 . . . . . . 7 0 ∈ (0[,]1)
42 fveq1 6663 . . . . . . . . . . . . . 14 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) → (𝑥𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))))‘𝑖))
43 fveq2 6664 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (𝐵𝑘) = (𝐵𝑖))
44 fveq2 6664 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝐶𝑘) = (𝐶𝑖))
45 fveq2 6664 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (𝐷𝑘) = (𝐷𝑖))
4644, 45oveq12d 7168 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → ((𝐶𝑘) − (𝐷𝑘)) = ((𝐶𝑖) − (𝐷𝑖)))
4743, 46oveq12d 7168 . . . . . . . . . . . . . . 15 (𝑘 = 𝑖 → ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))) = ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))
48 eqid 2821 . . . . . . . . . . . . . . 15 (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))))
49 ovex 7183 . . . . . . . . . . . . . . 15 ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))) ∈ V
5047, 48, 49fvmpt 6762 . . . . . . . . . . . . . 14 (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘))))‘𝑖) = ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))
5142, 50sylan9eq 2876 . . . . . . . . . . . . 13 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) = ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))
5251oveq2d 7166 . . . . . . . . . . . 12 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝑥𝑖)) = (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))))
5352oveq2d 7166 . . . . . . . . . . 11 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))))
5453eqeq2d 2832 . . . . . . . . . 10 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ↔ (𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))))))
5554ralbidva 3196 . . . . . . . . 9 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))))))
5651oveq2d 7166 . . . . . . . . . . . 12 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐵𝑖) − (𝑥𝑖)) = ((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))))
5756oveq1d 7165 . . . . . . . . . . 11 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵𝑖) − (𝑥𝑖))↑2) = (((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2))
5857sumeq2dv 15054 . . . . . . . . . 10 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) → Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2))
5958eqeq1d 2823 . . . . . . . . 9 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) → (Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2) ↔ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)))
6055, 59anbi12d 632 . . . . . . . 8 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) → ((∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)) ↔ (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))))
61 oveq2 7158 . . . . . . . . . . . . 13 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
6261oveq1d 7165 . . . . . . . . . . . 12 (𝑡 = 0 → ((1 − 𝑡) · (𝐵𝑖)) = ((1 − 0) · (𝐵𝑖)))
63 oveq1 7157 . . . . . . . . . . . 12 (𝑡 = 0 → (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))) = (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))))
6462, 63oveq12d 7168 . . . . . . . . . . 11 (𝑡 = 0 → (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))))
6564eqeq2d 2832 . . . . . . . . . 10 (𝑡 = 0 → ((𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) ↔ (𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))))))
6665ralbidv 3197 . . . . . . . . 9 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖)))))))
6766anbi1d 631 . . . . . . . 8 (𝑡 = 0 → ((∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)) ↔ (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))))
6860, 67rspc2ev 3634 . . . . . . 7 (((𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∈ (𝔼‘𝑁) ∧ 0 ∈ (0[,]1) ∧ (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)))
6941, 68mp3an2 1445 . . . . . 6 (((𝑘 ∈ (1...𝑁) ↦ ((𝐵𝑘) − ((𝐶𝑘) − (𝐷𝑘)))) ∈ (𝔼‘𝑁) ∧ (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 0) · (𝐵𝑖)) + (0 · ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − ((𝐵𝑖) − ((𝐶𝑖) − (𝐷𝑖))))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)))
7014, 36, 40, 69syl12anc 834 . . . . 5 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)))
71703expb 1116 . . . 4 ((𝐵 ∈ (𝔼‘𝑁) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)))
7271adantll 712 . . 3 (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)))
73 fveq1 6663 . . . . . . . . 9 (𝐴 = 𝐵 → (𝐴𝑖) = (𝐵𝑖))
7473oveq2d 7166 . . . . . . . 8 (𝐴 = 𝐵 → ((1 − 𝑡) · (𝐴𝑖)) = ((1 − 𝑡) · (𝐵𝑖)))
7574oveq1d 7165 . . . . . . 7 (𝐴 = 𝐵 → (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝑥𝑖))) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))))
7675eqeq2d 2832 . . . . . 6 (𝐴 = 𝐵 → ((𝐵𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝑥𝑖))) ↔ (𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖)))))
7776ralbidv 3197 . . . . 5 (𝐴 = 𝐵 → (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝑥𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖)))))
7877anbi1d 631 . . . 4 (𝐴 = 𝐵 → ((∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)) ↔ (∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))))
79782rexbidv 3300 . . 3 (𝐴 = 𝐵 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2)) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐵𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))))
8072, 79syl5ibr 248 . 2 (𝐴 = 𝐵 → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝑥𝑖))) ∧ Σ𝑖 ∈ (1...𝑁)(((𝐵𝑖) − (𝑥𝑖))↑2) = Σ𝑖 ∈ (1...𝑁)(((𝐶𝑖) − (𝐷𝑖))↑2))))
8180imp 409 1 ((𝐴 = 𝐵 ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑡 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐵𝑖) = (((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  wral 3138  wrex 3139  cmpt 5138  cfv 6349  (class class class)co 7150  cc 10529  cr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536  cmin 10864  cn 11632  2c2 11686  [,]cicc 12735  ...cfz 12886  cexp 13423  Σ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 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  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
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-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-tp 4565  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  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-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-n0 11892  df-z 11976  df-uz 12238  df-icc 12739  df-fz 12887  df-seq 13364  df-sum 15037  df-ee 26671
This theorem is referenced by:  axsegcon  26707
  Copyright terms: Public domain W3C validator