axpasch - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axpasch		Structured version Visualization version GIF version

Theorem axpasch 29328

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 29327	. . . . . . . . . 10 ⊢ ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)))
2	1	3ad2ant3 1153	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)))
3		simp1 1154	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑞 = ((1 − 𝑟) · (1 − 𝑡)))
4	3	oveq1d 7438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑞 · (𝐴‘𝑖)) = (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)))
5	4	eqcomd 2772	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = (𝑞 · (𝐴‘𝑖)))
6		simp2 1155	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑟 = ((1 − 𝑞) · (1 − 𝑠)))
7	6	oveq1d 7438	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑟 · (𝐵‘𝑖)) = (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)))
8	5, 7	oveq12d 7441	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) = ((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))))
9		simp3 1156	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))
10	9	oveq1d 7438	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)))
11	8, 10	oveq12d 7441	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) = (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))))
12	11	3ad2ant3 1153	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) = (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))))
13	12	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))) = (((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖))))
14		1re 11226	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
15		simpl2l 1245	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ (0[,]1))
16		elicc01 13511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ (0[,]1) ↔ (𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ∧ 𝑟 ≤ 1))
17	16	simp1bi 1163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑟 ∈ (0[,]1) → 𝑟 ∈ ℝ)
18	15, 17	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ ℝ)
19		resubcl 11540	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (1 − 𝑟) ∈ ℝ)
20	14, 18, 19	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
21	20	recnd 11255	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℂ)
22		simp13l 1307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝑡 ∈ (0[,]1))
23	22	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
24		elicc01 13511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1))
25	24	simp1bi 1163	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
26	23, 25	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
27		resubcl 11540	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
28	14, 26, 27	sylancr 599	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
29		simp121 1324	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐴 ∈ (𝔼‘𝑁))
30		fveere 29288	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
31	29, 30	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
32	28, 31	remulcld 11257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑖)) ∈ ℝ)
33	32	recnd 11255	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑖)) ∈ ℂ)
34		simp123 1326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐶 ∈ (𝔼‘𝑁))
35		fveere 29288	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
36	34, 35	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
37	26, 36	remulcld 11257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℝ)
38	37	recnd 11255	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℂ)
39	21, 33, 38	adddid 11251	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖)))))
40	28	recnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
41	31	recnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
42	21, 40, 41	mulassd 11250	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = ((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))))
43	26	recnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
44		fveecn 29289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
45	34, 44	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
46	21, 43, 45	mulassd 11250	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖))))
47	42, 46	oveq12d 7441	. . . . . . . . . . . . . . . 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 2804	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
49	48	oveq1d 7438	. . . . . . . . . . . . . 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 11257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (1 − 𝑡)) ∈ ℝ)
51	50, 31	remulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℝ)
52	51	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℂ)
53	20, 26	remulcld 11257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · 𝑡) ∈ ℝ)
54	53, 36	remulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) ∈ ℝ)
55	54	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) ∈ ℂ)
56		simp122 1325	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐵 ∈ (𝔼‘𝑁))
57		fveere 29288	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
58	56, 57	sylan 592	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
59	18, 58	remulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℝ)
60	59	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℂ)
61	52, 55, 60	add32d 11456	. . . . . . . . . . . . . 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 2801	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
63		simpl2r 1246	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ (0[,]1))
64		elicc01 13511	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ (0[,]1) ↔ (𝑞 ∈ ℝ ∧ 0 ≤ 𝑞 ∧ 𝑞 ≤ 1))
65	64	simp1bi 1163	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ (0[,]1) → 𝑞 ∈ ℝ)
66	63, 65	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ ℝ)
67		resubcl 11540	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 𝑞 ∈ ℝ) → (1 − 𝑞) ∈ ℝ)
68	14, 66, 67	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℝ)
69		simp13r 1308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝑠 ∈ (0[,]1))
70	69	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
71		elicc01 13511	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1))
72	71	simp1bi 1163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
73	70, 72	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
74		resubcl 11540	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (1 − 𝑠) ∈ ℝ)
75	14, 73, 74	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℝ)
76	75, 58	remulcld 11257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℝ)
77	68, 76	remulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℝ)
78	77	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℂ)
79	73, 36	remulcld 11257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℝ)
80	68, 79	remulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℝ)
81	80	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℂ)
82	66, 31	remulcld 11257	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℝ)
83	82	recnd 11255	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℂ)
84	78, 81, 83	add32d 11456	. . . . . . . . . . . . . 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 11255	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℂ)
86	76	recnd 11255	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℂ)
87	79	recnd 11255	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℂ)
88	85, 86, 87	adddid 11251	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))))
89	88	oveq1d 7438	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
90	75	recnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℂ)
91	58	recnd 11255	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
92	85, 90, 91	mulassd 11250	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)) = ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))))
93	92	oveq2d 7439	. . . . . . . . . . . . . . . 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 11442	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + (𝑞 · (𝐴‘𝑖))))
95	73	recnd 11255	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
96	85, 95, 45	mulassd 11250	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)) = ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))))
97	94, 96	oveq12d 7441	. . . . . . . . . . . . . 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 2811	. . . . . . . . . . . . 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 2811	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
100	99	ralrimiva 3160	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
101	100	3expia 1139	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
102	101	reximdvva 3216	. . . . . . . . 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 16	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
104		simplrl 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑟 ∈ (0[,]1))
105	104, 17	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑟 ∈ ℝ)
106	14, 105, 19	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
107		simpl3l 1247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝑡 ∈ (0[,]1))
108	107	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
109	108, 25	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
110	14, 109, 27	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
111		simpl21 1270	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐴 ∈ (𝔼‘𝑁))
112		fveere 29288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
113	111, 112	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
114	110, 113	remulcld 11257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑘)) ∈ ℝ)
115		simpl23 1272	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐶 ∈ (𝔼‘𝑁))
116		fveere 29288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
117	115, 116	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
118	109, 117	remulcld 11257	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑘)) ∈ ℝ)
119	114, 118	readdcld 11256	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) ∈ ℝ)
120	106, 119	remulcld 11257	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) ∈ ℝ)
121		simpl22 1271	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐵 ∈ (𝔼‘𝑁))
122		fveere 29288	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
123	121, 122	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
124	105, 123	remulcld 11257	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑘)) ∈ ℝ)
125	120, 124	readdcld 11256	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
126	125	ralrimiva 3160	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
127	126	anassrs 473	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
128		simpll1 1231	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
129		mptelee 29281	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ))
130	128, 129	syl 18	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ))
131	127, 130	mpbird 260	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁))
132		fveq1 6887	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖))
133		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
134	133	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝐴‘𝑘)) = ((1 − 𝑡) · (𝐴‘𝑖)))
135		fveq2 6888	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
136	135	oveq2d 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝐶‘𝑘)) = (𝑡 · (𝐶‘𝑖)))
137	134, 136	oveq12d 7441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))))
138	137	oveq2d 7439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
139		fveq2 6888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
140	139	oveq2d 7439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑟 · (𝐵‘𝑘)) = (𝑟 · (𝐵‘𝑖)))
141	138, 140	oveq12d 7441	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
142		eqid 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))
143		ovex 7456	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∈ V
144	141, 142, 143	fvmpt 6996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
145	132, 144	sylan9eq 2821	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
146	145	eqeq1d 2768	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
147	145	eqeq1d 2768	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
148	146, 147	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
149		eqid 2766	. . . . . . . . . . . . . . . 16 ⊢ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))
150	149	biantrur 540	. . . . . . . . . . . . . . 15 ⊢ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
151	148, 150	bitr4di 292	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
152	151	ralbidva 3189	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
153	152	rspcev 3584	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
154	153	ex 418	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∈ (𝔼‘𝑁) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
155	131, 154	syl 18	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
156	155	reximdva 3181	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
157	156	reximdva 3181	. . . . . . . 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 16	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
159		rexcom 3297	. . . . . . . . 9 ⊢ (∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
160	159	rexbii 3115	. . . . . . . 8 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
161		rexcom 3297	. . . . . . . 8 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
162	160, 161	bitri 278	. . . . . . 7 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
163	158, 162	sylib 221	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
164		oveq2 7431	. . . . . . . . . . . . 13 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((1 − 𝑟) · (𝐷‘𝑖)) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
165	164	oveq1d 7438	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
166	165	eqeq2d 2777	. . . . . . . . . . 11 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
167		oveq2 7431	. . . . . . . . . . . . 13 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((1 − 𝑞) · (𝐸‘𝑖)) = ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
168	167	oveq1d 7438	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
169	168	eqeq2d 2777	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
170	166, 169	bi2anan9 650	. . . . . . . . . 10 ⊢ (((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
171	170	ralimi 3105	. . . . . . . . 9 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
172		ralbi 3123	. . . . . . . . 9 ⊢ (∀𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
173	171, 172	syl 18	. . . . . . . 8 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
174	173	rexbidv 3192	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
175	174	2rexbidv 3233	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
176	163, 175	syl5ibrcom 250	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
177	176	3expia 1139	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))))
178	177	rexlimdvv 3224	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
179	178	3adant3 1150	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
180		simp3l 1220	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
181		simp21 1225	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
182		simp23 1227	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
183		brbtwn 29286	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
184	180, 181, 182, 183	syl3anc 1398	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
185		simp3r 1221	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
186		simp22 1226	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
187		brbtwn 29286	. . . . 5 ⊢ ((𝐸 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
188	185, 186, 182, 187	syl3anc 1398	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
189	184, 188	anbi12d 644	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))))))
190		r19.26 3128	. . . . 5 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
191	190	2rexbii 3144	. . . 4 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
192		reeanv 3240	. . . 4 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
193	191, 192	bitri 278	. . 3 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
194	189, 193	bitr4di 292	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))))))
195		simpr 490	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
196		simpl3l 1247	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
197		simpl22 1271	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
198		brbtwn 29286	. . . . . 6 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖)))))
199	195, 196, 197, 198	syl3anc 1398	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖)))))
200		simpl3r 1248	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
201		simpl21 1270	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
202		brbtwn 29286	. . . . . 6 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
203	195, 200, 201, 202	syl3anc 1398	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
204	199, 203	anbi12d 644	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
205		r19.26 3128	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
206	205	2rexbii 3144	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
207		reeanv 3240	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
208	206, 207	bitri 278	. . . 4 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
209	204, 208	bitr4di 292	. . 3 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
210	209	rexbidva 3190	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
211	179, 194, 210	3imtr4d 297	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2146 ∀wral 3082 ∃wrex 3092 ⟨cop 4600 class class class wbr 5114 ↦ cmpt 5197 ‘cfv 6543 (class class class)co 7423 ℂcc 11116 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 · cmul 11123 ≤ cle 11262 − cmin 11459 ℕcn 12251 [,]cicc 13393 ...cfz 13553 𝔼cee 29274 Btwn cbtwn 29275

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-er 8703 df-map 8835 df-en 8953 df-dom 8954 df-sdom 8955 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-z 12610 df-uz 12881 df-icc 13397 df-fz 13554 df-ee 29277 df-btwn 29278

This theorem is used by: eengtrkg 29373 btwncomim 36526 btwnswapid 36530 btwnintr 36532 btwnexch3 36533 trisegint 36541 btwnconn1lem13 36612

W3C validator