Theorem axeuclidlem 29253

Description: Lemma for axeuclid 29254. Handle the algebraic aspects of the theorem. (Contributed by Scott Fenton, 9-Sep-2013.)

Assertion

Ref	Expression
axeuclidlem	⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))

Distinct variable groups:   𝐴,𝑖,𝑟,𝑠,𝑢,𝑥,𝑦   𝐵,𝑖,𝑟,𝑠,𝑢,𝑥,𝑦   𝐶,𝑖,𝑟,𝑠,𝑢,𝑥,𝑦   𝑖,𝑁,𝑟,𝑠,𝑢,𝑥,𝑦   𝑃,𝑖,𝑟,𝑠,𝑢,𝑥,𝑦   𝑄,𝑖,𝑟,𝑠,𝑢,𝑥,𝑦   𝑇,𝑖,𝑟,𝑠,𝑢,𝑥,𝑦

Proof of Theorem axeuclidlem

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp21 1223	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → 𝑃 ∈ (0[,]1))
2		simp22 1224	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → 𝑄 ∈ (0[,]1))
3		fveere 29192	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
4	3	expcom 418	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑘) ∈ ℝ))
5		fveere 29192	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
6	5	expcom 418	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑘) ∈ ℝ))
7	4, 6	anim12d 620	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ)))
8		fveere 29192	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
9	8	expcom 418	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑘) ∈ ℝ))
10		fveere 29192	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑇‘𝑘) ∈ ℝ)
11	10	expcom 418	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑘) ∈ ℝ))
12	9, 11	anim12d 620	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
13	7, 12	anim12d 620	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ))))
14	13	impcom 412	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
15		unitssre 13526	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
16	15	sseli 3941	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℝ)
17	16	3ad2ant1 1149	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) → 𝑃 ∈ ℝ)
18	17	adantl 486	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℝ)
19		peano2rem 11525	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
20	18, 19	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℝ)
21		simplll 786	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑘) ∈ ℝ)
22	20, 21	remulcld 11239	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑘)) ∈ ℝ)
23		simpllr 787	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑘) ∈ ℝ)
24	22, 23	readdcld 11238	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) ∈ ℝ)
25		simpr3 1213	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
26	24, 18, 25	redivcld 12043	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
27	14, 26	sylan 591	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
28	27	an32s 664	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
29	28	ralrimiva 3163	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
30		eleenn 29187	. . . . . . . 8 ⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
31	30	ad3antrrr 742	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑁 ∈ ℕ)
32		mptelee 29185	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ))
33	31, 32	syl 18	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ))
34	29, 33	mpbird 260	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
35	34	3adant3 1148	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
36		simplrl 788	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑘) ∈ ℝ)
37	22, 36	readdcld 11238	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) ∈ ℝ)
38	37, 18, 25	redivcld 12043	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
39	14, 38	sylan 591	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
40	39	an32s 664	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
41	40	ralrimiva 3163	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
42		mptelee 29185	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ))
43	31, 42	syl 18	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ))
44	41, 43	mpbird 260	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
45	44	3adant3 1148	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
46		fveecn 29193	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
47	46	expcom 418	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑖) ∈ ℂ))
48		fveecn 29193	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
49	48	expcom 418	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑖) ∈ ℂ))
50	47, 49	anim12d 620	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ)))
51		fveecn 29193	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
52	51	expcom 418	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑖) ∈ ℂ))
53		fveecn 29193	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
54	53	expcom 418	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑖) ∈ ℂ))
55	52, 54	anim12d 620	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
56	50, 55	anim12d 620	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ))))
57	56	impcom 412	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
58		eqcom 2776	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖))
59		ax-1cn 11158	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
60		simpr2 1212	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ (0[,]1))
61	15	sseli 3941	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℝ)
62	61	recnd 11237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℂ)
63	60, 62	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ ℂ)
64		subcl 11456	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → (1 − 𝑄) ∈ ℂ)
65	59, 63, 64	sylancr 598	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑄) ∈ ℂ)
66		simpr1 1211	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ (0[,]1))
67	16	recnd 11237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℂ)
68	66, 67	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℂ)
69		subcl 11456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 − 1) ∈ ℂ)
70	68, 59, 69	sylancl 597	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℂ)
71		simplll 786	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑖) ∈ ℂ)
72	70, 71	mulcld 11229	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) ∈ ℂ)
73	65, 72	mulcld 11229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
74	63, 72	mulcld 11229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
75	73, 74	addcld 11228	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) ∈ ℂ)
76		simpllr 787	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) ∈ ℂ)
77	65, 76	mulcld 11229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (𝐵‘𝑖)) ∈ ℂ)
78		simplrl 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) ∈ ℂ)
79	63, 78	mulcld 11229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (𝐶‘𝑖)) ∈ ℂ)
80	77, 79	addcld 11228	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ∈ ℂ)
81	75, 80	addcld 11228	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) ∈ ℂ)
82		simplrr 789	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑇‘𝑖) ∈ ℂ)
83		simpr3 1213	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
84	81, 68, 82, 83	divmuld 12013	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
85	58, 84	bitrid 286	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
86		negsubdi2 11517	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → -(1 − 𝑃) = (𝑃 − 1))
87	59, 68, 86	sylancr 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -(1 − 𝑃) = (𝑃 − 1))
88	87	oveq1d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = ((𝑃 − 1) · (𝐴‘𝑖)))
89		subcl 11456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (1 − 𝑃) ∈ ℂ)
90	59, 68, 89	sylancr 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑃) ∈ ℂ)
91	90, 71	mulneg1d 11667	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = -((1 − 𝑃) · (𝐴‘𝑖)))
92		npcan 11466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → ((1 − 𝑄) + 𝑄) = 1)
93	59, 63, 92	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) + 𝑄) = 1)
94	93	oveq1d 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (1 · ((𝑃 − 1) · (𝐴‘𝑖))))
95	65, 63, 72	adddird 11234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
96	72	mullidd 11227	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 · ((𝑃 − 1) · (𝐴‘𝑖))) = ((𝑃 − 1) · (𝐴‘𝑖)))
97	94, 95, 96	3eqtr3rd 2813	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
98	88, 91, 97	3eqtr3d 2812	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -((1 − 𝑃) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
99	98	oveq2d 7427	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))))
100	90, 71	mulcld 11229	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) · (𝐴‘𝑖)) ∈ ℂ)
101	80, 100	negsubd 11575	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))))
102	80, 75	addcomd 11412	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
103	99, 101, 102	3eqtr3d 2812	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
104	103	eqeq1d 2771	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖))))
105		eqcom 2776	. . . . . . . . . . . . . 14 ⊢ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖)) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
106	104, 105	bitrdi 290	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
107	85, 106	bitr4d 285	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖))))
108	73, 74, 77, 79	add4d 11439	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
109	65, 72, 76	adddid 11233	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))))
110	63, 72, 78	adddid 11233	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) = ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖))))
111	109, 110	oveq12d 7429	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
112	108, 111	eqtr4d 2807	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))))
113	112	oveq1d 7426	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃))
114	72, 76	addcld 11228	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) ∈ ℂ)
115	65, 114	mulcld 11229	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) ∈ ℂ)
116	72, 78	addcld 11228	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) ∈ ℂ)
117	63, 116	mulcld 11229	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) ∈ ℂ)
118	115, 117, 68, 83	divdird 12029	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)))
119	65, 114, 68, 83	divassd 12026	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
120	63, 116, 68, 83	divassd 12026	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
121	119, 120	oveq12d 7429	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
122	113, 118, 121	3eqtrd 2808	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
123	122	eqeq2d 2780	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
124	68, 82	mulcld 11229	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · (𝑇‘𝑖)) ∈ ℂ)
125	80, 100, 124	subaddd 11587	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
126	107, 123, 125	3bitr3rd 313	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
127	126	biimpd 232	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
128		npncan2 11485	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
129	59, 68, 128	sylancr 598	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
130	129	oveq1d 7426	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (0 · (𝐴‘𝑖)))
131	90, 70, 71	adddird 11234	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))))
132		mul02 11388	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑖) ∈ ℂ → (0 · (𝐴‘𝑖)) = 0)
133	132	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 · (𝐴‘𝑖)) = 0)
134	130, 131, 133	3eqtr3d 2812	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) = 0)
135	134	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (0 + (𝐵‘𝑖)))
136	100, 72, 76	addassd 11231	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
137	76	addlidd 11411	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐵‘𝑖)) = (𝐵‘𝑖))
138	135, 136, 137	3eqtr3rd 2813	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
139	114, 68, 83	divcan2d 11993	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
140	139	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
141	138, 140	eqtr4d 2807	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
142	134	oveq1d 7426	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (0 + (𝐶‘𝑖)))
143	100, 72, 78	addassd 11231	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
144	78	addlidd 11411	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐶‘𝑖)) = (𝐶‘𝑖))
145	142, 143, 144	3eqtr3rd 2813	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
146	116, 68, 83	divcan2d 11993	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
147	146	oveq2d 7427	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
148	145, 147	eqtr4d 2807	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
149	141, 148	jca 520	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
150	127, 149	jctild 534	. . . . . . . . 9 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
151		df-3an 1103	. . . . . . . . 9 ⊢ (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ↔ (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
152	150, 151	imbitrrdi 255	. . . . . . . 8 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
153	57, 152	sylan 591	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
154	153	an32s 664	. . . . . 6 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
155	154	ralimdva 3183	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
156	155	3impia 1133	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
157		fveq1 6881	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖))
158		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
159	158	oveq2d 7427	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝑃 − 1) · (𝐴‘𝑘)) = ((𝑃 − 1) · (𝐴‘𝑖)))
160		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
161	159, 160	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
162	161	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
163		eqid 2769	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))
164		ovex 7444	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) ∈ V
165	162, 163, 164	fvmpt 6990	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
166	157, 165	sylan9eq 2824	. . . . . . 7 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
167		oveq2 7419	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (𝑃 · (𝑥‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
168	167	oveq2d 7427	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
169	168	eqeq2d 2780	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))))
170		oveq2 7419	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((1 − 𝑄) · (𝑥‘𝑖)) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
171	170	oveq1d 7426	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))
172	171	eqeq2d 2780	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))))
173	169, 172	3anbi13d 1464	. . . . . . 7 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
174	166, 173	syl 18	. . . . . 6 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
175	174	ralbidva 3192	. . . . 5 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
176		fveq1 6881	. . . . . . . 8 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (𝑦‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖))
177		fveq2 6882	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
178	159, 177	oveq12d 7429	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
179	178	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
180		eqid 2769	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))
181		ovex 7444	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) ∈ V
182	179, 180, 181	fvmpt 6990	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
183	176, 182	sylan9eq 2824	. . . . . . 7 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
184		oveq2 7419	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑃 · (𝑦‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
185	184	oveq2d 7427	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
186	185	eqeq2d 2780	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
187		oveq2 7419	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑄 · (𝑦‘𝑖)) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
188	187	oveq2d 7427	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
189	188	eqeq2d 2780	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
190	186, 189	3anbi23d 1465	. . . . . . 7 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
191	183, 190	syl 18	. . . . . 6 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
192	191	ralbidva 3192	. . . . 5 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
193	175, 192	rspc2ev 3603	. . . 4 ⊢ (((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
194	35, 45, 156, 193	syl3anc 1396	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
195		oveq2 7419	. . . . . . . . . 10 ⊢ (𝑟 = 𝑃 → (1 − 𝑟) = (1 − 𝑃))
196	195	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → ((1 − 𝑟) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
197		oveq1 7418	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → (𝑟 · (𝑥‘𝑖)) = (𝑃 · (𝑥‘𝑖)))
198	196, 197	oveq12d 7429	. . . . . . . 8 ⊢ (𝑟 = 𝑃 → (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))))
199	198	eqeq2d 2780	. . . . . . 7 ⊢ (𝑟 = 𝑃 → ((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖)))))
200	199	3anbi1d 1466	. . . . . 6 ⊢ (𝑟 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
201	200	ralbidv 3194	. . . . 5 ⊢ (𝑟 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
202	201	2rexbidv 3236	. . . 4 ⊢ (𝑟 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
203		oveq2 7419	. . . . . . . . . 10 ⊢ (𝑠 = 𝑃 → (1 − 𝑠) = (1 − 𝑃))
204	203	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → ((1 − 𝑠) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
205		oveq1 7418	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 · (𝑦‘𝑖)) = (𝑃 · (𝑦‘𝑖)))
206	204, 205	oveq12d 7429	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))))
207	206	eqeq2d 2780	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖)))))
208	207	3anbi2d 1467	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
209	208	ralbidv 3194	. . . . 5 ⊢ (𝑠 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
210	209	2rexbidv 3236	. . . 4 ⊢ (𝑠 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
211		oveq2 7419	. . . . . . . . . 10 ⊢ (𝑢 = 𝑄 → (1 − 𝑢) = (1 − 𝑄))
212	211	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → ((1 − 𝑢) · (𝑥‘𝑖)) = ((1 − 𝑄) · (𝑥‘𝑖)))
213		oveq1 7418	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → (𝑢 · (𝑦‘𝑖)) = (𝑄 · (𝑦‘𝑖)))
214	212, 213	oveq12d 7429	. . . . . . . 8 ⊢ (𝑢 = 𝑄 → (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))
215	214	eqeq2d 2780	. . . . . . 7 ⊢ (𝑢 = 𝑄 → ((𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
216	215	3anbi3d 1468	. . . . . 6 ⊢ (𝑢 = 𝑄 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
217	216	ralbidv 3194	. . . . 5 ⊢ (𝑢 = 𝑄 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
218	217	2rexbidv 3236	. . . 4 ⊢ (𝑢 = 𝑄 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
219	202, 210, 218	rspc3ev 3607	. . 3 ⊢ (((𝑃 ∈ (0[,]1) ∧ 𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1)) ∧ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))) → ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
220	1, 1, 2, 194, 219	syl31anc 1398	. 2 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
221		rexcom 3300	. . . . . 6 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
222	221	rexbii 3118	. . . . 5 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
223		rexcom 3300	. . . . 5 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
224	222, 223	bitri 278	. . . 4 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
225	224	rexbii 3118	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
226		rexcom 3300	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
227		rexcom 3300	. . . . . . . 8 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
228	227	rexbii 3118	. . . . . . 7 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
229		rexcom 3300	. . . . . . 7 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
230	228, 229	bitri 278	. . . . . 6 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
231	230	rexbii 3118	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
232		rexcom 3300	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
233	231, 232	bitri 278	. . . 4 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
234	233	rexbii 3118	. . 3 ⊢ (∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
235	225, 226, 234	3bitri 300	. 2 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
236	220, 235	sylib 221	1 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085  ∃wrex 3095   ↦ cmpt 5196  ‘cfv 6537  (class class class)co 7411  ℂcc 11098  ℝcr 11099  0cc0 11100  1c1 11101   + caddc 11103   · cmul 11105   − cmin 11441  -cneg 11442   / cdiv 11871  ℕcn 12233  [,]cicc 13375  ...cfz 13535  𝔼cee 29178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-po 5570  df-so 5571  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-er 8694  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872  df-icc 13379  df-ee 29181

This theorem is referenced by:  axeuclid  29254