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

Theorem axpasch 27890
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 27889 . . . . . . . . . 10 ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)))
213ad2ant3 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 − 𝑡)))
43oveq1d 7372 . . . . . . . . . . . . . . . . . 18 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑞 · (𝐴𝑖)) = (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)))
54eqcomd 2742 . . . . . . . . . . . . . . . . 17 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) = (𝑞 · (𝐴𝑖)))
6 simp2 1137 . . . . . . . . . . . . . . . . . 18 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → 𝑟 = ((1 − 𝑞) · (1 − 𝑠)))
76oveq1d 7372 . . . . . . . . . . . . . . . . 17 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (𝑟 · (𝐵𝑖)) = (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖)))
85, 7oveq12d 7375 . . . . . . . . . . . . . . . 16 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) = ((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))))
9 simp3 1138 . . . . . . . . . . . . . . . . 17 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))
109oveq1d 7372 . . . . . . . . . . . . . . . 16 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((1 − 𝑟) · 𝑡) · (𝐶𝑖)) = (((1 − 𝑞) · 𝑠) · (𝐶𝑖)))
118, 10oveq12d 7375 . . . . . . . . . . . . . . 15 ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) = (((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶𝑖))))
12113ad2ant3 1135 . . . . . . . . . . . . . 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 11155 . . . . . . . . . . . . . . . . . . 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 13383 . . . . . . . . . . . . . . . . . . . . 21 (𝑟 ∈ (0[,]1) ↔ (𝑟 ∈ ℝ ∧ 0 ≤ 𝑟𝑟 ≤ 1))
1716simp1bi 1145 . . . . . . . . . . . . . . . . . . . 20 (𝑟 ∈ (0[,]1) → 𝑟 ∈ ℝ)
1815, 17syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑟 ∈ ℝ)
19 resubcl 11465 . . . . . . . . . . . . . . . . . . 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 11183 . . . . . . . . . . . . . . . . 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))
2322adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ (0[,]1))
24 elicc01 13383 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 ∈ (0[,]1) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1))
2524simp1bi 1145 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 ∈ (0[,]1) → 𝑡 ∈ ℝ)
2623, 25syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℝ)
27 resubcl 11465 . . . . . . . . . . . . . . . . . . . 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 1305 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → 𝐴 ∈ (𝔼‘𝑁))
30 fveere 27850 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℝ)
3129, 30sylan 580 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℝ)
3228, 31remulcld 11185 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑡) · (𝐴𝑖)) ∈ ℝ)
3332recnd 11183 . . . . . . . . . . . . . . . . 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 27850 . . . . . . . . . . . . . . . . . . . 20 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℝ)
3634, 35sylan 580 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℝ)
3726, 36remulcld 11185 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶𝑖)) ∈ ℝ)
3837recnd 11183 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑡 · (𝐶𝑖)) ∈ ℂ)
3921, 33, 38adddid 11179 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶𝑖)))))
4028recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑡) ∈ ℂ)
4131recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐴𝑖) ∈ ℂ)
4221, 40, 41mulassd 11178 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) = ((1 − 𝑟) · ((1 − 𝑡) · (𝐴𝑖))))
4326recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑡 ∈ ℂ)
44 fveecn 27851 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
4534, 44sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐶𝑖) ∈ ℂ)
4621, 43, 45mulassd 11178 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶𝑖)) = ((1 − 𝑟) · (𝑡 · (𝐶𝑖))))
4742, 46oveq12d 7375 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) = (((1 − 𝑟) · ((1 − 𝑡) · (𝐴𝑖))) + ((1 − 𝑟) · (𝑡 · (𝐶𝑖)))))
4839, 47eqtr4d 2779 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) = ((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))))
4948oveq1d 7372 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) + (𝑟 · (𝐵𝑖))))
5020, 28remulcld 11185 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · (1 − 𝑡)) ∈ ℝ)
5150, 31remulcld 11185 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) ∈ ℝ)
5251recnd 11183 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) ∈ ℂ)
5320, 26remulcld 11185 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑟) · 𝑡) ∈ ℝ)
5453, 36remulcld 11185 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · 𝑡) · (𝐶𝑖)) ∈ ℝ)
5554recnd 11183 . . . . . . . . . . . . . . 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 27850 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℝ)
5856, 57sylan 580 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℝ)
5918, 58remulcld 11185 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵𝑖)) ∈ ℝ)
6059recnd 11183 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑟 · (𝐵𝑖)) ∈ ℂ)
6152, 55, 60add32d 11382 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))) + (𝑟 · (𝐵𝑖))) = (((((1 − 𝑟) · (1 − 𝑡)) · (𝐴𝑖)) + (𝑟 · (𝐵𝑖))) + (((1 − 𝑟) · 𝑡) · (𝐶𝑖))))
6249, 61eqtrd 2776 . . . . . . . . . . . . 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 13383 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ (0[,]1) ↔ (𝑞 ∈ ℝ ∧ 0 ≤ 𝑞𝑞 ≤ 1))
6564simp1bi 1145 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ (0[,]1) → 𝑞 ∈ ℝ)
6663, 65syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑞 ∈ ℝ)
67 resubcl 11465 . . . . . . . . . . . . . . . . . 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 1289 . . . . . . . . . . . . . . . . . . . . 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 13383 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 ∈ (0[,]1) ↔ (𝑠 ∈ ℝ ∧ 0 ≤ 𝑠𝑠 ≤ 1))
7271simp1bi 1145 . . . . . . . . . . . . . . . . . . . 20 (𝑠 ∈ (0[,]1) → 𝑠 ∈ ℝ)
7370, 72syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℝ)
74 resubcl 11465 . . . . . . . . . . . . . . . . . . 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 11185 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵𝑖)) ∈ ℝ)
7768, 76remulcld 11185 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) ∈ ℝ)
7877recnd 11183 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) ∈ ℂ)
7973, 36remulcld 11185 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶𝑖)) ∈ ℝ)
8068, 79remulcld 11185 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶𝑖))) ∈ ℝ)
8180recnd 11183 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (𝑠 · (𝐶𝑖))) ∈ ℂ)
8266, 31remulcld 11185 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴𝑖)) ∈ ℝ)
8382recnd 11183 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑞 · (𝐴𝑖)) ∈ ℂ)
8478, 81, 83add32d 11382 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + (𝑞 · (𝐴𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))))
8568recnd 11183 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑞) ∈ ℂ)
8676recnd 11183 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑠) · (𝐵𝑖)) ∈ ℂ)
8779recnd 11183 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑠 · (𝐶𝑖)) ∈ ℂ)
8885, 86, 87adddid 11179 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))))
8988oveq1d 7372 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) = ((((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + ((1 − 𝑞) · (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
9075recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (1 − 𝑠) ∈ ℂ)
9158recnd 11183 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐵𝑖) ∈ ℂ)
9285, 90, 91mulassd 11178 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖)) = ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))))
9392oveq2d 7373 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) = ((𝑞 · (𝐴𝑖)) + ((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖)))))
9483, 78, 93comraddd 11369 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) = (((1 − 𝑞) · ((1 − 𝑠) · (𝐵𝑖))) + (𝑞 · (𝐴𝑖))))
9573recnd 11183 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑠 ∈ ℂ)
9685, 95, 45mulassd 11178 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · 𝑠) · (𝐶𝑖)) = ((1 − 𝑞) · (𝑠 · (𝐶𝑖))))
9794, 96oveq12d 7375 . . . . . . . . . . . . . 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 2786 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) = (((𝑞 · (𝐴𝑖)) + (((1 − 𝑞) · (1 − 𝑠)) · (𝐵𝑖))) + (((1 − 𝑞) · 𝑠) · (𝐶𝑖))))
9913, 62, 983eqtr4d 2786 . . . . . . . . . . . 12 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
10099ralrimiva 3143 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1)) ∧ (𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠))) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
1011003expia 1121 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → ((𝑞 = ((1 − 𝑟) · (1 − 𝑡)) ∧ 𝑟 = ((1 − 𝑞) · (1 − 𝑠)) ∧ ((1 − 𝑟) · 𝑡) = ((1 − 𝑞) · 𝑠)) → ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
102101reximdvva 3202 . . . . . . . . 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 775 . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . . . . 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 1251 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) → 𝐴 ∈ (𝔼‘𝑁))
112 fveere 27850 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴𝑘) ∈ ℝ)
113111, 112sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴𝑘) ∈ ℝ)
114110, 113remulcld 11185 . . . . . . . . . . . . . . . . 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 27850 . . . . . . . . . . . . . . . . . . 19 ((𝐶 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶𝑘) ∈ ℝ)
117115, 116sylan 580 . . . . . . . . . . . . . . . . . 18 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐶𝑘) ∈ ℝ)
118109, 117remulcld 11185 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑡 · (𝐶𝑘)) ∈ ℝ)
119114, 118readdcld 11184 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘))) ∈ ℝ)
120106, 119remulcld 11185 . . . . . . . . . . . . . . 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 27850 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ (𝔼‘𝑁) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) ∈ ℝ)
123121, 122sylan 580 . . . . . . . . . . . . . . . 16 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝐵𝑘) ∈ ℝ)
124105, 123remulcld 11185 . . . . . . . . . . . . . . 15 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (𝑟 · (𝐵𝑘)) ∈ ℝ)
125120, 124readdcld 11184 . . . . . . . . . . . . . 14 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ (𝑟 ∈ (0[,]1) ∧ 𝑞 ∈ (0[,]1))) ∧ 𝑘 ∈ (1...𝑁)) → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) ∈ ℝ)
126125ralrimiva 3143 . . . . . . . . . . . . 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 1212 . . . . . . . . . . . . 13 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → 𝑁 ∈ ℕ)
129 mptelee 27844 . . . . . . . . . . . . 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 256 . . . . . . . . . . 11 ((((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) ∧ 𝑞 ∈ (0[,]1)) → (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∈ (𝔼‘𝑁))
132 fveq1 6841 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) → (𝑥𝑖) = ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))))‘𝑖))
133 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → (𝐴𝑘) = (𝐴𝑖))
134133oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → ((1 − 𝑡) · (𝐴𝑘)) = ((1 − 𝑡) · (𝐴𝑖)))
135 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → (𝐶𝑘) = (𝐶𝑖))
136135oveq2d 7373 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 = 𝑖 → (𝑡 · (𝐶𝑘)) = (𝑡 · (𝐶𝑖)))
137134, 136oveq12d 7375 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘))) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))))
138137oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
139 fveq2 6842 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (𝐵𝑘) = (𝐵𝑖))
140139oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 𝑖 → (𝑟 · (𝐵𝑘)) = (𝑟 · (𝐵𝑖)))
141138, 140oveq12d 7375 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
142 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))))
143 ovex 7390 . . . . . . . . . . . . . . . . . . 19 (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∈ V
144141, 142, 143fvmpt 6948 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ (1...𝑁) → ((𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘))))‘𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
145132, 144sylan9eq 2796 . . . . . . . . . . . . . . . . 17 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
146145eqeq1d 2738 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖)))))
147145eqeq1d 2738 . . . . . . . . . . . . . . . 16 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
148146, 147anbi12d 631 . . . . . . . . . . . . . . 15 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
149 eqid 2736 . . . . . . . . . . . . . . . 16 (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖)))
150149biantrur 531 . . . . . . . . . . . . . . 15 ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) ↔ ((((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
151148, 150bitr4di 288 . . . . . . . . . . . . . 14 ((𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) ∧ 𝑖 ∈ (1...𝑁)) → (((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
152151ralbidva 3172 . . . . . . . . . . . . 13 (𝑥 = (𝑘 ∈ (1...𝑁) ↦ (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑘)) + (𝑡 · (𝐶𝑘)))) + (𝑟 · (𝐵𝑘)))) → (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
153152rspcev 3581 . . . . . . . . . . . 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 3165 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) ∧ 𝑟 ∈ (0[,]1)) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))) → ∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
157156reximdva 3165 . . . . . . . 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 3273 . . . . . . . . 9 (∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
160159rexbii 3097 . . . . . . . 8 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
161 rexcom 3273 . . . . . . . 8 (∃𝑟 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
162160, 161bitri 274 . . . . . . 7 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∃𝑥 ∈ (𝔼‘𝑁)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
163158, 162sylib 217 . . . . . 6 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
164 oveq2 7365 . . . . . . . . . . . . 13 ((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) → ((1 − 𝑟) · (𝐷𝑖)) = ((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
165164oveq1d 7372 . . . . . . . . . . . 12 ((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) → (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))))
166165eqeq2d 2747 . . . . . . . . . . 11 ((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) → ((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖)))))
167 oveq2 7365 . . . . . . . . . . . . 13 ((𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))) → ((1 − 𝑞) · (𝐸𝑖)) = ((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
168167oveq1d 7372 . . . . . . . . . . . 12 ((𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))) → (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))
169168eqeq2d 2747 . . . . . . . . . . 11 ((𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))) → ((𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))) ↔ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖)))))
170166, 169bi2anan9 637 . . . . . . . . . 10 (((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → (((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
171170ralimi 3086 . . . . . . . . 9 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∀𝑖 ∈ (1...𝑁)(((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
172 ralbi 3106 . . . . . . . . 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 3175 . . . . . . 7 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → (∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
1751742rexbidv 3213 . . . . . 6 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → (∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) + (𝑞 · (𝐴𝑖))))))
176163, 175syl5ibrcom 246 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1))) → (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
1771763expia 1121 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → ((𝑡 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))))
178177rexlimdvv 3204 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁))) → (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) → ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
1791783adant3 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 27848 . . . . 5 ((𝐷 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
184180, 181, 182, 183syl3anc 1371 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐷 Btwn ⟨𝐴, 𝐶⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖)))))
185 simp3r 1202 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐸 ∈ (𝔼‘𝑁))
186 simp22 1207 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → 𝐵 ∈ (𝔼‘𝑁))
187 brbtwn 27848 . . . . 5 ((𝐸 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
188185, 186, 182, 187syl3anc 1371 . . . 4 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (𝐸 Btwn ⟨𝐵, 𝐶⟩ ↔ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
189184, 188anbi12d 631 . . 3 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))))))
190 r19.26 3114 . . . . 5 (∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
1911902rexbii 3128 . . . 4 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
192 reeanv 3217 . . . 4 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
193191, 192bitri 274 . . 3 (∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))) ↔ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ ∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖)))))
194189, 193bitr4di 288 . 2 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) ↔ ∃𝑡 ∈ (0[,]1)∃𝑠 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝐷𝑖) = (((1 − 𝑡) · (𝐴𝑖)) + (𝑡 · (𝐶𝑖))) ∧ (𝐸𝑖) = (((1 − 𝑠) · (𝐵𝑖)) + (𝑠 · (𝐶𝑖))))))
195 simpr 485 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝑥 ∈ (𝔼‘𝑁))
196 simpl3l 1228 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐷 ∈ (𝔼‘𝑁))
197 simpl22 1252 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐵 ∈ (𝔼‘𝑁))
198 brbtwn 27848 . . . . . 6 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖)))))
199195, 196, 197, 198syl3anc 1371 . . . . 5 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐷, 𝐵⟩ ↔ ∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖)))))
200 simpl3r 1229 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐸 ∈ (𝔼‘𝑁))
201 simpl21 1251 . . . . . 6 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → 𝐴 ∈ (𝔼‘𝑁))
202 brbtwn 27848 . . . . . 6 ((𝑥 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁) ∧ 𝐴 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
203195, 200, 201, 202syl3anc 1371 . . . . 5 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → (𝑥 Btwn ⟨𝐸, 𝐴⟩ ↔ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
204199, 203anbi12d 631 . . . 4 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
205 r19.26 3114 . . . . . 6 (∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
2062052rexbii 3128 . . . . 5 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
207 reeanv 3217 . . . . 5 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)(∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
208206, 207bitri 274 . . . 4 (∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))) ↔ (∃𝑟 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ ∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖)))))
209204, 208bitr4di 288 . . 3 (((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) ∧ 𝑥 ∈ (𝔼‘𝑁)) → ((𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
210209rexbidva 3173 . 2 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → (∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩) ↔ ∃𝑥 ∈ (𝔼‘𝑁)∃𝑟 ∈ (0[,]1)∃𝑞 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)((𝑥𝑖) = (((1 − 𝑟) · (𝐷𝑖)) + (𝑟 · (𝐵𝑖))) ∧ (𝑥𝑖) = (((1 − 𝑞) · (𝐸𝑖)) + (𝑞 · (𝐴𝑖))))))
211179, 194, 2103imtr4d 293 1 ((𝑁 ∈ ℕ ∧ (𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁) ∧ 𝐶 ∈ (𝔼‘𝑁)) ∧ (𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁))) → ((𝐷 Btwn ⟨𝐴, 𝐶⟩ ∧ 𝐸 Btwn ⟨𝐵, 𝐶⟩) → ∃𝑥 ∈ (𝔼‘𝑁)(𝑥 Btwn ⟨𝐷, 𝐵⟩ ∧ 𝑥 Btwn ⟨𝐸, 𝐴⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  cop 4592   class class class wbr 5105  cmpt 5188  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  cle 11190  cmin 11385  cn 12153  [,]cicc 13267  ...cfz 13424  𝔼cee 27837   Btwn cbtwn 27838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-z 12500  df-uz 12764  df-icc 13271  df-fz 13425  df-ee 27840  df-btwn 27841
This theorem is referenced by:  eengtrkg  27935  btwncomim  34598  btwnswapid  34602  btwnintr  34604  btwnexch3  34605  trisegint  34613  btwnconn1lem13  34684
  Copyright terms: Public domain W3C validator