Theorem axpasch 28868

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 28867	. . . . . . . . . 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 7402	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑞 · (𝐴‘𝑖)) = (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)))
5	4	eqcomd 2735	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = (𝑞 · (𝐴‘𝑖)))
6		simp2 1137	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑟 = ((1 − 𝑞) · (1 − 𝑠)))
7	6	oveq1d 7402	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑟 · (𝐵‘𝑖)) = (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)))
8	5, 7	oveq12d 7405	. . . . . . . . . . . . . . . 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 7402	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)))
11	8, 10	oveq12d 7405	. . . . . . . . . . . . . . 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 11174	. . . . . . . . . . . . . . . . . . 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 13427	. . . . . . . . . . . . . . . . . . . . 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 11486	. . . . . . . . . . . . . . . . . . 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 11202	. . . . . . . . . . . . . . . . 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 13427	. . . . . . . . . . . . . . . . . . . . . 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 11486	. . . . . . . . . . . . . . . . . . . 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 28828	. . . . . . . . . . . . . . . . . . . 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 11204	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑖)) ∈ ℝ)
33	32	recnd 11202	. . . . . . . . . . . . . . . . 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 28828	. . . . . . . . . . . . . . . . . . . 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 11204	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℝ)
38	37	recnd 11202	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℂ)
39	21, 33, 38	adddid 11198	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖)))))
40	28	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
41	31	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
42	21, 40, 41	mulassd 11197	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = ((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))))
43	26	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
44		fveecn 28829	. . . . . . . . . . . . . . . . . . 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 11197	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖))))
47	42, 46	oveq12d 7405	. . . . . . . . . . . . . . . 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 2767	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
49	48	oveq1d 7402	. . . . . . . . . . . . . 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 11204	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (1 − 𝑡)) ∈ ℝ)
51	50, 31	remulcld 11204	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℝ)
52	51	recnd 11202	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℂ)
53	20, 26	remulcld 11204	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · 𝑡) ∈ ℝ)
54	53, 36	remulcld 11204	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) ∈ ℝ)
55	54	recnd 11202	. . . . . . . . . . . . . . 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 28828	. . . . . . . . . . . . . . . . . 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 11204	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℝ)
60	59	recnd 11202	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℂ)
61	52, 55, 60	add32d 11402	. . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . 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 13427	. . . . . . . . . . . . . . . . . . . 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 11486	. . . . . . . . . . . . . . . . . 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 13427	. . . . . . . . . . . . . . . . . . . . 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 11486	. . . . . . . . . . . . . . . . . . 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 11204	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℝ)
77	68, 76	remulcld 11204	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℝ)
78	77	recnd 11202	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℂ)
79	73, 36	remulcld 11204	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℝ)
80	68, 79	remulcld 11204	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℝ)
81	80	recnd 11202	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℂ)
82	66, 31	remulcld 11204	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℝ)
83	82	recnd 11202	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℂ)
84	78, 81, 83	add32d 11402	. . . . . . . . . . . . . 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 11202	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℂ)
86	76	recnd 11202	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℂ)
87	79	recnd 11202	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℂ)
88	85, 86, 87	adddid 11198	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))))
89	88	oveq1d 7402	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
90	75	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℂ)
91	58	recnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
92	85, 90, 91	mulassd 11197	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)) = ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))))
93	92	oveq2d 7403	. . . . . . . . . . . . . . . 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 11388	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + (𝑞 · (𝐴‘𝑖))))
95	73	recnd 11202	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
96	85, 95, 45	mulassd 11197	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)) = ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))))
97	94, 96	oveq12d 7405	. . . . . . . . . . . . . 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 2774	. . . . . . . . . . . . 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 2774	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
100	99	ralrimiva 3125	. . . . . . . . . . 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 3185	. . . . . . . . 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 28828	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
113	111, 112	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
114	110, 113	remulcld 11204	. . . . . . . . . . . . . . . . 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 28828	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
117	115, 116	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
118	109, 117	remulcld 11204	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑘)) ∈ ℝ)
119	114, 118	readdcld 11203	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) ∈ ℝ)
120	106, 119	remulcld 11204	. . . . . . . . . . . . . . 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 28828	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
123	121, 122	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
124	105, 123	remulcld 11204	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑘)) ∈ ℝ)
125	120, 124	readdcld 11203	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
126	125	ralrimiva 3125	. . . . . . . . . . . . 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 28822	. . . . . . . . . . . . 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 6857	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖))
133		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
134	133	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝐴‘𝑘)) = ((1 − 𝑡) · (𝐴‘𝑖)))
135		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
136	135	oveq2d 7403	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝐶‘𝑘)) = (𝑡 · (𝐶‘𝑖)))
137	134, 136	oveq12d 7405	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))))
138	137	oveq2d 7403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
139		fveq2 6858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
140	139	oveq2d 7403	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑟 · (𝐵‘𝑘)) = (𝑟 · (𝐵‘𝑖)))
141	138, 140	oveq12d 7405	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
142		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))
143		ovex 7420	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∈ V
144	141, 142, 143	fvmpt 6968	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
145	132, 144	sylan9eq 2784	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
146	145	eqeq1d 2731	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
147	145	eqeq1d 2731	. . . . . . . . . . . . . . . 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 2729	. . . . . . . . . . . . . . . 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 3154	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
153	152	rspcev 3588	. . . . . . . . . . . 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 3146	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
157	156	reximdva 3146	. . . . . . . 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 3266	. . . . . . . . 9 ⊢ (∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
160	159	rexbii 3076	. . . . . . . 8 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
161		rexcom 3266	. . . . . . . 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 7395	. . . . . . . . . . . . 13 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((1 − 𝑟) · (𝐷‘𝑖)) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
165	164	oveq1d 7402	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
166	165	eqeq2d 2740	. . . . . . . . . . 11 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
167		oveq2 7395	. . . . . . . . . . . . 13 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((1 − 𝑞) · (𝐸‘𝑖)) = ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
168	167	oveq1d 7402	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
169	168	eqeq2d 2740	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
170	166, 169	bi2anan9 638	. . . . . . . . . 10 ⊢ (((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
171	170	ralimi 3066	. . . . . . . . 9 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
172		ralbi 3085	. . . . . . . . 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 3157	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
175	174	2rexbidv 3202	. . . . . 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 3193	. . 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 28826	. . . . 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 28826	. . . . 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 3091	. . . . 5 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
191	190	2rexbii 3109	. . . 4 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
192		reeanv 3209	. . . 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 28826	. . . . . 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 28826	. . . . . 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 3091	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
206	205	2rexbii 3109	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
207		reeanv 3209	. . . . 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 3155	. 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 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  ⟨cop 4595   class class class wbr 5107   ↦ cmpt 5188  ‘cfv 6511  (class class class)co 7387  ℂcc 11066  ℝcr 11067  0cc0 11068  1c1 11069   + caddc 11071   · cmul 11073   ≤ cle 11209   − cmin 11405  ℕcn 12186  [,]cicc 13309  ...cfz 13468  𝔼cee 28815   Btwn cbtwn 28816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-er 8671  df-map 8801  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-z 12530  df-uz 12794  df-icc 13313  df-fz 13469  df-ee 28818  df-btwn 28819

This theorem is referenced by:  eengtrkg  28913  btwncomim  36001  btwnswapid  36005  btwnintr  36007  btwnexch3  36008  trisegint  36016  btwnconn1lem13  36087