Metamath Proof Explorer

Theorem axeuclidlem

Description: Lemma for axeuclid . Handle the algebraic aspects of the theorem. (Contributed by Scott Fenton, 9-Sep-2013)

Ref Expression
Assertion axeuclidlem ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp21 ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → 𝑃 ∈ ( 0 [,] 1 ) )
2 simp22 ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → 𝑄 ∈ ( 0 [,] 1 ) )
3 fveere ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
4 3 expcom ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ ) )
5 fveere ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
6 5 expcom ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) )
7 4 6 anim12d ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ) )
8 fveere ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℝ )
9 8 expcom ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐶 ‘ 𝑘 ) ∈ ℝ ) )
10 fveere ⊢ ( ( 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑘 ) ∈ ℝ )
11 10 expcom ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) )
12 9 11 anim12d ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) )
13 7 12 anim12d ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ) )
14 13 impcom ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) )
15 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
16 15 sseli ⊢ ( 𝑃 ∈ ( 0 [,] 1 ) → 𝑃 ∈ ℝ )
17 16 3ad2ant1 ⊢ ( ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) → 𝑃 ∈ ℝ )
18 17 adantl ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑃 ∈ ℝ )
19 peano2rem ⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
20 18 19 syl ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
21 simplll ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℝ )
22 20 21 remulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) ∈ ℝ )
23 simpllr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ℝ )
24 22 23 readdcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) ∈ ℝ )
25 simpr3 ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑃 ≠ 0 )
26 24 18 25 redivcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
27 14 26 sylan ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
28 27 an32s ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
29 28 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
30 eleenn ⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
31 30 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑁 ∈ ℕ )
32 mptelee ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ ) )
33 31 32 syl ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ ) )
34 29 33 mpbird ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
35 34 3adant3 ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
36 simplrl ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐶 ‘ 𝑘 ) ∈ ℝ )
37 22 36 readdcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) ∈ ℝ )
38 37 18 25 redivcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝐵 ‘ 𝑘 ) ∈ ℝ ) ∧ ( ( 𝐶 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑇 ‘ 𝑘 ) ∈ ℝ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
39 14 38 sylan ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
40 39 an32s ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
41 40 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ )
42 mptelee ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ ) )
43 31 42 syl ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ∈ ℝ ) )
44 41 43 mpbird ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
45 44 3adant3 ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
46 fveecn ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
47 46 expcom ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ ) )
48 fveecn ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
49 48 expcom ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) )
50 47 49 anim12d ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ) )
51 fveecn ⊢ ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
52 51 expcom ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ ) )
53 fveecn ⊢ ( ( 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑇 ‘ 𝑖 ) ∈ ℂ )
54 53 expcom ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) )
55 52 54 anim12d ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) )
56 50 55 anim12d ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ) )
57 56 impcom ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) )
58 eqcom ⊢ ( ( 𝑇 ‘ 𝑖 ) = ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) ↔ ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) = ( 𝑇 ‘ 𝑖 ) )
59 ax-1cn ⊢ 1 ∈ ℂ
60 simpr2 ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑄 ∈ ( 0 [,] 1 ) )
61 15 sseli ⊢ ( 𝑄 ∈ ( 0 [,] 1 ) → 𝑄 ∈ ℝ )
62 61 recnd ⊢ ( 𝑄 ∈ ( 0 [,] 1 ) → 𝑄 ∈ ℂ )
63 60 62 syl ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑄 ∈ ℂ )
64 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑄 ∈ ℂ ) → ( 1 − 𝑄 ) ∈ ℂ )
65 59 63 64 sylancr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 1 − 𝑄 ) ∈ ℂ )
66 simpr1 ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑃 ∈ ( 0 [,] 1 ) )
67 16 recnd ⊢ ( 𝑃 ∈ ( 0 [,] 1 ) → 𝑃 ∈ ℂ )
68 66 67 syl ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑃 ∈ ℂ )
69 subcl ⊢ ( ( 𝑃 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑃 − 1 ) ∈ ℂ )
70 68 59 69 sylancl ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑃 − 1 ) ∈ ℂ )
71 simplll ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ ℂ )
72 70 71 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
73 65 72 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ )
74 63 72 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ∈ ℂ )
75 73 74 addcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) ∈ ℂ )
76 simpllr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐵 ‘ 𝑖 ) ∈ ℂ )
77 65 76 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
78 simplrl ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐶 ‘ 𝑖 ) ∈ ℂ )
79 63 78 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ∈ ℂ )
80 77 79 addcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ∈ ℂ )
81 75 80 addcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) ∈ ℂ )
82 simplrr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑇 ‘ 𝑖 ) ∈ ℂ )
83 simpr3 ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → 𝑃 ≠ 0 )
84 81 68 82 83 divmuld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) = ( 𝑇 ‘ 𝑖 ) ↔ ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
85 58 84 syl5bb ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑇 ‘ 𝑖 ) = ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) ↔ ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
86 negsubdi2 ⊢ ( ( 1 ∈ ℂ ∧ 𝑃 ∈ ℂ ) → - ( 1 − 𝑃 ) = ( 𝑃 − 1 ) )
87 59 68 86 sylancr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → - ( 1 − 𝑃 ) = ( 𝑃 − 1 ) )
88 87 oveq1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( - ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) )
89 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( 1 − 𝑃 ) ∈ ℂ )
90 59 68 89 sylancr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 1 − 𝑃 ) ∈ ℂ )
91 90 71 mulneg1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( - ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) = - ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) )
92 npcan ⊢ ( ( 1 ∈ ℂ ∧ 𝑄 ∈ ℂ ) → ( ( 1 − 𝑄 ) + 𝑄 ) = 1 )
93 59 63 92 sylancr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 1 − 𝑄 ) + 𝑄 ) = 1 )
94 93 oveq1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑄 ) + 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( 1 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
95 65 63 72 adddird ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑄 ) + 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) )
96 72 mulid2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 1 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) )
97 94 95 96 3eqtr3rd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) )
98 88 91 97 3eqtr3d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → - ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) )
99 98 oveq2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) + - ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) ) )
100 90 71 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ∈ ℂ )
101 80 100 negsubd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) + - ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) − ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
102 80 75 addcomd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) + ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
103 99 101 102 3eqtr3d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) − ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
104 103 eqeq1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) − ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ↔ ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) = ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) )
105 eqcom ⊢ ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) = ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ↔ ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
106 104 105 bitrdi ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) − ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ↔ ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) ) )
107 85 106 bitr4d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑇 ‘ 𝑖 ) = ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) ↔ ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) − ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) )
108 73 74 77 79 add4d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
109 65 72 76 adddid ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) ) )
110 63 72 78 adddid ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) = ( ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) )
111 109 110 oveq12d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) ) = ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) ) + ( ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
112 108 111 eqtr4d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) ) )
113 112 oveq1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) = ( ( ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) )
114 72 76 addcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ∈ ℂ )
115 65 114 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) ∈ ℂ )
116 72 78 addcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ∈ ℂ )
117 63 116 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) ∈ ℂ )
118 115 117 68 83 divdird ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) = ( ( ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) / 𝑃 ) + ( ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) / 𝑃 ) ) )
119 65 114 68 83 divassd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) / 𝑃 ) = ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) )
120 63 116 68 83 divassd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) / 𝑃 ) = ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) )
121 119 120 oveq12d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑄 ) · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) / 𝑃 ) + ( ( 𝑄 · ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) / 𝑃 ) ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) )
122 113 118 121 3eqtrd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) )
123 122 eqeq2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝑇 ‘ 𝑖 ) = ( ( ( ( ( 1 − 𝑄 ) · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝑄 · ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) ) + ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) / 𝑃 ) ↔ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
124 68 82 mulcld ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ∈ ℂ )
125 80 100 124 subaddd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) − ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) ) = ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ↔ ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) )
126 107 123 125 3bitr3rd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ↔ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
127 126 biimpd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) → ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
128 npncan2 ⊢ ( ( 1 ∈ ℂ ∧ 𝑃 ∈ ℂ ) → ( ( 1 − 𝑃 ) + ( 𝑃 − 1 ) ) = 0 )
129 59 68 128 sylancr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 1 − 𝑃 ) + ( 𝑃 − 1 ) ) = 0 )
130 129 oveq1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑃 ) + ( 𝑃 − 1 ) ) · ( 𝐴 ‘ 𝑖 ) ) = ( 0 · ( 𝐴 ‘ 𝑖 ) ) )
131 90 70 71 adddird ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑃 ) + ( 𝑃 − 1 ) ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) )
132 mul02 ⊢ ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ → ( 0 · ( 𝐴 ‘ 𝑖 ) ) = 0 )
133 132 ad3antrrr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 0 · ( 𝐴 ‘ 𝑖 ) ) = 0 )
134 130 131 133 3eqtr3d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) = 0 )
135 134 oveq1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐵 ‘ 𝑖 ) ) = ( 0 + ( 𝐵 ‘ 𝑖 ) ) )
136 100 72 76 addassd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐵 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) )
137 76 addid2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 0 + ( 𝐵 ‘ 𝑖 ) ) = ( 𝐵 ‘ 𝑖 ) )
138 135 136 137 3eqtr3rd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) )
139 114 68 83 divcan2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) = ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) )
140 139 oveq2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) ) )
141 138 140 eqtr4d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) )
142 134 oveq1d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐶 ‘ 𝑖 ) ) = ( 0 + ( 𝐶 ‘ 𝑖 ) ) )
143 100 72 78 addassd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) ) + ( 𝐶 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) )
144 78 addid2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 0 + ( 𝐶 ‘ 𝑖 ) ) = ( 𝐶 ‘ 𝑖 ) )
145 142 143 144 3eqtr3rd ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) )
146 116 68 83 divcan2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) = ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) )
147 146 oveq2d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) ) )
148 145 147 eqtr4d ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) )
149 141 148 jca ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
150 127 149 jctild ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
151 df-3an ⊢ ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ↔ ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
152 150 151 syl6ibr ⊢ ( ( ( ( ( 𝐴 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝐵 ‘ 𝑖 ) ∈ ℂ ) ∧ ( ( 𝐶 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑇 ‘ 𝑖 ) ∈ ℂ ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
153 57 152 sylan ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
154 153 an32s ⊢ ( ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
155 154 ralimdva ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
156 155 3impia ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
157 fveq1 ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ‘ 𝑖 ) )
158 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑖 ) )
159 158 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) = ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) )
160 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑖 ) )
161 159 160 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) = ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) )
162 161 oveq1d ⊢ ( 𝑘 = 𝑖 → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) )
163 eqid ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) )
164 ovex ⊢ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ∈ V
165 162 163 164 fvmpt ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) )
166 157 165 sylan9eq ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) )
167 oveq2 ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) → ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) )
168 167 oveq2d ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) → ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) )
169 168 eqeq2d ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
170 oveq2 ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) → ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) )
171 170 oveq1d ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) → ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) )
172 171 eqeq2d ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) → ( ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
173 169 172 3anbi13d ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
174 166 173 syl ⊢ ( ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
175 174 ralbidva ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
176 fveq1 ⊢ ( 𝑦 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) → ( 𝑦 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ‘ 𝑖 ) )
177 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐶 ‘ 𝑘 ) = ( 𝐶 ‘ 𝑖 ) )
178 159 177 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) = ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) )
179 178 oveq1d ⊢ ( 𝑘 = 𝑖 → ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) )
180 eqid ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) )
181 ovex ⊢ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ∈ V
182 179 180 181 fvmpt ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) )
183 176 182 sylan9eq ⊢ ( ( 𝑦 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) )
184 oveq2 ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) → ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) = ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) )
185 184 oveq2d ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) → ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) )
186 185 eqeq2d ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) → ( ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
187 oveq2 ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) → ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) = ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) )
188 187 oveq2d ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) → ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) )
189 188 eqeq2d ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) → ( ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) )
190 186 189 3anbi23d ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
191 183 190 syl ⊢ ( ( 𝑦 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
192 191 ralbidva ⊢ ( 𝑦 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) )
193 175 192 rspc2ev ⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐵 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑘 ) ) + ( 𝐶 ‘ 𝑘 ) ) / 𝑃 ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐵 ‘ 𝑖 ) ) / 𝑃 ) ) + ( 𝑄 · ( ( ( ( 𝑃 − 1 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝐶 ‘ 𝑖 ) ) / 𝑃 ) ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
194 35 45 156 193 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
195 oveq2 ⊢ ( 𝑟 = 𝑃 → ( 1 − 𝑟 ) = ( 1 − 𝑃 ) )
196 195 oveq1d ⊢ ( 𝑟 = 𝑃 → ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) )
197 oveq1 ⊢ ( 𝑟 = 𝑃 → ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) )
198 196 197 oveq12d ⊢ ( 𝑟 = 𝑃 → ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) )
199 198 eqeq2d ⊢ ( 𝑟 = 𝑃 → ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
200 199 3anbi1d ⊢ ( 𝑟 = 𝑃 → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
201 200 ralbidv ⊢ ( 𝑟 = 𝑃 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
202 201 2rexbidv ⊢ ( 𝑟 = 𝑃 → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
203 oveq2 ⊢ ( 𝑠 = 𝑃 → ( 1 − 𝑠 ) = ( 1 − 𝑃 ) )
204 203 oveq1d ⊢ ( 𝑠 = 𝑃 → ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) = ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) )
205 oveq1 ⊢ ( 𝑠 = 𝑃 → ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) = ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) )
206 204 205 oveq12d ⊢ ( 𝑠 = 𝑃 → ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) )
207 206 eqeq2d ⊢ ( 𝑠 = 𝑃 → ( ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
208 207 3anbi2d ⊢ ( 𝑠 = 𝑃 → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
209 208 ralbidv ⊢ ( 𝑠 = 𝑃 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
210 209 2rexbidv ⊢ ( 𝑠 = 𝑃 → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
211 oveq2 ⊢ ( 𝑢 = 𝑄 → ( 1 − 𝑢 ) = ( 1 − 𝑄 ) )
212 211 oveq1d ⊢ ( 𝑢 = 𝑄 → ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) )
213 oveq1 ⊢ ( 𝑢 = 𝑄 → ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) = ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) )
214 212 213 oveq12d ⊢ ( 𝑢 = 𝑄 → ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) )
215 214 eqeq2d ⊢ ( 𝑢 = 𝑄 → ( ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
216 215 3anbi3d ⊢ ( 𝑢 = 𝑄 → ( ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
217 216 ralbidv ⊢ ( 𝑢 = 𝑄 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
218 217 2rexbidv ⊢ ( 𝑢 = 𝑄 → ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) )
219 202 210 218 rspc3ev ⊢ ( ( ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ) ∧ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑄 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝑦 ‘ 𝑖 ) ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
220 1 1 2 194 219 syl31anc ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
221 rexcom ⊢ ( ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
222 221 rexbii ⊢ ( ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
223 rexcom ⊢ ( ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
224 222 223 bitri ⊢ ( ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
225 224 rexbii ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
226 rexcom ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
227 rexcom ⊢ ( ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
228 227 rexbii ⊢ ( ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
229 rexcom ⊢ ( ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
230 228 229 bitri ⊢ ( ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
231 230 rexbii ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
232 rexcom ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
233 231 232 bitri ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
234 233 rexbii ⊢ ( ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
235 225 226 234 3bitri ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
236 220 235 sylib ⊢ ( ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑇 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑃 ∈ ( 0 [,] 1 ) ∧ 𝑄 ∈ ( 0 [,] 1 ) ∧ 𝑃 ≠ 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑃 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑃 · ( 𝑇 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑄 ) · ( 𝐵 ‘ 𝑖 ) ) + ( 𝑄 · ( 𝐶 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ∃ 𝑟 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∃ 𝑢 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝐵 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ ( 𝐶 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝐴 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑦 ‘ 𝑖 ) ) ) ∧ ( 𝑇 ‘ 𝑖 ) = ( ( ( 1 − 𝑢 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑢 · ( 𝑦 ‘ 𝑖 ) ) ) ) )