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

Theorem axpasch 26660
 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.
StepHypRef Expression
1 axpaschlem 26659 . . . . . . . . . 10 ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)))
213ad2ant3 1129 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)))
3 simp1 1130 . . . . . . . . . . . . . . . . . . 19 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑞 = ((1 − 𝑟) · (1 − 𝑡)))
43oveq1d 7165 . . . . . . . . . . . . . . . . . 18 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑞 · (𝐴𝑖)) = (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)))
54eqcomd 2832 . . . . . . . . . . . . . . . . 17 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) = (𝑞 · (𝐴𝑖)))
6 simp2 1131 . . . . . . . . . . . . . . . . . 18 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑟 = ((1 − 𝑞) · (1 − 𝑠)))
76oveq1d 7165 . . . . . . . . . . . . . . . . 17 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑟 · (𝐵𝑖)) = (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖)))
85, 7oveq12d 7168 . . . . . . . . . . . . . . . 16 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) = ((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))))
9 simp3 1132 . . . . . . . . . . . . . . . . 17 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))
109oveq1d 7165 . . . . . . . . . . . . . . . 16 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · 𝑡) · (𝐶𝑖)) = (((1 − 𝑞) · 𝑠) · (𝐶𝑖)))
118, 10oveq12d 7168 . . . . . . . . . . . . . . 15 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) = (((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶𝑖))))
12113ad2ant3 1129 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) = (((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶𝑖))))
1312adantr 481 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) = (((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶𝑖))))
14 1re 10635 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
15 simpl2l 1220 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ (0[,]1))
16 elicc01 12849 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ (0[,]1) ↔ (𝑟 ∈ ℝ ∧ 0 ≤ 𝑟𝑟 ≤ 1))
1716simp1bi 1139 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ (0[,]1) → 𝑟 ∈ ℝ)
1815, 17syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ ℝ)
19 resubcl 10944 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (1 − 𝑟) ∈ ℝ)
2014, 18, 19sylancr 587 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
2120recnd 10663 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℂ)
22 simp13l 1282 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝑡 ∈ (0[,]1))
2322adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
24 elicc01 12849 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
2524simp1bi 1139 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
2623, 25syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
27 resubcl 10944 . . . . . . . . . . . . . . . . . . . 20 ((1 ∈ ℝ ∧ 𝑡 ∈ ℝ) → (1 − 𝑡) ∈ ℝ)
2814, 26, 27sylancr 587 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
29 simp121 1299 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐴 ∈ (𝔼‘𝑁))
30 fveere 26620 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℝ)
3129, 30sylan 580 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℝ)
3228, 31remulcld 10665 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴𝑖)) ∈ ℝ)
3332recnd 10663 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴𝑖)) ∈ ℂ)
34 simp123 1301 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐶 ∈ (𝔼‘𝑁))
35 fveere 26620 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℝ)
3634, 35sylan 580 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℝ)
3726, 36remulcld 10665 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶𝑖)) ∈ ℝ)
3837recnd 10663 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶𝑖)) ∈ ℂ)
3921, 33, 38adddid 10659 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶𝑖)))))
4028recnd 10663 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
4131recnd 10663 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℂ)
4221, 40, 41mulassd 10658 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) = ((1 − 𝑟) · ((1 − 𝑡) · (𝐴𝑖))))
4326recnd 10663 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
44 fveecn 26621 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
4534, 44sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
4621, 43, 45mulassd 10658 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶𝑖)) = ((1 − 𝑟) · (𝑡 · (𝐶𝑖))))
4742, 46oveq12d 7168 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶𝑖)))))
4839, 47eqtr4d 2864 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) = ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))))
4948oveq1d 7165 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) + (𝑟 · (𝐵𝑖))))
5020, 28remulcld 10665 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (1 − 𝑡)) ∈ ℝ)
5150, 31remulcld 10665 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) ∈ ℝ)
5251recnd 10663 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) ∈ ℂ)
5320, 26remulcld 10665 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · 𝑡) ∈ ℝ)
5453, 36remulcld 10665 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶𝑖)) ∈ ℝ)
5554recnd 10663 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶𝑖)) ∈ ℂ)
56 simp122 1300 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐵 ∈ (𝔼‘𝑁))
57 fveere 26620 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℝ)
5856, 57sylan 580 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℝ)
5918, 58remulcld 10665 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵𝑖)) ∈ ℝ)
6059recnd 10663 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵𝑖)) ∈ ℂ)
6152, 55, 60add32d 10861 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) + (𝑟 · (𝐵𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))))
6249, 61eqtrd 2861 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))))
63 simpl2r 1221 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ (0[,]1))
64 elicc01 12849 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ (0[,]1) ↔ (𝑞 ∈ ℝ ∧ 0 ≤ 𝑞𝑞 ≤ 1))
6564simp1bi 1139 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ (0[,]1) → 𝑞 ∈ ℝ)
6663, 65syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ ℝ)
67 resubcl 10944 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℝ ∧ 𝑞 ∈ ℝ) → (1 − 𝑞) ∈ ℝ)
6814, 66, 67sylancr 587 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℝ)
69 simp13r 1283 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝑠 ∈ (0[,]1))
7069adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ (0[,]1))
71 elicc01 12849 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
7271simp1bi 1139 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
7370, 72syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
74 resubcl 10944 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℝ ∧ 𝑠 ∈ ℝ) → (1 − 𝑠) ∈ ℝ)
7514, 73, 74sylancr 587 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℝ)
7675, 58remulcld 10665 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵𝑖)) ∈ ℝ)
7768, 76remulcld 10665 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) ∈ ℝ)
7877recnd 10663 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) ∈ ℂ)
7973, 36remulcld 10665 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶𝑖)) ∈ ℝ)
8068, 79remulcld 10665 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶𝑖))) ∈ ℝ)
8180recnd 10663 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶𝑖))) ∈ ℂ)
8266, 31remulcld 10665 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴𝑖)) ∈ ℝ)
8382recnd 10663 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴𝑖)) ∈ ℂ)
8478, 81, 83add32d 10861 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + (𝑞 · (𝐴𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))))
8568recnd 10663 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℂ)
8676recnd 10663 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵𝑖)) ∈ ℂ)
8779recnd 10663 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶𝑖)) ∈ ℂ)
8885, 86, 87adddid 10659 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))))
8988oveq1d 7165 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
9075recnd 10663 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℂ)
9158recnd 10663 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
9285, 90, 91mulassd 10658 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖)) = ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))))
9392oveq2d 7166 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) = ((𝑞 · (𝐴𝑖)) + ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖)))))
9483, 78, 93comraddd 10848 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + (𝑞 · (𝐴𝑖))))
9573recnd 10663 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
9685, 95, 45mulassd 10658 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · 𝑠) · (𝐶𝑖)) = ((1 − 𝑞) · (𝑠 · (𝐶𝑖))))
9794, 96oveq12d 7168 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + (𝑞 · (𝐴𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))))
9884, 89, 973eqtr4d 2871 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) = (((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶𝑖))))
9913, 62, 983eqtr4d 2871 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
10099ralrimiva 3187 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
1011003expia 1115 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
102101reximdvva 3282 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
1032, 102mpd 15 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
104 simplrl 773 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑟 ∈ (0[,]1))
105104, 17syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑟 ∈ ℝ)
10614, 105, 19sylancr 587 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑟) ∈ ℝ)
107 simpl3l 1222 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝑡 ∈ (0[,]1))
108107adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
109108, 25syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
11014, 109, 27sylancr 587 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℝ)
111 simpl21 1245 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐴 ∈ (𝔼‘𝑁))
112 fveere 26620 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴𝑘) ∈ ℝ)
113111, 112sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴𝑘) ∈ ℝ)
114110, 113remulcld 10665 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴𝑘)) ∈ ℝ)
115 simpl23 1247 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐶 ∈ (𝔼‘𝑁))
116 fveere 26620 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶𝑘) ∈ ℝ)
117115, 116sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶𝑘) ∈ ℝ)
118109, 117remulcld 10665 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑡 · (𝐶𝑘)) ∈ ℝ)
119114, 118readdcld 10664 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘))) ∈ ℝ)
120106, 119remulcld 10665 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) ∈ ℝ)
121 simpl22 1246 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐵 ∈ (𝔼‘𝑁))
122 fveere 26620 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) ∈ ℝ)
123121, 122sylan 580 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) ∈ ℝ)
124105, 123remulcld 10665 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑟 · (𝐵𝑘)) ∈ ℝ)
125120, 124readdcld 10664 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) ∈ ℝ)
126125ralrimiva 3187 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) ∈ ℝ)
127126anassrs 468 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) ∈ ℝ)
128 simpll1 1206 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
129 mptelee 26614 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) ∈ ℝ))
130128, 129syl 17 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∈ (𝔼‘𝑁) ↔ ∀𝑘 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) ∈ ℝ))
131127, 130mpbird 258 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∈ (𝔼‘𝑁))
132 fveq1 6668 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) → (𝑥𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))))‘𝑖))
133 fveq2 6669 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → (𝐴𝑘) = (𝐴𝑖))
134133oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → ((1 − 𝑡) · (𝐴𝑘)) = ((1 − 𝑡) · (𝐴𝑖)))
135 fveq2 6669 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → (𝐶𝑘) = (𝐶𝑖))
136135oveq2d 7166 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → (𝑡 · (𝐶𝑘)) = (𝑡 · (𝐶𝑖)))
137134, 136oveq12d 7168 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘))) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))))
138137oveq2d 7166 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
139 fveq2 6669 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝐵𝑘) = (𝐵𝑖))
140139oveq2d 7166 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (𝑟 · (𝐵𝑘)) = (𝑟 · (𝐵𝑖)))
141138, 140oveq12d 7168 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
142 eqid 2826 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))))
143 ovex 7183 . . . . . . . . . . . . . . . . . . 19 (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∈ V
144141, 142, 143fvmpt 6767 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))))‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
145132, 144sylan9eq 2881 . . . . . . . . . . . . . . . . 17 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
146145eqeq1d 2828 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖)))))
147145eqeq1d 2828 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
148146, 147anbi12d 630 . . . . . . . . . . . . . . 15 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
149 eqid 2826 . . . . . . . . . . . . . . . 16 (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖)))
150149biantrur 531 . . . . . . . . . . . . . . 15 ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
151148, 150syl6bbr 290 . . . . . . . . . . . . . 14 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
152151ralbidva 3201 . . . . . . . . . . . . 13 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) → (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
153152rspcev 3627 . . . . . . . . . . . 12 (((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∈ (𝔼‘𝑁) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
154153ex 413 . . . . . . . . . . 11 ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∈ (𝔼‘𝑁) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
155131, 154syl 17 . . . . . . . . . 10 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) → ∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
156155reximdva 3279 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) → ∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
157156reximdva 3279 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
158103, 157mpd 15 . . . . . . 7 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
159 rexcom 3360 . . . . . . . . 9 (∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
160159rexbii 3252 . . . . . . . 8 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
161 rexcom 3360 . . . . . . . 8 (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
162160, 161bitri 276 . . . . . . 7 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
163158, 162sylib 219 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
164 oveq2 7158 . . . . . . . . . . . . 13 ((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) → ((1 − 𝑟) · (𝐷𝑖)) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
165164oveq1d 7165 . . . . . . . . . . . 12 ((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) → (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
166165eqeq2d 2837 . . . . . . . . . . 11 ((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) → ((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖)))))
167 oveq2 7158 . . . . . . . . . . . . 13 ((𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))) → ((1 − 𝑞) · (𝐸𝑖)) = ((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
168167oveq1d 7165 . . . . . . . . . . . 12 ((𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))) → (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
169168eqeq2d 2837 . . . . . . . . . . 11 ((𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))) → ((𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
170166, 169bi2anan9 635 . . . . . . . . . 10 (((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → (((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
171170ralimi 3165 . . . . . . . . 9 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
172 ralbi 3172 . . . . . . . . 9 (∀𝑖 ∈ (1...𝑁)(((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
173171, 172syl 17 . . . . . . . 8 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
174173rexbidv 3302 . . . . . . 7 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
1751742rexbidv 3305 . . . . . 6 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
176163, 175syl5ibrcom 248 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
1771763expia 1115 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))))
178177rexlimdvv 3298 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
1791783adant3 1126 . 2 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
180 simp3l 1195 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐷 ∈ (𝔼‘𝑁))
181 simp21 1200 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐴 ∈ (𝔼‘𝑁))
182 simp23 1202 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐶 ∈ (𝔼‘𝑁))
183 brbtwn 26618 . . . . 5 ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
184180, 181, 182, 183syl3anc 1365 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
185 simp3r 1196 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
186 simp22 1201 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
187 brbtwn 26618 . . . . 5 ((𝐸 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
188185, 186, 182, 187syl3anc 1365 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
189184, 188anbi12d 630 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))))))
190 r19.26 3175 . . . . 5 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
1911902rexbii 3253 . . . 4 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
192 reeanv 3373 . . . 4 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
193191, 192bitri 276 . . 3 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
194189, 193syl6bbr 290 . 2 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))))))
195 simpr 485 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
196 simpl3l 1222 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
197 simpl22 1246 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
198 brbtwn 26618 . . . . . 6 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖)))))
199195, 196, 197, 198syl3anc 1365 . . . . 5 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖)))))
200 simpl3r 1223 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
201 simpl21 1245 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
202 brbtwn 26618 . . . . . 6 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
203195, 200, 201, 202syl3anc 1365 . . . . 5 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
204199, 203anbi12d 630 . . . 4 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
205 r19.26 3175 . . . . . 6 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
2062052rexbii 3253 . . . . 5 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
207 reeanv 3373 . . . . 5 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
208206, 207bitri 276 . . . 4 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
209204, 208syl6bbr 290 . . 3 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
210209rexbidva 3301 . 2 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
211179, 194, 2103imtr4d 295 1 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  ∀wral 3143  ∃wrex 3144  ⟨cop 4570   class class class wbr 5063   ↦ cmpt 5143  ‘cfv 6354  (class class class)co 7150  ℂcc 10529  ℝcr 10530  0cc0 10531  1c1 10532   + caddc 10534   · cmul 10536   ≤ cle 10670   − cmin 10864  ℕcn 11632  [,]cicc 12736  ...cfz 12887  𝔼cee 26607   Btwn cbtwn 26608 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-er 8284  df-map 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-div 11292  df-nn 11633  df-z 11976  df-uz 12238  df-icc 12740  df-fz 12888  df-ee 26610  df-btwn 26611 This theorem is referenced by:  eengtrkg  26705  btwncomim  33377  btwnswapid  33381  btwnintr  33383  btwnexch3  33384  trisegint  33392  btwnconn1lem13  33463
 Copyright terms: Public domain W3C validator