Theorem axeuclidlem 28995

Description: Lemma for axeuclid 28996. 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 28934	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
4	3	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑘) ∈ ℝ))
5		fveere 28934	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
6	5	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑘) ∈ ℝ))
7	4, 6	anim12d 608	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ)))
8		fveere 28934	. . . . . . . . . . . . 13 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
9	8	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑘) ∈ ℝ))
10		fveere 28934	. . . . . . . . . . . . 13 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝑇‘𝑘) ∈ ℝ)
11	10	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑘) ∈ ℝ))
12	9, 11	anim12d 608	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
13	7, 12	anim12d 608	. . . . . . . . . 10 ⊢ (𝑘 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ))))
14	13	impcom 407	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) → (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)))
15		unitssre 13559	. . . . . . . . . . . . . . . 16 ⊢ (0[,]1) ⊆ ℝ
16	15	sseli 4004	. . . . . . . . . . . . . . 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 11603	. . . . . . . . . . . . 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 11320	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑘)) ∈ ℝ)
23		simpllr 775	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑘) ∈ ℝ)
24	22, 23	readdcld 11319	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) ∈ ℝ)
25		simpr3 1196	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ≠ 0)
26	24, 18, 25	redivcld 12122	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
27	14, 26	sylan 579	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
28	27	an32s 651	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
29	28	ralrimiva 3152	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) ∈ ℝ)
30		eleenn 28929	. . . . . . . 8 ⊢ (𝐴 ∈ (𝔼‘𝑁) → 𝑁 ∈ ℕ)
31	30	ad3antrrr 729	. . . . . . 7 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑁 ∈ ℕ)
32		mptelee 28928	. . . . . . 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 11319	. . . . . . . . . 10 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) ∈ ℝ)
38	37, 18, 25	redivcld 12122	. . . . . . . . 9 ⊢ (((((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) ∧ ((𝐶‘𝑘) ∈ ℝ ∧ (𝑇‘𝑘) ∈ ℝ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
39	14, 38	sylan 579	. . . . . . . 8 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑘 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
40	39	an32s 651	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑘 ∈ (1...𝑁)) → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
41	40	ralrimiva 3152	. . . . . 6 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ∀𝑘 ∈ (1...𝑁)((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) ∈ ℝ)
42		mptelee 28928	. . . . . . 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 28935	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
47	46	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐴 ∈ (𝔼‘𝑁) → (𝐴‘𝑖) ∈ ℂ))
48		fveecn 28935	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
49	48	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐵 ∈ (𝔼‘𝑁) → (𝐵‘𝑖) ∈ ℂ))
50	47, 49	anim12d 608	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → ((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ)))
51		fveecn 28935	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
52	51	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝐶 ∈ (𝔼‘𝑁) → (𝐶‘𝑖) ∈ ℂ))
53		fveecn 28935	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑇‘𝑖) ∈ ℂ)
54	53	expcom 413	. . . . . . . . . . 11 ⊢ (𝑖 ∈ (1...𝑁) → (𝑇 ∈ (𝔼‘𝑁) → (𝑇‘𝑖) ∈ ℂ))
55	52, 54	anim12d 608	. . . . . . . . . 10 ⊢ (𝑖 ∈ (1...𝑁) → ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁)) → ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
56	50, 55	anim12d 608	. . . . . . . . 9 ⊢ (𝑖 ∈ (1...𝑁) → (((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ))))
57	56	impcom 407	. . . . . . . 8 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)))
58		eqcom 2747	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (𝑇‘𝑖))
59		ax-1cn 11242	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℂ
60		simpr2 1195	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ (0[,]1))
61	15	sseli 4004	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℝ)
62	61	recnd 11318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑄 ∈ (0[,]1) → 𝑄 ∈ ℂ)
63	60, 62	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑄 ∈ ℂ)
64		subcl 11535	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → (1 − 𝑄) ∈ ℂ)
65	59, 63, 64	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑄) ∈ ℂ)
66		simpr1 1194	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ (0[,]1))
67	16	recnd 11318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (0[,]1) → 𝑃 ∈ ℂ)
68	66, 67	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → 𝑃 ∈ ℂ)
69		subcl 11535	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑃 − 1) ∈ ℂ)
70	68, 59, 69	sylancl 585	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 − 1) ∈ ℂ)
71		simplll 774	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐴‘𝑖) ∈ ℂ)
72	70, 71	mulcld 11310	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) ∈ ℂ)
73	65, 72	mulcld 11310	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
74	63, 72	mulcld 11310	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) ∈ ℂ)
75	73, 74	addcld 11309	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) ∈ ℂ)
76		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) ∈ ℂ)
77	65, 76	mulcld 11310	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (𝐵‘𝑖)) ∈ ℂ)
78		simplrl 776	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) ∈ ℂ)
79	63, 78	mulcld 11310	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (𝐶‘𝑖)) ∈ ℂ)
80	77, 79	addcld 11309	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) ∈ ℂ)
81	75, 80	addcld 11309	. . . . . . . . . . . . . . 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 12092	. . . . . . . . . . . . . 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 11595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → -(1 − 𝑃) = (𝑃 − 1))
87	59, 68, 86	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -(1 − 𝑃) = (𝑃 − 1))
88	87	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = ((𝑃 − 1) · (𝐴‘𝑖)))
89		subcl 11535	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → (1 − 𝑃) ∈ ℂ)
90	59, 68, 89	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 − 𝑃) ∈ ℂ)
91	90, 71	mulneg1d 11743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (-(1 − 𝑃) · (𝐴‘𝑖)) = -((1 − 𝑃) · (𝐴‘𝑖)))
92		npcan 11545	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑄 ∈ ℂ) → ((1 − 𝑄) + 𝑄) = 1)
93	59, 63, 92	sylancr 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) + 𝑄) = 1)
94	93	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (1 · ((𝑃 − 1) · (𝐴‘𝑖))))
95	65, 63, 72	adddird 11315	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) + 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
96	72	mullidd 11308	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (1 · ((𝑃 − 1) · (𝐴‘𝑖))) = ((𝑃 − 1) · (𝐴‘𝑖)))
97	94, 95, 96	3eqtr3rd 2789	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑃 − 1) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
98	88, 91, 97	3eqtr3d 2788	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → -((1 − 𝑃) · (𝐴‘𝑖)) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))))
99	98	oveq2d 7464	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))))
100	90, 71	mulcld 11310	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) · (𝐴‘𝑖)) ∈ ℂ)
101	80, 100	negsubd 11653	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + -((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))))
102	80, 75	addcomd 11492	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) + (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
103	99, 101, 102	3eqtr3d 2788	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))))
104	103	eqeq1d 2742	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) − ((1 − 𝑃) · (𝐴‘𝑖))) = (𝑃 · (𝑇‘𝑖)) ↔ ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (𝑃 · (𝑇‘𝑖))))
105		eqcom 2747	. . . . . . . . . . . . . 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 11518	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
109	65, 72, 76	adddid 11314	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) = (((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))))
110	63, 72, 78	adddid 11314	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) = ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖))))
111	109, 110	oveq12d 7466	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) = ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + ((1 − 𝑄) · (𝐵‘𝑖))) + ((𝑄 · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · (𝐶‘𝑖)))))
112	108, 111	eqtr4d 2783	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) = (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))))
113	112	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃))
114	72, 76	addcld 11309	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) ∈ ℂ)
115	65, 114	mulcld 11310	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) ∈ ℂ)
116	72, 78	addcld 11309	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) ∈ ℂ)
117	63, 116	mulcld 11310	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) ∈ ℂ)
118	115, 117, 68, 83	divdird 12108	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) + (𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))) / 𝑃) = ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)))
119	65, 114, 68, 83	divassd 12105	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
120	63, 116, 68, 83	divassd 12105	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
121	119, 120	oveq12d 7466	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑄) · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))) / 𝑃) + ((𝑄 · (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))) / 𝑃)) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
122	113, 118, 121	3eqtrd 2784	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
123	122	eqeq2d 2751	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((𝑇‘𝑖) = (((((1 − 𝑄) · ((𝑃 − 1) · (𝐴‘𝑖))) + (𝑄 · ((𝑃 − 1) · (𝐴‘𝑖)))) + (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) / 𝑃) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
124	68, 82	mulcld 11310	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · (𝑇‘𝑖)) ∈ ℂ)
125	80, 100, 124	subaddd 11665	. . . . . . . . . . . 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 11563	. . . . . . . . . . . . . . . . 17 ⊢ ((1 ∈ ℂ ∧ 𝑃 ∈ ℂ) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
129	59, 68, 128	sylancr 586	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((1 − 𝑃) + (𝑃 − 1)) = 0)
130	129	oveq1d 7463	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (0 · (𝐴‘𝑖)))
131	90, 70, 71	adddird 11315	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) + (𝑃 − 1)) · (𝐴‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))))
132		mul02 11468	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝑖) ∈ ℂ → (0 · (𝐴‘𝑖)) = 0)
133	132	ad3antrrr 729	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 · (𝐴‘𝑖)) = 0)
134	130, 131, 133	3eqtr3d 2788	. . . . . . . . . . . . . 14 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) = 0)
135	134	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (0 + (𝐵‘𝑖)))
136	100, 72, 76	addassd 11312	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐵‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
137	76	addlidd 11491	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐵‘𝑖)) = (𝐵‘𝑖))
138	135, 136, 137	3eqtr3rd 2789	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
139	114, 68, 83	divcan2d 12072	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
140	139	oveq2d 7464	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖))))
141	138, 140	eqtr4d 2783	. . . . . . . . . . 11 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
142	134	oveq1d 7463	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (0 + (𝐶‘𝑖)))
143	100, 72, 78	addassd 11312	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + ((𝑃 − 1) · (𝐴‘𝑖))) + (𝐶‘𝑖)) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
144	78	addlidd 11491	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (0 + (𝐶‘𝑖)) = (𝐶‘𝑖))
145	142, 143, 144	3eqtr3rd 2789	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
146	116, 68, 83	divcan2d 12072	. . . . . . . . . . . . 13 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
147	146	oveq2d 7464	. . . . . . . . . . . 12 ⊢ (((((𝐴‘𝑖) ∈ ℂ ∧ (𝐵‘𝑖) ∈ ℂ) ∧ ((𝐶‘𝑖) ∈ ℂ ∧ (𝑇‘𝑖) ∈ ℂ)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖))))
148	145, 147	eqtr4d 2783	. . . . . . . . . . 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 1089	. . . . . . . . 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 579	. . . . . . 7 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ 𝑖 ∈ (1...𝑁)) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
154	153	an32s 651	. . . . . 6 ⊢ (((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0)) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖))) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
155	154	ralimdva 3173	. . . . 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 6919	. . . . . . . 8 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖))
158		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
159	158	oveq2d 7464	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → ((𝑃 − 1) · (𝐴‘𝑘)) = ((𝑃 − 1) · (𝐴‘𝑖)))
160		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
161	159, 160	oveq12d 7466	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)))
162	161	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
163		eqid 2740	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))
164		ovex 7481	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) ∈ V
165	162, 163, 164	fvmpt 7029	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
166	157, 165	sylan9eq 2800	. . . . . . 7 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))
167		oveq2 7456	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (𝑃 · (𝑥‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
168	167	oveq2d 7464	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))))
169	168	eqeq2d 2751	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))))
170		oveq2 7456	. . . . . . . . . 10 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((1 − 𝑄) · (𝑥‘𝑖)) = ((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)))
171	170	oveq1d 7463	. . . . . . . . 9 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))
172	171	eqeq2d 2751	. . . . . . . 8 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))))
173	169, 172	3anbi13d 1438	. . . . . . 7 ⊢ ((𝑥‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
174	166, 173	syl 17	. . . . . 6 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
175	174	ralbidva 3182	. . . . 5 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))))))
176		fveq1 6919	. . . . . . . 8 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (𝑦‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖))
177		fveq2 6920	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
178	159, 177	oveq12d 7466	. . . . . . . . . 10 ⊢ (𝑘 = 𝑖 → (((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) = (((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)))
179	178	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑘 = 𝑖 → ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
180		eqid 2740	. . . . . . . . 9 ⊢ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))
181		ovex 7481	. . . . . . . . 9 ⊢ ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) ∈ V
182	179, 180, 181	fvmpt 7029	. . . . . . . 8 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃))‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
183	176, 182	sylan9eq 2800	. . . . . . 7 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))
184		oveq2 7456	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑃 · (𝑦‘𝑖)) = (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
185	184	oveq2d 7464	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
186	185	eqeq2d 2751	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
187		oveq2 7456	. . . . . . . . . 10 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (𝑄 · (𝑦‘𝑖)) = (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))
188	187	oveq2d 7464	. . . . . . . . 9 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))
189	188	eqeq2d 2751	. . . . . . . 8 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → ((𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃)))))
190	186, 189	3anbi23d 1439	. . . . . . 7 ⊢ ((𝑦‘𝑖) = ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
191	183, 190	syl 17	. . . . . 6 ⊢ ((𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∧ 𝑖 ∈ (1...𝑁)) → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
192	191	ralbidva 3182	. . . . 5 ⊢ (𝑦 = (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))))
193	175, 192	rspc2ev 3648	. . . 4 ⊢ (((𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐵‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ (𝑘 ∈ (1...𝑁) ↦ ((((𝑃 − 1) · (𝐴‘𝑘)) + (𝐶‘𝑘)) / 𝑃)) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐵‘𝑖)) / 𝑃)) + (𝑄 · ((((𝑃 − 1) · (𝐴‘𝑖)) + (𝐶‘𝑖)) / 𝑃))))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
194	35, 45, 156, 193	syl3anc 1371	. . 3 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
195		oveq2 7456	. . . . . . . . . 10 ⊢ (𝑟 = 𝑃 → (1 − 𝑟) = (1 − 𝑃))
196	195	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → ((1 − 𝑟) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
197		oveq1 7455	. . . . . . . . 9 ⊢ (𝑟 = 𝑃 → (𝑟 · (𝑥‘𝑖)) = (𝑃 · (𝑥‘𝑖)))
198	196, 197	oveq12d 7466	. . . . . . . 8 ⊢ (𝑟 = 𝑃 → (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))))
199	198	eqeq2d 2751	. . . . . . 7 ⊢ (𝑟 = 𝑃 → ((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ↔ (𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖)))))
200	199	3anbi1d 1440	. . . . . 6 ⊢ (𝑟 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
201	200	ralbidv 3184	. . . . 5 ⊢ (𝑟 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
202	201	2rexbidv 3228	. . . 4 ⊢ (𝑟 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
203		oveq2 7456	. . . . . . . . . 10 ⊢ (𝑠 = 𝑃 → (1 − 𝑠) = (1 − 𝑃))
204	203	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → ((1 − 𝑠) · (𝐴‘𝑖)) = ((1 − 𝑃) · (𝐴‘𝑖)))
205		oveq1 7455	. . . . . . . . 9 ⊢ (𝑠 = 𝑃 → (𝑠 · (𝑦‘𝑖)) = (𝑃 · (𝑦‘𝑖)))
206	204, 205	oveq12d 7466	. . . . . . . 8 ⊢ (𝑠 = 𝑃 → (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))))
207	206	eqeq2d 2751	. . . . . . 7 ⊢ (𝑠 = 𝑃 → ((𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ↔ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖)))))
208	207	3anbi2d 1441	. . . . . 6 ⊢ (𝑠 = 𝑃 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
209	208	ralbidv 3184	. . . . 5 ⊢ (𝑠 = 𝑃 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
210	209	2rexbidv 3228	. . . 4 ⊢ (𝑠 = 𝑃 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))))))
211		oveq2 7456	. . . . . . . . . 10 ⊢ (𝑢 = 𝑄 → (1 − 𝑢) = (1 − 𝑄))
212	211	oveq1d 7463	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → ((1 − 𝑢) · (𝑥‘𝑖)) = ((1 − 𝑄) · (𝑥‘𝑖)))
213		oveq1 7455	. . . . . . . . 9 ⊢ (𝑢 = 𝑄 → (𝑢 · (𝑦‘𝑖)) = (𝑄 · (𝑦‘𝑖)))
214	212, 213	oveq12d 7466	. . . . . . . 8 ⊢ (𝑢 = 𝑄 → (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))
215	214	eqeq2d 2751	. . . . . . 7 ⊢ (𝑢 = 𝑄 → ((𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖))) ↔ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖)))))
216	215	3anbi3d 1442	. . . . . 6 ⊢ (𝑢 = 𝑄 → (((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
217	216	ralbidv 3184	. . . . 5 ⊢ (𝑢 = 𝑄 → (∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
218	217	2rexbidv 3228	. . . 4 ⊢ (𝑢 = 𝑄 → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))))
219	202, 210, 218	rspc3ev 3652	. . 3 ⊢ (((𝑃 ∈ (0[,]1) ∧ 𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1)) ∧ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑄) · (𝑥‘𝑖)) + (𝑄 · (𝑦‘𝑖))))) → ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
220	1, 1, 2, 194, 219	syl31anc 1373	. 2 ⊢ ((((𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝑇 ∈ (𝔼‘𝑁))) ∧ (𝑃 ∈ (0[,]1) ∧ 𝑄 ∈ (0[,]1) ∧ 𝑃 ≠ 0) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑃) · (𝐴‘𝑖)) + (𝑃 · (𝑇‘𝑖))) = (((1 − 𝑄) · (𝐵‘𝑖)) + (𝑄 · (𝐶‘𝑖)))) → ∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
221		rexcom 3296	. . . . . 6 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
222	221	rexbii 3100	. . . . 5 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
223		rexcom 3296	. . . . 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 3100	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
226		rexcom 3296	. . 3 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
227		rexcom 3296	. . . . . . . 8 ⊢ (∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
228	227	rexbii 3100	. . . . . . 7 ⊢ (∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑠 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
229		rexcom 3296	. . . . . . 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 3100	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑦 ∈ (𝔼‘𝑁)∃𝑠 ∈ (0[,]1)∃𝑢 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐵‘𝑖) = (((1 − 𝑟) · (𝐴‘𝑖)) + (𝑟 · (𝑥‘𝑖))) ∧ (𝐶‘𝑖) = (((1 − 𝑠) · (𝐴‘𝑖)) + (𝑠 · (𝑦‘𝑖))) ∧ (𝑇‘𝑖) = (((1 − 𝑢) · (𝑥‘𝑖)) + (𝑢 · (𝑦‘𝑖)))))
232		rexcom 3296	. . . . 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 3100	. . 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 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076   ↦ cmpt 5249  ‘cfv 6573  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189   − cmin 11520  -cneg 11521   / cdiv 11947  ℕcn 12293  [,]cicc 13410  ...cfz 13567  𝔼cee 28921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-po 5607  df-so 5608  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-er 8763  df-map 8886  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-icc 13414  df-ee 28924

This theorem is referenced by:  axeuclid  28996