Theorem axeuclidlem 29555

Description: Lemma for axeuclid 29556. 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 1225	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → 𝑃 ∈ (0[,]1))
2		simp22 1226	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → 𝑄 ∈ (0[,]1))
3		fveere 29494	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
4	3	expcom 419	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑘) ∈ ℝ))
5		fveere 29494	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
6	5	expcom 419	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑘) ∈ ℝ))
7	4, 6	anim12d 621	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ)))
8		fveere 29494	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
9	8	expcom 419	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑘) ∈ ℝ))
10		fveere 29494	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑇‘𝑘) ∈ ℝ)
11	10	expcom 419	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑘) ∈ ℝ))
12	9, 11	anim12d 621	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
13	7, 12	anim12d 621	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ))))
14	13	impcom 413	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
15		unitssre 13643	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
16	15	sseli 3909	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℝ)
17	16	3ad2ant1 1151	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) → 𝑃 ∈ ℝ)
18	17	adantl 487	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℝ)
19		peano2rem 11638	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
20	18, 19	syl 18	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℝ)
21		simplll 787	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑘) ∈ ℝ)
22	20, 21	remulcld 11352	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑘)) ∈ ℝ)
23		simpllr 788	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑘) ∈ ℝ)
24	22, 23	readdcld 11351	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) ∈ ℝ)
25		simpr3 1215	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
26	24, 18, 25	redivcld 12158	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
27	14, 26	sylan 592	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
28	27	an32s 665	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
29	28	ralrimiva 3158	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
30		eleenn 29489	. . . . . . . 8 ⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
31	30	ad3antrrr 743	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑁 ∈ ℕ)
32		mptelee 29487	. . . . . . 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 1150	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
36		simplrl 789	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑘) ∈ ℝ)
37	22, 36	readdcld 11351	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) ∈ ℝ)
38	37, 18, 25	redivcld 12158	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
39	14, 38	sylan 592	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
40	39	an32s 665	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
41	40	ralrimiva 3158	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
42		mptelee 29487	. . . . . . 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 1150	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁))
46		fveecn 29495	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
47	46	expcom 419	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑖) ∈ ℂ))
48		fveecn 29495	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
49	48	expcom 419	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑖) ∈ ℂ))
50	47, 49	anim12d 621	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ)))
51		fveecn 29495	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
52	51	expcom 419	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑖) ∈ ℂ))
53		fveecn 29495	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
54	53	expcom 419	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑖) ∈ ℂ))
55	52, 54	anim12d 621	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
56	50, 55	anim12d 621	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ))))
57	56	impcom 413	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
58		eqcom 2770	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖))
59		ax-1cn 11271	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
60		simpr2 1214	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ (0[,]1))
61	15	sseli 3909	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℝ)
62	61	recnd 11350	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℂ)
63	60, 62	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ ℂ)
64		subcl 11569	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → (1 − 𝑄) ∈ ℂ)
65	59, 63, 64	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑄) ∈ ℂ)
66		simpr1 1213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ (0[,]1))
67	16	recnd 11350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℂ)
68	66, 67	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℂ)
69		subcl 11569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 − 1) ∈ ℂ)
70	68, 59, 69	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℂ)
71		simplll 787	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑖) ∈ ℂ)
72	70, 71	mulcld 11342	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) ∈ ℂ)
73	65, 72	mulcld 11342	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
74	63, 72	mulcld 11342	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
75	73, 74	addcld 11341	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) ∈ ℂ)
76		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) ∈ ℂ)
77	65, 76	mulcld 11342	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (𝐵‘𝑖)) ∈ ℂ)
78		simplrl 789	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) ∈ ℂ)
79	63, 78	mulcld 11342	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (𝐶‘𝑖)) ∈ ℂ)
80	77, 79	addcld 11341	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ∈ ℂ)
81	75, 80	addcld 11341	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) ∈ ℂ)
82		simplrr 790	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑇‘𝑖) ∈ ℂ)
83		simpr3 1215	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
84	81, 68, 82, 83	divmuld 12128	. . . . . . . . . . . . . 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 11630	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → -(1 − 𝑃) = (𝑃 − 1))
87	59, 68, 86	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -(1 − 𝑃) = (𝑃 − 1))
88	87	oveq1d 7445	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ( -(1 − 𝑃) · (𝐴‘𝑖)) = ((𝑃 − 1) · (𝐴‘𝑖)))
89		subcl 11569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (1 − 𝑃) ∈ ℂ)
90	59, 68, 89	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑃) ∈ ℂ)
91	90, 71	mulneg1d 11782	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ( -(1 − 𝑃) · (𝐴‘𝑖)) = -((1 − 𝑃) · (𝐴‘𝑖)))
92		npcan 11579	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → ((1 − 𝑄) + 𝑄) = 1)
93	59, 63, 92	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) + 𝑄) = 1)
94	93	oveq1d 7445	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (1 · ((𝑃 − 1) · (𝐴‘𝑖))))
95	65, 63, 72	adddird 11347	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
96	72	mullidd 11340	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 · ((𝑃 − 1) · (𝐴‘𝑖))) = ((𝑃 − 1) · (𝐴‘𝑖)))
97	94, 95, 96	3eqtr3rd 2807	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
98	88, 91, 97	3eqtr3d 2806	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -((1 − 𝑃) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
99	98	oveq2d 7446	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))))
100	90, 71	mulcld 11342	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) · (𝐴‘𝑖)) ∈ ℂ)
101	80, 100	negsubd 11688	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))))
102	80, 75	addcomd 11525	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
103	99, 101, 102	3eqtr3d 2806	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
104	103	eqeq1d 2765	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖))))
105		eqcom 2770	. . . . . . . . . . . . . 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 11552	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
109	65, 72, 76	adddid 11346	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))))
110	63, 72, 78	adddid 11346	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) = ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖))))
111	109, 110	oveq12d 7448	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
112	108, 111	eqtr4d 2801	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))))
113	112	oveq1d 7445	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃))
114	72, 76	addcld 11341	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) ∈ ℂ)
115	65, 114	mulcld 11342	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) ∈ ℂ)
116	72, 78	addcld 11341	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) ∈ ℂ)
117	63, 116	mulcld 11342	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) ∈ ℂ)
118	115, 117, 68, 83	divdird 12144	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)))
119	65, 114, 68, 83	divassd 12141	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
120	63, 116, 68, 83	divassd 12141	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
121	119, 120	oveq12d 7448	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
122	113, 118, 121	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
123	122	eqeq2d 2774	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
124	68, 82	mulcld 11342	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · (𝑇‘𝑖)) ∈ ℂ)
125	80, 100, 124	subaddd 11700	. . . . . . . . . . . 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 11598	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
129	59, 68, 128	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
130	129	oveq1d 7445	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (0 · (𝐴‘𝑖)))
131	90, 70, 71	adddird 11347	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))))
132		mul02 11501	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑖) ∈ ℂ → (0 · (𝐴‘𝑖)) = 0)
133	132	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 · (𝐴‘𝑖)) = 0)
134	130, 131, 133	3eqtr3d 2806	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) = 0)
135	134	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (0 + (𝐵‘𝑖)))
136	100, 72, 76	addassd 11344	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
137	76	addlidd 11524	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐵‘𝑖)) = (𝐵‘𝑖))
138	135, 136, 137	3eqtr3rd 2807	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
139	114, 68, 83	divcan2d 12108	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
140	139	oveq2d 7446	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
141	138, 140	eqtr4d 2801	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
142	134	oveq1d 7445	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (0 + (𝐶‘𝑖)))
143	100, 72, 78	addassd 11344	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
144	78	addlidd 11524	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐶‘𝑖)) = (𝐶‘𝑖))
145	142, 143, 144	3eqtr3rd 2807	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
146	116, 68, 83	divcan2d 12108	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
147	146	oveq2d 7446	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
148	145, 147	eqtr4d 2801	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
149	141, 148	jca 521	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
150	127, 149	jctild 535	. . . . . . . . 9 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
151		df-3an 1105	. . . . . . . . 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 592	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
154	153	an32s 665	. . . . . 6 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
155	154	ralimdva 3178	. . . . 5 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
156	155	3impia 1135	. . . 4 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
157		fveq1 6895	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖))
158		fveq2 6896	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
159	158	oveq2d 7446	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝑃 − 1) · (𝐴‘𝑘)) = ((𝑃 − 1) · (𝐴‘𝑖)))
160		fveq2 6896	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
161	159, 160	oveq12d 7448	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
162	161	oveq1d 7445	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
163		eqid 2763	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))
164		ovex 7463	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) ∈ V
165	162, 163, 164	fvmpt 7004	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
166	157, 165	sylan9eq 2818	. . . . . . 7 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
167		oveq2 7438	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (𝑃 · (𝑥‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
168	167	oveq2d 7446	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
169	168	eqeq2d 2774	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))))
170		oveq2 7438	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((1 − 𝑄) · (𝑥‘𝑖)) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
171	170	oveq1d 7445	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))
172	171	eqeq2d 2774	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))))
173	169, 172	3anbi13d 1466	. . . . . . 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 3187	. . . . 5 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
176		fveq1 6895	. . . . . . . 8 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (𝑦‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖))
177		fveq2 6896	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
178	159, 177	oveq12d 7448	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
179	178	oveq1d 7445	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
180		eqid 2763	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))
181		ovex 7463	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) ∈ V
182	179, 180, 181	fvmpt 7004	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
183	176, 182	sylan9eq 2818	. . . . . . 7 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
184		oveq2 7438	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑃 · (𝑦‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
185	184	oveq2d 7446	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
186	185	eqeq2d 2774	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
187		oveq2 7438	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑄 · (𝑦‘𝑖)) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
188	187	oveq2d 7446	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
189	188	eqeq2d 2774	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
190	186, 189	3anbi23d 1467	. . . . . . 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 3187	. . . . 5 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
193	175, 192	rspc2ev 3592	. . . 4 ⊢ (((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
194	35, 45, 156, 193	syl3anc 1398	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
195		oveq2 7438	. . . . . . . . . 10 ⊢ (𝑟 = 𝑃 → (1 − 𝑟) = (1 − 𝑃))
196	195	oveq1d 7445	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → ((1 − 𝑟) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
197		oveq1 7437	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → (𝑟 · (𝑥‘𝑖)) = (𝑃 · (𝑥‘𝑖)))
198	196, 197	oveq12d 7448	. . . . . . . 8 ⊢ (𝑟 = 𝑃 → (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))))
199	198	eqeq2d 2774	. . . . . . 7 ⊢ (𝑟 = 𝑃 → ((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖)))))
200	199	3anbi1d 1468	. . . . . 6 ⊢ (𝑟 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
201	200	ralbidv 3189	. . . . 5 ⊢ (𝑟 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
202	201	2rexbidv 3231	. . . 4 ⊢ (𝑟 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
203		oveq2 7438	. . . . . . . . . 10 ⊢ (𝑠 = 𝑃 → (1 − 𝑠) = (1 − 𝑃))
204	203	oveq1d 7445	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → ((1 − 𝑠) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
205		oveq1 7437	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 · (𝑦‘𝑖)) = (𝑃 · (𝑦‘𝑖)))
206	204, 205	oveq12d 7448	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))))
207	206	eqeq2d 2774	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖)))))
208	207	3anbi2d 1469	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
209	208	ralbidv 3189	. . . . 5 ⊢ (𝑠 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
210	209	2rexbidv 3231	. . . 4 ⊢ (𝑠 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
211		oveq2 7438	. . . . . . . . . 10 ⊢ (𝑢 = 𝑄 → (1 − 𝑢) = (1 − 𝑄))
212	211	oveq1d 7445	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → ((1 − 𝑢) · (𝑥‘𝑖)) = ((1 − 𝑄) · (𝑥‘𝑖)))
213		oveq1 7437	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → (𝑢 · (𝑦‘𝑖)) = (𝑄 · (𝑦‘𝑖)))
214	212, 213	oveq12d 7448	. . . . . . . 8 ⊢ (𝑢 = 𝑄 → (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))
215	214	eqeq2d 2774	. . . . . . 7 ⊢ (𝑢 = 𝑄 → ((𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
216	215	3anbi3d 1470	. . . . . 6 ⊢ (𝑢 = 𝑄 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
217	216	ralbidv 3189	. . . . 5 ⊢ (𝑢 = 𝑄 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
218	217	2rexbidv 3231	. . . 4 ⊢ (𝑢 = 𝑄 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
219	202, 210, 218	rspc3ev 3596	. . 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 1400	. 2 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
221		rexcom 3295	. . . . . 6 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
222	221	rexbii 3113	. . . . 5 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
223		rexcom 3295	. . . . 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 3113	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
226		rexcom 3295	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
227		rexcom 3295	. . . . . . . 8 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
228	227	rexbii 3113	. . . . . . 7 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
229		rexcom 3295	. . . . . . 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 3113	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
232		rexcom 3295	. . . . 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 3113	. . 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 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2146   ≠ wne 2959  ∀wral 3080  ∃wrex 3090   ↦ cmpt 5189  ‘cfv 6547  (class class class)co 7430  ℂcc 11211  ℝcr 11212  0cc0 11213  1c1 11214   + caddc 11216   · cmul 11218   − cmin 11554   -cneg 11555   / cdiv 11986  ℕcn 12348  [,]cicc 13492  ...cfz 13652  𝔼cee 29480

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761  ax-cnex 11269  ax-resscn 11270  ax-1cn 11271  ax-icn 11272  ax-addcl 11273  ax-addrcl 11274  ax-mulcl 11275  ax-mulrcl 11276  ax-mulcom 11277  ax-addass 11278  ax-mulass 11279  ax-distr 11280  ax-i2m1 11281  ax-1ne0 11282  ax-1rid 11283  ax-rnegex 11284  ax-rrecex 11285  ax-cnre 11286  ax-pre-lttri 11287  ax-pre-lttrn 11288  ax-pre-ltadd 11289  ax-pre-mulgt0 11290

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8731  df-map 8863  df-en 8988  df-dom 8989  df-sdom 8990  df-pnf 11358  df-mnf 11359  df-xr 11360  df-ltxr 11361  df-le 11362  df-sub 11556  df-neg 11557  df-div 11987  df-icc 13496  df-ee 29483

This theorem is used by:  axeuclid  29556