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 28974

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 28973	. . . . . . . . . 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 7463	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑞 · (𝐴‘𝑖)) = (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)))
5	4	eqcomd 2746	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = (𝑞 · (𝐴‘𝑖)))
6		simp2 1137	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑟 = ((1 − 𝑞) · (1 − 𝑠)))
7	6	oveq1d 7463	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑟 · (𝐵‘𝑖)) = (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)))
8	5, 7	oveq12d 7466	. . . . . . . . . . . . . . . 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 7463	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)))
11	8, 10	oveq12d 7466	. . . . . . . . . . . . . . 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 11290	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ
15		simpl2l 1226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ (0[,]1))
16		elicc01 13526	. . . . . . . . . . . . . . . . . . . . 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 11600	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (1 − 𝑟) ∈ ℝ)
20	14, 18, 19	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
21	20	recnd 11318	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℂ)
22		simp13l 1288	. . . . . . . . . . . . . . . . . . . . . 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 13526	. . . . . . . . . . . . . . . . . . . . . 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 11600	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
28	14, 26, 27	sylancr 586	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
29		simp121 1305	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐴 ∈ (𝔼‘𝑁))
30		fveere 28934	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
31	29, 30	sylan 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℝ)
32	28, 31	remulcld 11320	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑖)) ∈ ℝ)
33	32	recnd 11318	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑖)) ∈ ℂ)
34		simp123 1307	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐶 ∈ (𝔼‘𝑁))
35		fveere 28934	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
36	34, 35	sylan 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℝ)
37	26, 36	remulcld 11320	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℝ)
38	37	recnd 11318	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑖)) ∈ ℂ)
39	21, 33, 38	adddid 11314	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖)))))
40	28	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
41	31	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴‘𝑖) ∈ ℂ)
42	21, 40, 41	mulassd 11313	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) = ((1 − 𝑟) · ((1 − 𝑡) · (𝐴‘𝑖))))
43	26	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
44		fveecn 28935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
45	34, 44	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶‘𝑖) ∈ ℂ)
46	21, 43, 45	mulassd 11313	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) = ((1 − 𝑟) · (𝑡 · (𝐶‘𝑖))))
47	42, 46	oveq12d 7466	. . . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) = ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
49	48	oveq1d 7463	. . . . . . . . . . . . . 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 11320	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (1 − 𝑡)) ∈ ℝ)
51	50, 31	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℝ)
52	51	recnd 11318	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) ∈ ℂ)
53	20, 26	remulcld 11320	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · 𝑡) ∈ ℝ)
54	53, 36	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) ∈ ℝ)
55	54	recnd 11318	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖)) ∈ ℂ)
56		simp122 1306	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐵 ∈ (𝔼‘𝑁))
57		fveere 28934	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
58	56, 57	sylan 579	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℝ)
59	18, 58	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℝ)
60	59	recnd 11318	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑖)) ∈ ℂ)
61	52, 55, 60	add32d 11517	. . . . . . . . . . . . . 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 2780	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴‘𝑖)) + (𝑟 · (𝐵‘𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶‘𝑖))))
63		simpl2r 1227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ (0[,]1))
64		elicc01 13526	. . . . . . . . . . . . . . . . . . . 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 11600	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℝ ∧ 𝑞 ∈ ℝ) → (1 − 𝑞) ∈ ℝ)
68	14, 66, 67	sylancr 586	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℝ)
69		simp13r 1289	. . . . . . . . . . . . . . . . . . . . 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 13526	. . . . . . . . . . . . . . . . . . . . 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 11600	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (1 − 𝑠) ∈ ℝ)
75	14, 73, 74	sylancr 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℝ)
76	75, 58	remulcld 11320	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℝ)
77	68, 76	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℝ)
78	77	recnd 11318	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) ∈ ℂ)
79	73, 36	remulcld 11320	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℝ)
80	68, 79	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℝ)
81	80	recnd 11318	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))) ∈ ℂ)
82	66, 31	remulcld 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℝ)
83	82	recnd 11318	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴‘𝑖)) ∈ ℂ)
84	78, 81, 83	add32d 11517	. . . . . . . . . . . . . 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 11318	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℂ)
86	76	recnd 11318	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵‘𝑖)) ∈ ℂ)
87	79	recnd 11318	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶‘𝑖)) ∈ ℂ)
88	85, 86, 87	adddid 11314	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))))
89	88	oveq1d 7463	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
90	75	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℂ)
91	58	recnd 11318	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵‘𝑖) ∈ ℂ)
92	85, 90, 91	mulassd 11313	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖)) = ((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))))
93	92	oveq2d 7464	. . . . . . . . . . . . . . . 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 11504	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴‘𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵‘𝑖))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵‘𝑖))) + (𝑞 · (𝐴‘𝑖))))
95	73	recnd 11318	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
96	85, 95, 45	mulassd 11313	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · 𝑠) · (𝐶‘𝑖)) = ((1 − 𝑞) · (𝑠 · (𝐶‘𝑖))))
97	94, 96	oveq12d 7466	. . . . . . . . . . . . . 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 2790	. . . . . . . . . . . . 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 2790	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
100	99	ralrimiva 3152	. . . . . . . . . . 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 3213	. . . . . . . . 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 586	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
107		simpl3l 1228	. . . . . . . . . . . . . . . . . . . . 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 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
111		simpl21 1251	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐴 ∈ (𝔼‘𝑁))
112		fveere 28934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
113	111, 112	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴‘𝑘) ∈ ℝ)
114	110, 113	remulcld 11320	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴‘𝑘)) ∈ ℝ)
115		simpl23 1253	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐶 ∈ (𝔼‘𝑁))
116		fveere 28934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
117	115, 116	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶‘𝑘) ∈ ℝ)
118	109, 117	remulcld 11320	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑡 · (𝐶‘𝑘)) ∈ ℝ)
119	114, 118	readdcld 11319	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) ∈ ℝ)
120	106, 119	remulcld 11320	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) ∈ ℝ)
121		simpl22 1252	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐵 ∈ (𝔼‘𝑁))
122		fveere 28934	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
123	121, 122	sylan 579	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵‘𝑘) ∈ ℝ)
124	105, 123	remulcld 11320	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑟 · (𝐵‘𝑘)) ∈ ℝ)
125	120, 124	readdcld 11319	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) ∈ ℝ)
126	125	ralrimiva 3152	. . . . . . . . . . . . 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 1212	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
129		mptelee 28928	. . . . . . . . . . . . 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 6919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (𝑥‘𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖))
133		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐴‘𝑘) = (𝐴‘𝑖))
134	133	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → ((1 − 𝑡) · (𝐴‘𝑘)) = ((1 − 𝑡) · (𝐴‘𝑖)))
135		fveq2 6920	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝐶‘𝑘) = (𝐶‘𝑖))
136	135	oveq2d 7464	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 = 𝑖 → (𝑡 · (𝐶‘𝑘)) = (𝑡 · (𝐶‘𝑖)))
137	134, 136	oveq12d 7466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘))) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))))
138	137	oveq2d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
139		fveq2 6920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
140	139	oveq2d 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 = 𝑖 → (𝑟 · (𝐵‘𝑘)) = (𝑟 · (𝐵‘𝑖)))
141	138, 140	oveq12d 7466	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
142		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))
143		ovex 7481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∈ V
144	141, 142, 143	fvmpt 7029	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘))))‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
145	132, 144	sylan9eq 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
146	145	eqeq1d 2742	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
147	145	eqeq1d 2742	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
148	146, 147	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
149		eqid 2740	. . . . . . . . . . . . . . . 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 3182	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑘)) + (𝑡 · (𝐶‘𝑘)))) + (𝑟 · (𝐵‘𝑘)))) → (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
153	152	rspcev 3635	. . . . . . . . . . . 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 3174	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))) → ∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
157	156	reximdva 3174	. . . . . . . 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 3296	. . . . . . . . 9 ⊢ (∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
160	159	rexbii 3100	. . . . . . . 8 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
161		rexcom 3296	. . . . . . . 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 7456	. . . . . . . . . . . . 13 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((1 − 𝑟) · (𝐷‘𝑖)) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
165	164	oveq1d 7463	. . . . . . . . . . . 12 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))))
166	165	eqeq2d 2751	. . . . . . . . . . 11 ⊢ ((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖)))))
167		oveq2 7456	. . . . . . . . . . . . 13 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((1 − 𝑞) · (𝐸‘𝑖)) = ((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
168	167	oveq1d 7463	. . . . . . . . . . . 12 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))
169	168	eqeq2d 2751	. . . . . . . . . . 11 ⊢ ((𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))) → ((𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))) ↔ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖)))))
170	166, 169	bi2anan9 637	. . . . . . . . . 10 ⊢ (((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
171	170	ralimi 3089	. . . . . . . . 9 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
172		ralbi 3109	. . . . . . . . 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 3185	. . . . . . 7 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) + (𝑞 · (𝐴‘𝑖))))))
175	174	2rexbidv 3228	. . . . . 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 3218	. . 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 1201	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
181		simp21 1206	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
182		simp23 1208	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
183		brbtwn 28932	. . . . 5 ⊢ ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
184	180, 181, 182, 183	syl3anc 1371	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖)))))
185		simp3r 1202	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
186		simp22 1207	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
187		brbtwn 28932	. . . . 5 ⊢ ((𝐸 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
188	185, 186, 182, 187	syl3anc 1371	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
189	184, 188	anbi12d 631	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖))))))
190		r19.26 3117	. . . . 5 ⊢ (∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
191	190	2rexbii 3135	. . . 4 ⊢ (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ (𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷‘𝑖) = (((1 − 𝑡) · (𝐴‘𝑖)) + (𝑡 · (𝐶‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸‘𝑖) = (((1 − 𝑠) · (𝐵‘𝑖)) + (𝑠 · (𝐶‘𝑖)))))
192		reeanv 3235	. . . 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 1228	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
197		simpl22 1252	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
198		brbtwn 28932	. . . . . 6 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖)))))
199	195, 196, 197, 198	syl3anc 1371	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖)))))
200		simpl3r 1229	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
201		simpl21 1251	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
202		brbtwn 28932	. . . . . 6 ⊢ ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
203	195, 200, 201, 202	syl3anc 1371	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
204	199, 203	anbi12d 631	. . . 4 ⊢ (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
205		r19.26 3117	. . . . . 6 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
206	205	2rexbii 3135	. . . . 5 ⊢ (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖)))))
207		reeanv 3235	. . . . 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 3183	. 2 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥‘𝑖) = (((1 − 𝑟) · (𝐷‘𝑖)) + (𝑟 · (𝐵‘𝑖))) ∧ (𝑥‘𝑖) = (((1 − 𝑞) · (𝐸‘𝑖)) + (𝑞 · (𝐴‘𝑖))))))
211	179, 194, 210	3imtr4d 294	1 ⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 ⟨cop 4654 class class class wbr 5166 ↦ cmpt 5249 ‘cfv 6573 (class class class)co 7448 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 ≤ cle 11325 − cmin 11520 ℕcn 12293 [,]cicc 13410 ...cfz 13567 𝔼cee 28921 Btwn cbtwn 28922

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

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-er 8763 df-map 8886 df-en 9004 df-dom 9005 df-sdom 9006 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-z 12640 df-uz 12904 df-icc 13414 df-fz 13568 df-ee 28924 df-btwn 28925

This theorem is referenced by: eengtrkg 29019 btwncomim 35977 btwnswapid 35981 btwnintr 35983 btwnexch3 35984 trisegint 35992 btwnconn1lem13 36063

W3C validator