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 ⟨ 𝐸 , 𝐴 ⟩ ) ) )