Theorem axpasch 29014

Description: The inner Pasch axiom. Take a triangle 𝐴𝐶𝐸, a point 𝐷 on 𝐴𝐶, and a point 𝐵 extending 𝐶𝐸. Then 𝐴𝐸 and 𝐷𝐵 intersect at some point 𝑥. Axiom A7 of [Schwabhauser] p. 12. (Contributed by Scott Fenton, 3-Jun-2013.)

Assertion

Ref	Expression
axpasch	⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝑁   𝑥,𝐵   𝑥,𝐸   𝑥,𝐶   𝑥,𝐷

Proof of Theorem axpasch

Dummy variables 𝑖 𝑘 𝑞 𝑟 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axpaschlem 29013	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)))
2	1	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)))
3		simp1 1136	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑞 = ((1 − 𝑟) · (1 − 𝑡)))
4	3	oveq1d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑞 · (𝐴‘𝑖)) = (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)))
5	4	eqcomd 2742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = (𝑞 · (𝐴‘𝑖)))
6		simp2 1137	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑟 = ((1 − 𝑞) · (1 − 𝑠)))
7	6	oveq1d 7373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑟 · (𝐵‘𝑖)) = (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)))
8	5, 7	oveq12d 7376	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) = ((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))))
9		simp3 1138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))
10	9	oveq1d 7373	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)))
11	8, 10	oveq12d 7376	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) = (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))))
12	11	3ad2ant3 1135	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) = (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))))
13	12	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) = (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))))
14		1re 11132	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
15		simpl2l 1227	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ (0[,]1))
16		elicc01 13382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ (0[,]1) ↔ (𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ∧ 𝑟 ≤ 1))
17	16	simp1bi 1145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈ ℝ)
18	15, 17	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ ℝ)
19		resubcl 11445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (1 − 𝑟) ∈ ℝ)
20	14, 18, 19	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
21	20	recnd 11160	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℂ)
22		simp13l 1289	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝑡 ∈ (0[,]1))
23	22	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
24		elicc01 13382	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
25	24	simp1bi 1145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
26	23, 25	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
27		resubcl 11445	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
28	14, 26, 27	sylancr 587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
29		simp121 1306	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐴 ∈ (𝔼‘𝑁))
30		fveere 28974	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
31	29, 30	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
32	28, 31	remulcld 11162	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑖)) ∈ ℝ)
33	32	recnd 11160	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑖)) ∈ ℂ)
34		simp123 1308	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐶 ∈ (𝔼‘𝑁))
35		fveere 28974	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
36	34, 35	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
37	26, 36	remulcld 11162	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℝ)
38	37	recnd 11160	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℂ)
39	21, 33, 38	adddid 11156	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖)))))
40	28	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
41	31	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
42	21, 40, 41	mulassd 11155	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = ((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))))
43	26	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
44		fveecn 28975	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
45	34, 44	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
46	21, 43, 45	mulassd 11155	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖))))
47	42, 46	oveq12d 7376	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖)))))
48	39, 47	eqtr4d 2774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
49	48	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) + (𝑟 · (𝐵‘𝑖))))
50	20, 28	remulcld 11162	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (1 − 𝑡)) ∈ ℝ)
51	50, 31	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℝ)
52	51	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℂ)
53	20, 26	remulcld 11162	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · 𝑡) ∈ ℝ)
54	53, 36	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) ∈ ℝ)
55	54	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) ∈ ℂ)
56		simp122 1307	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐵 ∈ (𝔼‘𝑁))
57		fveere 28974	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
58	56, 57	sylan 580	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
59	18, 58	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℝ)
60	59	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℂ)
61	52, 55, 60	add32d 11361	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) + (𝑟 · (𝐵‘𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
62	49, 61	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
63		simpl2r 1228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ (0[,]1))
64		elicc01 13382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ (0[,]1) ↔ (𝑞 ∈ ℝ ∧ 0 ≤ 𝑞 ∧ 𝑞 ≤ 1))
65	64	simp1bi 1145	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ (0[,]1) → 𝑞 ∈ ℝ)
66	63, 65	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ ℝ)
67		resubcl 11445	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 𝑞 ∈ ℝ) → (1 − 𝑞) ∈ ℝ)
68	14, 66, 67	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℝ)
69		simp13r 1290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝑠 ∈ (0[,]1))
70	69	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
71		elicc01 13382	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1))
72	71	simp1bi 1145	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
73	70, 72	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
74		resubcl 11445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (1 − 𝑠) ∈ ℝ)
75	14, 73, 74	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℝ)
76	75, 58	remulcld 11162	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℝ)
77	68, 76	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℝ)
78	77	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℂ)
79	73, 36	remulcld 11162	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℝ)
80	68, 79	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℝ)
81	80	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℂ)
82	66, 31	remulcld 11162	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℝ)
83	82	recnd 11160	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℂ)
84	78, 81, 83	add32d 11361	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + (𝑞 · (𝐴‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))))
85	68	recnd 11160	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℂ)
86	76	recnd 11160	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℂ)
87	79	recnd 11160	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℂ)
88	85, 86, 87	adddid 11156	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))))
89	88	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
90	75	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℂ)
91	58	recnd 11160	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
92	85, 90, 91	mulassd 11155	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)) = ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))))
93	92	oveq2d 7374	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) = ((𝑞 · (𝐴‘𝑖)) + ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖)))))
94	83, 78, 93	comraddd 11347	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + (𝑞 · (𝐴‘𝑖))))
95	73	recnd 11160	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
96	85, 95, 45	mulassd 11155	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)) = ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))))
97	94, 96	oveq12d 7376	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + (𝑞 · (𝐴‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))))
98	84, 89, 97	3eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) = (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))))
99	13, 62, 98	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
100	99	ralrimiva 3128	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
101	100	3expia 1121	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
102	101	reximdvva 3184	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
103	2, 102	mpd 15	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
104		simplrl 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑟 ∈ (0[,]1))
105	104, 17	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑟 ∈ ℝ)
106	14, 105, 19	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
107		simpl3l 1229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝑡 ∈ (0[,]1))
108	107	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
109	108, 25	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
110	14, 109, 27	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
111		simpl21 1252	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐴 ∈ (𝔼‘𝑁))
112		fveere 28974	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
113	111, 112	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
114	110, 113	remulcld 11162	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑘)) ∈ ℝ)
115		simpl23 1254	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐶 ∈ (𝔼‘𝑁))
116		fveere 28974	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
117	115, 116	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
118	109, 117	remulcld 11162	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑘)) ∈ ℝ)
119	114, 118	readdcld 11161	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) ∈ ℝ)
120	106, 119	remulcld 11162	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) ∈ ℝ)
121		simpl22 1253	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐵 ∈ (𝔼‘𝑁))
122		fveere 28974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
123	121, 122	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
124	105, 123	remulcld 11162	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑘)) ∈ ℝ)
125	120, 124	readdcld 11161	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
126	125	ralrimiva 3128	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
127	126	anassrs 467	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
128		simpll1 1213	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
129		mptelee 28967	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ))
130	128, 129	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ))
131	127, 130	mpbird 257	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁))
132		fveq1 6833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖))
133		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
134	133	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝐴‘𝑘)) = ((1 − 𝑡) · (𝐴‘𝑖)))
135		fveq2 6834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
136	135	oveq2d 7374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝐶‘𝑘)) = (𝑡 · (𝐶‘𝑖)))
137	134, 136	oveq12d 7376	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))))
138	137	oveq2d 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
139		fveq2 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
140	139	oveq2d 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑟 · (𝐵‘𝑘)) = (𝑟 · (𝐵‘𝑖)))
141	138, 140	oveq12d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
142		eqid 2736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))
143		ovex 7391	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∈ V
144	141, 142, 143	fvmpt 6941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
145	132, 144	sylan9eq 2791	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
146	145	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
147	145	eqeq1d 2738	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
148	146, 147	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
149		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))
150	149	biantrur 530	. . . . . . . . . . . . . . 15 ⊢ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
151	148, 150	bitr4di 289	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
152	151	ralbidva 3157	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
153	152	rspcev 3576	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
154	153	ex 412	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
155	131, 154	syl 17	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
156	155	reximdva 3149	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
157	156	reximdva 3149	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
158	103, 157	mpd 15	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
159		rexcom 3265	. . . . . . . . 9 ⊢ (∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
160	159	rexbii 3083	. . . . . . . 8 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
161		rexcom 3265	. . . . . . . 8 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
162	160, 161	bitri 275	. . . . . . 7 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
163	158, 162	sylib 218	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
164		oveq2 7366	. . . . . . . . . . . . 13 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((1 − 𝑟) · (𝐷‘𝑖)) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
165	164	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
166	165	eqeq2d 2747	. . . . . . . . . . 11 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
167		oveq2 7366	. . . . . . . . . . . . 13 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((1 − 𝑞) · (𝐸‘𝑖)) = ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
168	167	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
169	168	eqeq2d 2747	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
170	166, 169	bi2anan9 638	. . . . . . . . . 10 ⊢ (((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
171	170	ralimi 3073	. . . . . . . . 9 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
172		ralbi 3091	. . . . . . . . 9 ⊢ (∀𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
173	171, 172	syl 17	. . . . . . . 8 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
174	173	rexbidv 3160	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
175	174	2rexbidv 3201	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
176	163, 175	syl5ibrcom 247	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
177	176	3expia 1121	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))))
178	177	rexlimdvv 3192	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
179	178	3adant3 1132	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
180		simp3l 1202	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
181		simp21 1207	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
182		simp23 1209	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
183		brbtwn 28972	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
184	180, 181, 182, 183	syl3anc 1373	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
185		simp3r 1203	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
186		simp22 1208	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
187		brbtwn 28972	. . . . 5 ⊢ ((𝐸 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
188	185, 186, 182, 187	syl3anc 1373	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
189	184, 188	anbi12d 632	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))))))
190		r19.26 3096	. . . . 5 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
191	190	2rexbii 3112	. . . 4 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
192		reeanv 3208	. . . 4 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
193	191, 192	bitri 275	. . 3 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
194	189, 193	bitr4di 289	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))))))
195		simpr 484	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
196		simpl3l 1229	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
197		simpl22 1253	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
198		brbtwn 28972	. . . . . 6 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖)))))
199	195, 196, 197, 198	syl3anc 1373	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖)))))
200		simpl3r 1230	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
201		simpl21 1252	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
202		brbtwn 28972	. . . . . 6 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
203	195, 200, 201, 202	syl3anc 1373	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
204	199, 203	anbi12d 632	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
205		r19.26 3096	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
206	205	2rexbii 3112	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
207		reeanv 3208	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
208	206, 207	bitri 275	. . . 4 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
209	204, 208	bitr4di 289	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
210	209	rexbidva 3158	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
211	179, 194, 210	3imtr4d 294	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060  ⟨cop 4586   class class class wbr 5098   ↦ cmpt 5179  ‘cfv 6492  (class class class)co 7358  ℂcc 11024  ℝcr 11025  0cc0 11026  1c1 11027   + caddc 11029   · cmul 11031   ≤ cle 11167   − cmin 11364  ℕcn 12145  [,]cicc 13264  ...cfz 13423  𝔼cee 28960   Btwn cbtwn 28961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-mulcom 11090  ax-addass 11091  ax-mulass 11092  ax-distr 11093  ax-i2m1 11094  ax-1ne0 11095  ax-1rid 11096  ax-rnegex 11097  ax-rrecex 11098  ax-cnre 11099  ax-pre-lttri 11100  ax-pre-lttrn 11101  ax-pre-ltadd 11102  ax-pre-mulgt0 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7809  df-1st 7933  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-er 8635  df-map 8765  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172  df-sub 11366  df-neg 11367  df-div 11795  df-nn 12146  df-z 12489  df-uz 12752  df-icc 13268  df-fz 13424  df-ee 28963  df-btwn 28964

This theorem is referenced by:  eengtrkg  29059  btwncomim  36207  btwnswapid  36211  btwnintr  36213  btwnexch3  36214  trisegint  36222  btwnconn1lem13  36293