Theorem axeuclidlem 28978

Description: Lemma for axeuclid 28979. 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 28917	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
4	3	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑘) ∈ ℝ))
5		fveere 28917	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
6	5	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑘) ∈ ℝ))
7	4, 6	anim12d 609	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ)))
8		fveere 28917	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
9	8	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑘) ∈ ℝ))
10		fveere 28917	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑇‘𝑘) ∈ ℝ)
11	10	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑘) ∈ ℝ))
12	9, 11	anim12d 609	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
13	7, 12	anim12d 609	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ))))
14	13	impcom 407	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
15		unitssre 13540	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
16	15	sseli 3978	. . . . . . . . . . . . . . 15 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℝ)
17	16	3ad2ant1 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) → 𝑃 ∈ ℝ)
18	17	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℝ)
19		peano2rem 11577	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
20	18, 19	syl 17	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℝ)
21		simplll 774	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑘) ∈ ℝ)
22	20, 21	remulcld 11292	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑘)) ∈ ℝ)
23		simpllr 775	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑘) ∈ ℝ)
24	22, 23	readdcld 11291	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) ∈ ℝ)
25		simpr3 1196	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
26	24, 18, 25	redivcld 12096	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
27	14, 26	sylan 580	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
28	27	an32s 652	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
29	28	ralrimiva 3145	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
30		eleenn 28912	. . . . . . . 8 ⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
31	30	ad3antrrr 730	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑁 ∈ ℕ)
32		mptelee 28911	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ))
33	31, 32	syl 17	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ))
34	29, 33	mpbird 257	. . . . 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 776	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑘) ∈ ℝ)
37	22, 36	readdcld 11291	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) ∈ ℝ)
38	37, 18, 25	redivcld 12096	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
39	14, 38	sylan 580	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
40	39	an32s 652	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
41	40	ralrimiva 3145	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
42		mptelee 28911	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ))
43	31, 42	syl 17	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ))
44	41, 43	mpbird 257	. . . . 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 28918	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
47	46	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑖) ∈ ℂ))
48		fveecn 28918	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
49	48	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑖) ∈ ℂ))
50	47, 49	anim12d 609	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ)))
51		fveecn 28918	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
52	51	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑖) ∈ ℂ))
53		fveecn 28918	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
54	53	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑖) ∈ ℂ))
55	52, 54	anim12d 609	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
56	50, 55	anim12d 609	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ))))
57	56	impcom 407	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
58		eqcom 2743	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖))
59		ax-1cn 11214	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
60		simpr2 1195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ (0[,]1))
61	15	sseli 3978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℝ)
62	61	recnd 11290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℂ)
63	60, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ ℂ)
64		subcl 11508	. . . . . . . . . . . . . . . . . . 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 11290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℂ)
68	66, 67	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℂ)
69		subcl 11508	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 − 1) ∈ ℂ)
70	68, 59, 69	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℂ)
71		simplll 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑖) ∈ ℂ)
72	70, 71	mulcld 11282	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) ∈ ℂ)
73	65, 72	mulcld 11282	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
74	63, 72	mulcld 11282	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
75	73, 74	addcld 11281	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) ∈ ℂ)
76		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) ∈ ℂ)
77	65, 76	mulcld 11282	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (𝐵‘𝑖)) ∈ ℂ)
78		simplrl 776	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) ∈ ℂ)
79	63, 78	mulcld 11282	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (𝐶‘𝑖)) ∈ ℂ)
80	77, 79	addcld 11281	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ∈ ℂ)
81	75, 80	addcld 11281	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) ∈ ℂ)
82		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑇‘𝑖) ∈ ℂ)
83		simpr3 1196	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
84	81, 68, 82, 83	divmuld 12066	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
85	58, 84	bitrid 283	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
86		negsubdi2 11569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → -(1 − 𝑃) = (𝑃 − 1))
87	59, 68, 86	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -(1 − 𝑃) = (𝑃 − 1))
88	87	oveq1d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = ((𝑃 − 1) · (𝐴‘𝑖)))
89		subcl 11508	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (1 − 𝑃) ∈ ℂ)
90	59, 68, 89	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑃) ∈ ℂ)
91	90, 71	mulneg1d 11717	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = -((1 − 𝑃) · (𝐴‘𝑖)))
92		npcan 11518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → ((1 − 𝑄) + 𝑄) = 1)
93	59, 63, 92	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) + 𝑄) = 1)
94	93	oveq1d 7447	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (1 · ((𝑃 − 1) · (𝐴‘𝑖))))
95	65, 63, 72	adddird 11287	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
96	72	mullidd 11280	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 · ((𝑃 − 1) · (𝐴‘𝑖))) = ((𝑃 − 1) · (𝐴‘𝑖)))
97	94, 95, 96	3eqtr3rd 2785	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
98	88, 91, 97	3eqtr3d 2784	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -((1 − 𝑃) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
99	98	oveq2d 7448	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))))
100	90, 71	mulcld 11282	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) · (𝐴‘𝑖)) ∈ ℂ)
101	80, 100	negsubd 11627	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))))
102	80, 75	addcomd 11464	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
103	99, 101, 102	3eqtr3d 2784	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
104	103	eqeq1d 2738	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖))))
105		eqcom 2743	. . . . . . . . . . . . . 14 ⊢ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖)) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
106	104, 105	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ (𝑃 · (𝑇‘𝑖)) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))))))
107	85, 106	bitr4d 282	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖))))
108	73, 74, 77, 79	add4d 11491	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
109	65, 72, 76	adddid 11286	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))))
110	63, 72, 78	adddid 11286	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) = ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖))))
111	109, 110	oveq12d 7450	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
112	108, 111	eqtr4d 2779	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))))
113	112	oveq1d 7447	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃))
114	72, 76	addcld 11281	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) ∈ ℂ)
115	65, 114	mulcld 11282	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) ∈ ℂ)
116	72, 78	addcld 11281	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) ∈ ℂ)
117	63, 116	mulcld 11282	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) ∈ ℂ)
118	115, 117, 68, 83	divdird 12082	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)))
119	65, 114, 68, 83	divassd 12079	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
120	63, 116, 68, 83	divassd 12079	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
121	119, 120	oveq12d 7450	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
122	113, 118, 121	3eqtrd 2780	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
123	122	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
124	68, 82	mulcld 11282	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · (𝑇‘𝑖)) ∈ ℂ)
125	80, 100, 124	subaddd 11639	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
126	107, 123, 125	3bitr3rd 310	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
127	126	biimpd 229	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
128		npncan2 11537	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
129	59, 68, 128	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
130	129	oveq1d 7447	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (0 · (𝐴‘𝑖)))
131	90, 70, 71	adddird 11287	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))))
132		mul02 11440	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑖) ∈ ℂ → (0 · (𝐴‘𝑖)) = 0)
133	132	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 · (𝐴‘𝑖)) = 0)
134	130, 131, 133	3eqtr3d 2784	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) = 0)
135	134	oveq1d 7447	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (0 + (𝐵‘𝑖)))
136	100, 72, 76	addassd 11284	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
137	76	addlidd 11463	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐵‘𝑖)) = (𝐵‘𝑖))
138	135, 136, 137	3eqtr3rd 2785	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
139	114, 68, 83	divcan2d 12046	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
140	139	oveq2d 7448	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
141	138, 140	eqtr4d 2779	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
142	134	oveq1d 7447	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (0 + (𝐶‘𝑖)))
143	100, 72, 78	addassd 11284	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
144	78	addlidd 11463	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐶‘𝑖)) = (𝐶‘𝑖))
145	142, 143, 144	3eqtr3rd 2785	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
146	116, 68, 83	divcan2d 12046	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
147	146	oveq2d 7448	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
148	145, 147	eqtr4d 2779	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
149	141, 148	jca 511	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
150	127, 149	jctild 525	. . . . . . . . 9 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
151		df-3an 1088	. . . . . . . . 9 ⊢ (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ↔ (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
152	150, 151	imbitrrdi 252	. . . . . . . 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 652	. . . . . 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 6904	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖))
158		fveq2 6905	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
159	158	oveq2d 7448	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝑃 − 1) · (𝐴‘𝑘)) = ((𝑃 − 1) · (𝐴‘𝑖)))
160		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
161	159, 160	oveq12d 7450	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
162	161	oveq1d 7447	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
163		eqid 2736	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))
164		ovex 7465	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) ∈ V
165	162, 163, 164	fvmpt 7015	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
166	157, 165	sylan9eq 2796	. . . . . . 7 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
167		oveq2 7440	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (𝑃 · (𝑥‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
168	167	oveq2d 7448	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
169	168	eqeq2d 2747	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))))
170		oveq2 7440	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((1 − 𝑄) · (𝑥‘𝑖)) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
171	170	oveq1d 7447	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))
172	171	eqeq2d 2747	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))))
173	169, 172	3anbi13d 1439	. . . . . . 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 3175	. . . . 5 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
176		fveq1 6904	. . . . . . . 8 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (𝑦‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖))
177		fveq2 6905	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
178	159, 177	oveq12d 7450	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
179	178	oveq1d 7447	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
180		eqid 2736	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))
181		ovex 7465	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) ∈ V
182	179, 180, 181	fvmpt 7015	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
183	176, 182	sylan9eq 2796	. . . . . . 7 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
184		oveq2 7440	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑃 · (𝑦‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
185	184	oveq2d 7448	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
186	185	eqeq2d 2747	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
187		oveq2 7440	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑄 · (𝑦‘𝑖)) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
188	187	oveq2d 7448	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
189	188	eqeq2d 2747	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
190	186, 189	3anbi23d 1440	. . . . . . 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 3175	. . . . 5 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
193	175, 192	rspc2ev 3634	. . . 4 ⊢ (((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
194	35, 45, 156, 193	syl3anc 1372	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
195		oveq2 7440	. . . . . . . . . 10 ⊢ (𝑟 = 𝑃 → (1 − 𝑟) = (1 − 𝑃))
196	195	oveq1d 7447	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → ((1 − 𝑟) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
197		oveq1 7439	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → (𝑟 · (𝑥‘𝑖)) = (𝑃 · (𝑥‘𝑖)))
198	196, 197	oveq12d 7450	. . . . . . . 8 ⊢ (𝑟 = 𝑃 → (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))))
199	198	eqeq2d 2747	. . . . . . 7 ⊢ (𝑟 = 𝑃 → ((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖)))))
200	199	3anbi1d 1441	. . . . . 6 ⊢ (𝑟 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
201	200	ralbidv 3177	. . . . 5 ⊢ (𝑟 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
202	201	2rexbidv 3221	. . . 4 ⊢ (𝑟 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
203		oveq2 7440	. . . . . . . . . 10 ⊢ (𝑠 = 𝑃 → (1 − 𝑠) = (1 − 𝑃))
204	203	oveq1d 7447	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → ((1 − 𝑠) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
205		oveq1 7439	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 · (𝑦‘𝑖)) = (𝑃 · (𝑦‘𝑖)))
206	204, 205	oveq12d 7450	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))))
207	206	eqeq2d 2747	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖)))))
208	207	3anbi2d 1442	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
209	208	ralbidv 3177	. . . . 5 ⊢ (𝑠 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
210	209	2rexbidv 3221	. . . 4 ⊢ (𝑠 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
211		oveq2 7440	. . . . . . . . . 10 ⊢ (𝑢 = 𝑄 → (1 − 𝑢) = (1 − 𝑄))
212	211	oveq1d 7447	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → ((1 − 𝑢) · (𝑥‘𝑖)) = ((1 − 𝑄) · (𝑥‘𝑖)))
213		oveq1 7439	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → (𝑢 · (𝑦‘𝑖)) = (𝑄 · (𝑦‘𝑖)))
214	212, 213	oveq12d 7450	. . . . . . . 8 ⊢ (𝑢 = 𝑄 → (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))
215	214	eqeq2d 2747	. . . . . . 7 ⊢ (𝑢 = 𝑄 → ((𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
216	215	3anbi3d 1443	. . . . . 6 ⊢ (𝑢 = 𝑄 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
217	216	ralbidv 3177	. . . . 5 ⊢ (𝑢 = 𝑄 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
218	217	2rexbidv 3221	. . . 4 ⊢ (𝑢 = 𝑄 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
219	202, 210, 218	rspc3ev 3638	. . 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 1374	. 2 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
221		rexcom 3289	. . . . . 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 3289	. . . . 5 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
224	222, 223	bitri 275	. . . 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 3289	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
227		rexcom 3289	. . . . . . . 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 3289	. . . . . . 7 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
230	228, 229	bitri 275	. . . . . 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 3289	. . . . 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 275	. . . 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 297	. 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 218	1 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2939  ∀wral 3060  ∃wrex 3069   ↦ cmpt 5224  ‘cfv 6560  (class class class)co 7432  ℂcc 11154  ℝcr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161   − cmin 11493  -cneg 11494   / cdiv 11921  ℕcn 12267  [,]cicc 13391  ...cfz 13548  𝔼cee 28904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-mpt 5225  df-id 5577  df-po 5591  df-so 5592  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-er 8746  df-map 8869  df-en 8987  df-dom 8988  df-sdom 8989  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-icc 13395  df-ee 28907

This theorem is referenced by:  axeuclid  28979