Proof of Theorem ax5seglem9
Step | Hyp | Ref
| Expression |
1 | | fzfid 12772 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (1...𝑁) ∈ Fin) |
2 | | 0re 10040 |
. . . . . . 7
⊢ 0 ∈
ℝ |
3 | | 1re 10039 |
. . . . . . 7
⊢ 1 ∈
ℝ |
4 | 2, 3 | elicc2i 12239 |
. . . . . 6
⊢ (𝑇 ∈ (0[,]1) ↔ (𝑇 ∈ ℝ ∧ 0 ≤
𝑇 ∧ 𝑇 ≤ 1)) |
5 | 4 | simp1bi 1076 |
. . . . 5
⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈
ℝ) |
6 | 5 | recnd 10068 |
. . . 4
⊢ (𝑇 ∈ (0[,]1) → 𝑇 ∈
ℂ) |
7 | 6 | ad2antrl 764 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → 𝑇 ∈ ℂ) |
8 | | simprrl 804 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → 𝐶 ∈ (𝔼‘𝑁)) |
9 | 8 | ad2antrr 762 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → 𝐶 ∈ (𝔼‘𝑁)) |
10 | | fveecn 25782 |
. . . . . 6
⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝐶‘𝑗) ∈ ℂ) |
11 | 9, 10 | sylancom 701 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (𝐶‘𝑗) ∈ ℂ) |
12 | | simprrr 805 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → 𝐷 ∈ (𝔼‘𝑁)) |
13 | 12 | ad2antrr 762 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → 𝐷 ∈ (𝔼‘𝑁)) |
14 | | fveecn 25782 |
. . . . . 6
⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝐷‘𝑗) ∈ ℂ) |
15 | 13, 14 | sylancom 701 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (𝐷‘𝑗) ∈ ℂ) |
16 | 11, 15 | subcld 10392 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → ((𝐶‘𝑗) − (𝐷‘𝑗)) ∈ ℂ) |
17 | 16 | sqcld 13006 |
. . 3
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (((𝐶‘𝑗) − (𝐷‘𝑗))↑2) ∈ ℂ) |
18 | 1, 7, 17 | fsummulc2 14516 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = Σ𝑗 ∈ (1...𝑁)(𝑇 · (((𝐶‘𝑗) − (𝐷‘𝑗))↑2))) |
19 | | simprll 802 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → 𝐴 ∈ (𝔼‘𝑁)) |
20 | 19 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → 𝐴 ∈ (𝔼‘𝑁)) |
21 | | fveecn 25782 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝐴‘𝑗) ∈ ℂ) |
22 | 20, 21 | sylancom 701 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (𝐴‘𝑗) ∈ ℂ) |
23 | 22, 11 | subcld 10392 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → ((𝐴‘𝑗) − (𝐶‘𝑗)) ∈ ℂ) |
24 | 23 | sqcld 13006 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (((𝐴‘𝑗) − (𝐶‘𝑗))↑2) ∈ ℂ) |
25 | 1, 7, 24 | fsummulc2 14516 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) = Σ𝑗 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2))) |
26 | 25 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2)) = (Σ𝑗 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2))) |
27 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → 𝑇 ∈ ℂ) |
28 | 27, 24 | mulcld 10060 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) ∈ ℂ) |
29 | 22, 15 | subcld 10392 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → ((𝐴‘𝑗) − (𝐷‘𝑗)) ∈ ℂ) |
30 | 29 | sqcld 13006 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (((𝐴‘𝑗) − (𝐷‘𝑗))↑2) ∈ ℂ) |
31 | 1, 28, 30 | fsumsub 14520 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → Σ𝑗 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)) = (Σ𝑗 ∈ (1...𝑁)(𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2))) |
32 | 26, 31 | eqtr4d 2659 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2)) = Σ𝑗 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))) |
33 | 32 | oveq2d 6666 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → ((1 − 𝑇) · ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2))) = ((1 − 𝑇) · Σ𝑗 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) |
34 | | ax-1cn 9994 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
35 | | subcl 10280 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝑇
∈ ℂ) → (1 − 𝑇) ∈ ℂ) |
36 | 34, 7, 35 | sylancr 695 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (1 − 𝑇) ∈ ℂ) |
37 | 28, 30 | subcld 10392 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)) ∈ ℂ) |
38 | 1, 36, 37 | fsummulc2 14516 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → ((1 − 𝑇) · Σ𝑗 ∈ (1...𝑁)((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))) = Σ𝑗 ∈ (1...𝑁)((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) |
39 | 33, 38 | eqtrd 2656 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → ((1 − 𝑇) · ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2))) = Σ𝑗 ∈ (1...𝑁)((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) |
40 | 39 | oveq2d 6666 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) = (Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + Σ𝑗 ∈ (1...𝑁)((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
41 | | simprlr 803 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) → 𝐵 ∈ (𝔼‘𝑁)) |
42 | 41 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → 𝐵 ∈ (𝔼‘𝑁)) |
43 | | fveecn 25782 |
. . . . . . . 8
⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑗 ∈ (1...𝑁)) → (𝐵‘𝑗) ∈ ℂ) |
44 | 42, 43 | sylancom 701 |
. . . . . . 7
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (𝐵‘𝑗) ∈ ℂ) |
45 | 44, 15 | subcld 10392 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → ((𝐵‘𝑗) − (𝐷‘𝑗)) ∈ ℂ) |
46 | 45 | sqcld 13006 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (((𝐵‘𝑗) − (𝐷‘𝑗))↑2) ∈ ℂ) |
47 | 34, 27, 35 | sylancr 695 |
. . . . . 6
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (1 − 𝑇) ∈ ℂ) |
48 | 47, 37 | mulcld 10060 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))) ∈ ℂ) |
49 | 1, 46, 48 | fsumadd 14470 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → Σ𝑗 ∈ (1...𝑁)((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) = (Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + Σ𝑗 ∈ (1...𝑁)((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
50 | 40, 49 | eqtr4d 2659 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) = Σ𝑗 ∈ (1...𝑁)((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
51 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (𝐵‘𝑖) = (𝐵‘𝑗)) |
52 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐴‘𝑖) = (𝐴‘𝑗)) |
53 | 52 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → ((1 − 𝑇) · (𝐴‘𝑖)) = ((1 − 𝑇) · (𝐴‘𝑗))) |
54 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝐶‘𝑖) = (𝐶‘𝑗)) |
55 | 54 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑗 → (𝑇 · (𝐶‘𝑖)) = (𝑇 · (𝐶‘𝑗))) |
56 | 53, 55 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑖 = 𝑗 → (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗)))) |
57 | 51, 56 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑖 = 𝑗 → ((𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) ↔ (𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))))) |
58 | 57 | rspccva 3308 |
. . . . . . 7
⊢
((∀𝑖 ∈
(1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))) ∧ 𝑗 ∈ (1...𝑁)) → (𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗)))) |
59 | 58 | adantll 750 |
. . . . . 6
⊢ (((𝑇 ∈ (0[,]1) ∧
∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖)))) ∧ 𝑗 ∈ (1...𝑁)) → (𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗)))) |
60 | 59 | adantll 750 |
. . . . 5
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗)))) |
61 | | ax5seglem8 25816 |
. . . . . . 7
⊢ ((((𝐴‘𝑗) ∈ ℂ ∧ 𝑇 ∈ ℂ) ∧ ((𝐶‘𝑗) ∈ ℂ ∧ (𝐷‘𝑗) ∈ ℂ)) → (𝑇 · (((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = ((((((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
62 | | oveq1 6657 |
. . . . . . . . . 10
⊢ ((𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) → ((𝐵‘𝑗) − (𝐷‘𝑗)) = ((((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) − (𝐷‘𝑗))) |
63 | 62 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) → (((𝐵‘𝑗) − (𝐷‘𝑗))↑2) = (((((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) − (𝐷‘𝑗))↑2)) |
64 | 63 | oveq1d 6665 |
. . . . . . . 8
⊢ ((𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) → ((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) = ((((((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
65 | 64 | eqcomd 2628 |
. . . . . . 7
⊢ ((𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) → ((((((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗))) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) = ((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
66 | 61, 65 | sylan9eq 2676 |
. . . . . 6
⊢
(((((𝐴‘𝑗) ∈ ℂ ∧ 𝑇 ∈ ℂ) ∧ ((𝐶‘𝑗) ∈ ℂ ∧ (𝐷‘𝑗) ∈ ℂ)) ∧ (𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗)))) → (𝑇 · (((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = ((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
67 | 66 | 3impa 1259 |
. . . . 5
⊢ ((((𝐴‘𝑗) ∈ ℂ ∧ 𝑇 ∈ ℂ) ∧ ((𝐶‘𝑗) ∈ ℂ ∧ (𝐷‘𝑗) ∈ ℂ) ∧ (𝐵‘𝑗) = (((1 − 𝑇) · (𝐴‘𝑗)) + (𝑇 · (𝐶‘𝑗)))) → (𝑇 · (((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = ((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
68 | 22, 27, 11, 15, 60, 67 | syl221anc 1337 |
. . . 4
⊢ ((((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) ∧ 𝑗 ∈ (1...𝑁)) → (𝑇 · (((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = ((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
69 | 68 | sumeq2dv 14433 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → Σ𝑗 ∈ (1...𝑁)(𝑇 · (((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = Σ𝑗 ∈ (1...𝑁)((((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · (((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − (((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |
70 | 50, 69 | eqtr4d 2659 |
. 2
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2)))) = Σ𝑗 ∈ (1...𝑁)(𝑇 · (((𝐶‘𝑗) − (𝐷‘𝑗))↑2))) |
71 | 18, 70 | eqtr4d 2659 |
1
⊢ (((𝑁 ∈ ℕ ∧ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁)))) ∧ (𝑇 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(𝐵‘𝑖) = (((1 − 𝑇) · (𝐴‘𝑖)) + (𝑇 · (𝐶‘𝑖))))) → (𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐶‘𝑗) − (𝐷‘𝑗))↑2)) = (Σ𝑗 ∈ (1...𝑁)(((𝐵‘𝑗) − (𝐷‘𝑗))↑2) + ((1 − 𝑇) · ((𝑇 · Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐶‘𝑗))↑2)) − Σ𝑗 ∈ (1...𝑁)(((𝐴‘𝑗) − (𝐷‘𝑗))↑2))))) |