Metamath Proof Explorer

Theorem axpasch

Description: The inner Pasch axiom. Take a triangle A C E , a point D on A C , and a point B extending C E . Then A E and D B intersect at some point x . Axiom A7 of Schwabhauser p. 12. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axpasch ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝑥 Btwn ⟨ 𝐸 , 𝐴 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 axpaschlem ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) )
2 1 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) )
3 simp1 ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) )
4 3 oveq1d ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) )
5 4 eqcomd ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) = ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) )
6 simp2 ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) )
7 6 oveq1d ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) )
8 5 7 oveq12d ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) )
9 simp3 ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) )
10 9 oveq1d ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑞 ) · 𝑠 ) · ( 𝐶 ‘ 𝑖 ) ) )
11 8 10 oveq12d ⊢ ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ( ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑞 ) · 𝑠 ) · ( 𝐶 ‘ 𝑖 ) ) ) )
12 11 3ad2ant3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) → ( ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑞 ) · 𝑠 ) · ( 𝐶 ‘ 𝑖 ) ) ) )
13 12 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑞 ) · 𝑠 ) · ( 𝐶 ‘ 𝑖 ) ) ) )
14 1re ⊢ 1 ∈ ℝ
15 simpl2l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑟 ∈ ( 0 [,] 1 ) )
16 elicc01 ⊢ ( 𝑟 ∈ ( 0 [,] 1 ) ↔ ( 𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ∧ 𝑟 ≤ 1 ) )
17 16 simp1bi ⊢ ( 𝑟 ∈ ( 0 [,] 1 ) → 𝑟 ∈ ℝ )
18 15 17 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑟 ∈ ℝ )
19 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 1 − 𝑟 ) ∈ ℝ )
20 14 18 19 sylancr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑟 ) ∈ ℝ )
21 20 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑟 ) ∈ ℂ )
22 simp13l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
23 22 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
24 elicc01 ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) )
25 24 simp1bi ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℝ )
26 23 25 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℝ )
27 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) ∈ ℝ )
28 14 26 27 sylancr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) ∈ ℝ )
29 simp121 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
30 fveere ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
31 29 30 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℝ )
32 28 31 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
33 32 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
34 simp123 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
35 fveere ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ )
36 34 35 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℝ )
37 26 36 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ )
38 37 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ∈ ℂ )
39 21 33 38 adddid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑟 ) · ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
40 28 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
41 31 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
42 21 40 41 mulassd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − 𝑟 ) · ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
43 26 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
44 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
45 34 44 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
46 21 43 45 mulassd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) = ( ( 1 − 𝑟 ) · ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) )
47 42 46 oveq12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑟 ) · ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
48 39 47 eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) = ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) )
49 48 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) )
50 20 28 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∈ ℝ )
51 50 31 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
52 51 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
53 20 26 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑟 ) · 𝑡 ) ∈ ℝ )
54 53 36 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ )
55 54 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ∈ ℂ )
56 simp122 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
57 fveere ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
58 56 57 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℝ )
59 18 58 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
60 59 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
61 52 55 60 add32d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) )
62 49 61 eqtrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑟 ) · 𝑡 ) · ( 𝐶 ‘ 𝑖 ) ) ) )
63 simpl2r ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑞 ∈ ( 0 [,] 1 ) )
64 elicc01 ⊢ ( 𝑞 ∈ ( 0 [,] 1 ) ↔ ( 𝑞 ∈ ℝ ∧ 0 ≤ 𝑞 ∧ 𝑞 ≤ 1 ) )
65 64 simp1bi ⊢ ( 𝑞 ∈ ( 0 [,] 1 ) → 𝑞 ∈ ℝ )
66 63 65 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑞 ∈ ℝ )
67 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑞 ∈ ℝ ) → ( 1 − 𝑞 ) ∈ ℝ )
68 14 66 67 sylancr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑞 ) ∈ ℝ )
69 simp13r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
70 69 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
71 elicc01 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) ↔ ( 𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1 ) )
72 71 simp1bi ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → 𝑠 ∈ ℝ )
73 70 72 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℝ )
74 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑠 ∈ ℝ ) → ( 1 − 𝑠 ) ∈ ℝ )
75 14 73 74 sylancr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑠 ) ∈ ℝ )
76 75 58 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℝ )
77 68 76 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) ∈ ℝ )
78 77 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) ∈ ℂ )
79 73 36 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ∈ ℝ )
80 68 79 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ∈ ℝ )
81 80 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ∈ ℂ )
82 66 31 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ∈ ℝ )
83 82 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
84 78 81 83 add32d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
85 68 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑞 ) ∈ ℂ )
86 76 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
87 79 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ∈ ℂ )
88 85 86 87 adddid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
89 88 oveq1d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) )
90 75 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑠 ) ∈ ℂ )
91 58 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
92 85 90 91 mulassd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) = ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) )
93 92 oveq2d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) ) )
94 83 78 93 comraddd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) )
95 73 recnd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
96 85 95 45 mulassd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑞 ) · 𝑠 ) · ( 𝐶 ‘ 𝑖 ) ) = ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) )
97 94 96 oveq12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑞 ) · 𝑠 ) · ( 𝐶 ‘ 𝑖 ) ) ) = ( ( ( ( 1 − 𝑞 ) · ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑞 ) · ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
98 84 89 97 3eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑞 ) · 𝑠 ) · ( 𝐶 ‘ 𝑖 ) ) ) )
99 13 62 98 3eqtr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) )
100 99 ralrimiva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) )
101 100 3expia ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
102 101 reximdvva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( 𝑞 = ( ( 1 − 𝑟 ) · ( 1 − 𝑡 ) ) ∧ 𝑟 = ( ( 1 − 𝑞 ) · ( 1 − 𝑠 ) ) ∧ ( ( 1 − 𝑟 ) · 𝑡 ) = ( ( 1 − 𝑞 ) · 𝑠 ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
103 2 102 mpd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) )
104 simplrl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑟 ∈ ( 0 [,] 1 ) )
105 104 17 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑟 ∈ ℝ )
106 14 105 19 sylancr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑟 ) ∈ ℝ )
107 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
108 107 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
109 108 25 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℝ )
110 14 109 27 sylancr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) ∈ ℝ )
111 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
112 fveere ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
113 111 112 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
114 110 113 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
115 simpl23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
116 fveere ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℝ )
117 115 116 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℝ )
118 109 117 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ∈ ℝ )
119 114 118 readdcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ∈ ℝ )
120 106 119 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) ∈ ℝ )
121 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
122 fveere ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
123 121 122 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
124 105 123 remulcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ∈ ℝ )
125 120 124 readdcld ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
126 125 ralrimiva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ( 𝑟 ∈ ( 0 [,] 1 ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
127 126 anassrs ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ )
128 simpll1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) → 𝑁 ∈ ℕ )
129 mptelee ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ ) )
130 128 129 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ∈ ℝ ) )
131 127 130 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
132 fveq1 ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) )
133 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑖 ) )
134 133 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) = ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) )
135 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑖 ) )
136 135 oveq2d ⊢ ( 𝑘 = 𝑖 → ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) = ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) )
137 134 136 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) )
138 137 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) = ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
139 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑖 ) )
140 139 oveq2d ⊢ ( 𝑘 = 𝑖 → ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) = ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) )
141 138 140 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) )
142 eqid ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) )
143 ovex ⊢ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∈ V
144 141 142 143 fvmpt ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) )
145 132 144 sylan9eq ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) )
146 145 eqeq1d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
147 145 eqeq1d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
148 146 147 anbi12d ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
149 eqid ⊢ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) )
150 149 biantrur ⊢ ( ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
151 148 150 bitr4di ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
152 151 ralbidva ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
153 152 rspcev ⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
154 153 ex ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑘 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
155 131 154 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑟 ∈ ( 0 [,] 1 ) ) ∧ 𝑞 ∈ ( 0 [,] 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
156 155 reximdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑟 ∈ ( 0 [,] 1 ) ) → ( ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) → ∃ 𝑞 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
157 156 reximdva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
158 103 157 mpd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
159 rexcom ⊢ ( ∃ 𝑞 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
160 159 rexbii ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
161 rexcom ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
162 160 161 bitri ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
163 158 162 sylib ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
164 oveq2 ⊢ ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) = ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
165 164 oveq1d ⊢ ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) )
166 165 eqeq2d ⊢ ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
167 oveq2 ⊢ ( ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) = ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
168 167 oveq1d ⊢ ( ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) )
169 168 eqeq2d ⊢ ( ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
170 166 169 bi2anan9 ⊢ ( ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
171 170 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
172 ralbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
173 171 172 syl ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
174 173 rexbidv ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
175 174 2rexbidv ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
176 163 175 syl5ibrcom ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
177 176 3expia ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) ) )
178 177 rexlimdvv ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
179 178 3adant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
180 simp3l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
181 simp21 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
182 simp23 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) )
183 brbtwn ⊢ ( ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
184 180 181 182 183 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
185 simp3r ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
186 simp22 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
187 brbtwn ⊢ ( ( 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝐸 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
188 185 186 182 187 syl3anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝐸 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
189 184 188 anbi12d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
190 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
191 190 2rexbii ⊢ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
192 reeanv ⊢ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
193 191 192 bitri ⊢ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
194 189 193 bitr4di ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐷 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝐶 ‘ 𝑖 ) ) ) ∧ ( 𝐸 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
195 simpr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
196 simpl3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) )
197 simpl22 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
198 brbtwn ⊢ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐷 , 𝐵 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
199 195 196 197 198 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐷 , 𝐵 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ) )
200 simpl3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) )
201 simpl21 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
202 brbtwn ⊢ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐸 , 𝐴 ⟩ ↔ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
203 195 200 201 202 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝐸 , 𝐴 ⟩ ↔ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
204 199 203 anbi12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑥 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝑥 Btwn ⟨ 𝐸 , 𝐴 ⟩ ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
205 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
206 205 2rexbii ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
207 reeanv ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
208 206 207 bitri ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) )
209 204 208 bitr4di ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑥 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝑥 Btwn ⟨ 𝐸 , 𝐴 ⟩ ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
210 209 rexbidva ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝑥 Btwn ⟨ 𝐸 , 𝐴 ⟩ ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑞 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐷 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝐵 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑞 ) · ( 𝐸 ‘ 𝑖 ) ) + ( 𝑞 · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
211 179 194 210 3imtr4d ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐸 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐸 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ( 𝑥 Btwn ⟨ 𝐷 , 𝐵 ⟩ ∧ 𝑥 Btwn ⟨ 𝐸 , 𝐴 ⟩ ) ) )