Theorem axeuclidlem 28008

Description: Lemma for axeuclid 28009. 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 1206	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → 𝑃 ∈ (0[,]1))
2		simp22 1207	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → 𝑄 ∈ (0[,]1))
3		fveere 27947	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
4	3	expcom 414	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑘) ∈ ℝ))
5		fveere 27947	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
6	5	expcom 414	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑘) ∈ ℝ))
7	4, 6	anim12d 609	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ)))
8		fveere 27947	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
9	8	expcom 414	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑘) ∈ ℝ))
10		fveere 27947	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑇‘𝑘) ∈ ℝ)
11	10	expcom 414	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑘) ∈ ℝ))
12	9, 11	anim12d 609	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
13	7, 12	anim12d 609	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ))))
14	13	impcom 408	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
15		unitssre 13441	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
16	15	sseli 3958	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℝ)
17	16	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) → 𝑃 ∈ ℝ)
18	17	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℝ)
19		peano2rem 11492	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
20	18, 19	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℝ)
21		simplll 773	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑘) ∈ ℝ)
22	20, 21	remulcld 11209	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑘)) ∈ ℝ)
23		simpllr 774	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑘) ∈ ℝ)
24	22, 23	readdcld 11208	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) ∈ ℝ)
25		simpr3 1196	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
26	24, 18, 25	redivcld 12007	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
27	14, 26	sylan 580	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
28	27	an32s 650	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
29	28	ralrimiva 3145	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
30		eleenn 27942	. . . . . . . 8 ⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
31	30	ad3antrrr 728	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑁 ∈ ℕ)
32		mptelee 27941	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ))
33	31, 32	syl 17	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ))
34	29, 33	mpbird 256	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
35	34	3adant3 1132	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
36		simplrl 775	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑘) ∈ ℝ)
37	22, 36	readdcld 11208	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) ∈ ℝ)
38	37, 18, 25	redivcld 12007	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
39	14, 38	sylan 580	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
40	39	an32s 650	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
41	40	ralrimiva 3145	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
42		mptelee 27941	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ))
43	31, 42	syl 17	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ))
44	41, 43	mpbird 256	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
45	44	3adant3 1132	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
46		fveecn 27948	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
47	46	expcom 414	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑖) ∈ ℂ))
48		fveecn 27948	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
49	48	expcom 414	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑖) ∈ ℂ))
50	47, 49	anim12d 609	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ)))
51		fveecn 27948	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
52	51	expcom 414	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑖) ∈ ℂ))
53		fveecn 27948	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
54	53	expcom 414	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑖) ∈ ℂ))
55	52, 54	anim12d 609	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
56	50, 55	anim12d 609	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ))))
57	56	impcom 408	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
58		eqcom 2738	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖))
59		ax-1cn 11133	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
60		simpr2 1195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ (0[,]1))
61	15	sseli 3958	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℝ)
62	61	recnd 11207	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℂ)
63	60, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ ℂ)
64		subcl 11424	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → (1 − 𝑄) ∈ ℂ)
65	59, 63, 64	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑄) ∈ ℂ)
66		simpr1 1194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ (0[,]1))
67	16	recnd 11207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℂ)
68	66, 67	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℂ)
69		subcl 11424	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 − 1) ∈ ℂ)
70	68, 59, 69	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℂ)
71		simplll 773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑖) ∈ ℂ)
72	70, 71	mulcld 11199	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) ∈ ℂ)
73	65, 72	mulcld 11199	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
74	63, 72	mulcld 11199	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
75	73, 74	addcld 11198	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) ∈ ℂ)
76		simpllr 774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) ∈ ℂ)
77	65, 76	mulcld 11199	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (𝐵‘𝑖)) ∈ ℂ)
78		simplrl 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) ∈ ℂ)
79	63, 78	mulcld 11199	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (𝐶‘𝑖)) ∈ ℂ)
80	77, 79	addcld 11198	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ∈ ℂ)
81	75, 80	addcld 11198	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) ∈ ℂ)
82		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑇‘𝑖) ∈ ℂ)
83		simpr3 1196	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
84	81, 68, 82, 83	divmuld 11977	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
85	58, 84	bitrid 282	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
86		negsubdi2 11484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → -(1 − 𝑃) = (𝑃 − 1))
87	59, 68, 86	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -(1 − 𝑃) = (𝑃 − 1))
88	87	oveq1d 7392	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = ((𝑃 − 1) · (𝐴‘𝑖)))
89		subcl 11424	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (1 − 𝑃) ∈ ℂ)
90	59, 68, 89	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑃) ∈ ℂ)
91	90, 71	mulneg1d 11632	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = -((1 − 𝑃) · (𝐴‘𝑖)))
92		npcan 11434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → ((1 − 𝑄) + 𝑄) = 1)
93	59, 63, 92	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) + 𝑄) = 1)
94	93	oveq1d 7392	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (1 · ((𝑃 − 1) · (𝐴‘𝑖))))
95	65, 63, 72	adddird 11204	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
96	72	mullidd 11197	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 · ((𝑃 − 1) · (𝐴‘𝑖))) = ((𝑃 − 1) · (𝐴‘𝑖)))
97	94, 95, 96	3eqtr3rd 2780	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
98	88, 91, 97	3eqtr3d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -((1 − 𝑃) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
99	98	oveq2d 7393	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))))
100	90, 71	mulcld 11199	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) · (𝐴‘𝑖)) ∈ ℂ)
101	80, 100	negsubd 11542	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))))
102	80, 75	addcomd 11381	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
103	99, 101, 102	3eqtr3d 2779	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
104	103	eqeq1d 2733	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖))))
105		eqcom 2738	. . . . . . . . . . . . . 14 ⊢ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖)) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
106	104, 105	bitrdi 286	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
107	85, 106	bitr4d 281	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖))))
108	73, 74, 77, 79	add4d 11407	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
109	65, 72, 76	adddid 11203	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))))
110	63, 72, 78	adddid 11203	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) = ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖))))
111	109, 110	oveq12d 7395	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
112	108, 111	eqtr4d 2774	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))))
113	112	oveq1d 7392	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃))
114	72, 76	addcld 11198	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) ∈ ℂ)
115	65, 114	mulcld 11199	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) ∈ ℂ)
116	72, 78	addcld 11198	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) ∈ ℂ)
117	63, 116	mulcld 11199	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) ∈ ℂ)
118	115, 117, 68, 83	divdird 11993	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)))
119	65, 114, 68, 83	divassd 11990	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
120	63, 116, 68, 83	divassd 11990	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
121	119, 120	oveq12d 7395	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
122	113, 118, 121	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
123	122	eqeq2d 2742	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
124	68, 82	mulcld 11199	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · (𝑇‘𝑖)) ∈ ℂ)
125	80, 100, 124	subaddd 11554	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
126	107, 123, 125	3bitr3rd 309	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
127	126	biimpd 228	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
128		npncan2 11452	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
129	59, 68, 128	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
130	129	oveq1d 7392	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (0 · (𝐴‘𝑖)))
131	90, 70, 71	adddird 11204	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))))
132		mul02 11357	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑖) ∈ ℂ → (0 · (𝐴‘𝑖)) = 0)
133	132	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 · (𝐴‘𝑖)) = 0)
134	130, 131, 133	3eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) = 0)
135	134	oveq1d 7392	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (0 + (𝐵‘𝑖)))
136	100, 72, 76	addassd 11201	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
137	76	addlidd 11380	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐵‘𝑖)) = (𝐵‘𝑖))
138	135, 136, 137	3eqtr3rd 2780	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
139	114, 68, 83	divcan2d 11957	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
140	139	oveq2d 7393	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
141	138, 140	eqtr4d 2774	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
142	134	oveq1d 7392	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (0 + (𝐶‘𝑖)))
143	100, 72, 78	addassd 11201	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
144	78	addlidd 11380	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐶‘𝑖)) = (𝐶‘𝑖))
145	142, 143, 144	3eqtr3rd 2780	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
146	116, 68, 83	divcan2d 11957	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
147	146	oveq2d 7393	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
148	145, 147	eqtr4d 2774	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
149	141, 148	jca 512	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
150	127, 149	jctild 526	. . . . . . . . 9 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
151		df-3an 1089	. . . . . . . . 9 ⊢ (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ↔ (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
152	150, 151	syl6ibr 251	. . . . . . . 8 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
153	57, 152	sylan 580	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
154	153	an32s 650	. . . . . 6 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
155	154	ralimdva 3166	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
156	155	3impia 1117	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
157		fveq1 6861	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖))
158		fveq2 6862	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
159	158	oveq2d 7393	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝑃 − 1) · (𝐴‘𝑘)) = ((𝑃 − 1) · (𝐴‘𝑖)))
160		fveq2 6862	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
161	159, 160	oveq12d 7395	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
162	161	oveq1d 7392	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
163		eqid 2731	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))
164		ovex 7410	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) ∈ V
165	162, 163, 164	fvmpt 6968	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
166	157, 165	sylan9eq 2791	. . . . . . 7 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
167		oveq2 7385	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (𝑃 · (𝑥‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
168	167	oveq2d 7393	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
169	168	eqeq2d 2742	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))))
170		oveq2 7385	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((1 − 𝑄) · (𝑥‘𝑖)) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
171	170	oveq1d 7392	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))
172	171	eqeq2d 2742	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))))
173	169, 172	3anbi13d 1438	. . . . . . 7 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
174	166, 173	syl 17	. . . . . 6 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
175	174	ralbidva 3174	. . . . 5 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
176		fveq1 6861	. . . . . . . 8 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (𝑦‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖))
177		fveq2 6862	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
178	159, 177	oveq12d 7395	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
179	178	oveq1d 7392	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
180		eqid 2731	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))
181		ovex 7410	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) ∈ V
182	179, 180, 181	fvmpt 6968	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
183	176, 182	sylan9eq 2791	. . . . . . 7 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
184		oveq2 7385	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑃 · (𝑦‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
185	184	oveq2d 7393	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
186	185	eqeq2d 2742	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
187		oveq2 7385	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑄 · (𝑦‘𝑖)) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
188	187	oveq2d 7393	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
189	188	eqeq2d 2742	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
190	186, 189	3anbi23d 1439	. . . . . . 7 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
191	183, 190	syl 17	. . . . . 6 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
192	191	ralbidva 3174	. . . . 5 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
193	175, 192	rspc2ev 3606	. . . 4 ⊢ (((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
194	35, 45, 156, 193	syl3anc 1371	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
195		oveq2 7385	. . . . . . . . . 10 ⊢ (𝑟 = 𝑃 → (1 − 𝑟) = (1 − 𝑃))
196	195	oveq1d 7392	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → ((1 − 𝑟) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
197		oveq1 7384	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → (𝑟 · (𝑥‘𝑖)) = (𝑃 · (𝑥‘𝑖)))
198	196, 197	oveq12d 7395	. . . . . . . 8 ⊢ (𝑟 = 𝑃 → (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))))
199	198	eqeq2d 2742	. . . . . . 7 ⊢ (𝑟 = 𝑃 → ((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖)))))
200	199	3anbi1d 1440	. . . . . 6 ⊢ (𝑟 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
201	200	ralbidv 3176	. . . . 5 ⊢ (𝑟 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
202	201	2rexbidv 3218	. . . 4 ⊢ (𝑟 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
203		oveq2 7385	. . . . . . . . . 10 ⊢ (𝑠 = 𝑃 → (1 − 𝑠) = (1 − 𝑃))
204	203	oveq1d 7392	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → ((1 − 𝑠) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
205		oveq1 7384	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 · (𝑦‘𝑖)) = (𝑃 · (𝑦‘𝑖)))
206	204, 205	oveq12d 7395	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))))
207	206	eqeq2d 2742	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖)))))
208	207	3anbi2d 1441	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
209	208	ralbidv 3176	. . . . 5 ⊢ (𝑠 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
210	209	2rexbidv 3218	. . . 4 ⊢ (𝑠 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
211		oveq2 7385	. . . . . . . . . 10 ⊢ (𝑢 = 𝑄 → (1 − 𝑢) = (1 − 𝑄))
212	211	oveq1d 7392	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → ((1 − 𝑢) · (𝑥‘𝑖)) = ((1 − 𝑄) · (𝑥‘𝑖)))
213		oveq1 7384	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → (𝑢 · (𝑦‘𝑖)) = (𝑄 · (𝑦‘𝑖)))
214	212, 213	oveq12d 7395	. . . . . . . 8 ⊢ (𝑢 = 𝑄 → (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))
215	214	eqeq2d 2742	. . . . . . 7 ⊢ (𝑢 = 𝑄 → ((𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
216	215	3anbi3d 1442	. . . . . 6 ⊢ (𝑢 = 𝑄 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
217	216	ralbidv 3176	. . . . 5 ⊢ (𝑢 = 𝑄 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
218	217	2rexbidv 3218	. . . 4 ⊢ (𝑢 = 𝑄 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
219	202, 210, 218	rspc3ev 3609	. . 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 1373	. 2 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
221		rexcom 3284	. . . . . 6 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
222	221	rexbii 3093	. . . . 5 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
223		rexcom 3284	. . . . 5 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
224	222, 223	bitri 274	. . . 4 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
225	224	rexbii 3093	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
226		rexcom 3284	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
227		rexcom 3284	. . . . . . . 8 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
228	227	rexbii 3093	. . . . . . 7 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
229		rexcom 3284	. . . . . . 7 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
230	228, 229	bitri 274	. . . . . 6 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
231	230	rexbii 3093	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
232		rexcom 3284	. . . . 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 274	. . . 4 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
234	233	rexbii 3093	. . 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 296	. 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 217	1 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ↦ cmpt 5208  ‘cfv 6516  (class class class)co 7377  ℂcc 11073  ℝcr 11074  0cc0 11075  1c1 11076   + caddc 11078   · cmul 11080   − cmin 11409  -cneg 11410   / cdiv 11836  ℕcn 12177  [,]cicc 13292  ...cfz 13449  𝔼cee 27934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3364  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-br 5126  df-opab 5188  df-mpt 5209  df-id 5551  df-po 5565  df-so 5566  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-er 8670  df-map 8789  df-en 8906  df-dom 8907  df-sdom 8908  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11411  df-neg 11412  df-div 11837  df-icc 13296  df-ee 27937

This theorem is referenced by:  axeuclid  28009