Metamath Proof Explorer

Theorem eenglngeehlnmlem1

Description: Lemma 1 for eenglngeehlnm . (Contributed by AV, 15-Feb-2023)

Ref Expression
Assertion eenglngeehlnmlem1 ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑘 = 𝑡 → ( 1 − 𝑘 ) = ( 1 − 𝑡 ) )
2 1 oveq1d ⊢ ( 𝑘 = 𝑡 → ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) )
3 oveq1 ⊢ ( 𝑘 = 𝑡 → ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) )
4 2 3 oveq12d ⊢ ( 𝑘 = 𝑡 → ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) )
5 4 eqeq2d ⊢ ( 𝑘 = 𝑡 → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
6 5 ralbidv ⊢ ( 𝑘 = 𝑡 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
7 6 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) )
8 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
9 ssrexv ⊢ ( ( 0 [,] 1 ) ⊆ ℝ → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
10 8 9 mp1i ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
11 7 10 syl5bi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
12 0re ⊢ 0 ∈ ℝ
13 1xr ⊢ 1 ∈ ℝ*
14 elico2 ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ* ) → ( 𝑙 ∈ ( 0 [,) 1 ) ↔ ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) ) )
15 12 13 14 mp2an ⊢ ( 𝑙 ∈ ( 0 [,) 1 ) ↔ ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) )
16 simp1 ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → 𝑙 ∈ ℝ )
17 1red ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → 1 ∈ ℝ )
18 17 16 resubcld ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → ( 1 − 𝑙 ) ∈ ℝ )
19 1cnd ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → 1 ∈ ℂ )
20 16 recnd ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → 𝑙 ∈ ℂ )
21 ltne ⊢ ( ( 𝑙 ∈ ℝ ∧ 𝑙 < 1 ) → 1 ≠ 𝑙 )
22 21 3adant2 ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → 1 ≠ 𝑙 )
23 19 20 22 subne0d ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → ( 1 − 𝑙 ) ≠ 0 )
24 16 18 23 redivcld ⊢ ( ( 𝑙 ∈ ℝ ∧ 0 ≤ 𝑙 ∧ 𝑙 < 1 ) → ( 𝑙 / ( 1 − 𝑙 ) ) ∈ ℝ )
25 15 24 sylbi ⊢ ( 𝑙 ∈ ( 0 [,) 1 ) → ( 𝑙 / ( 1 − 𝑙 ) ) ∈ ℝ )
26 25 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 𝑙 / ( 1 − 𝑙 ) ) ∈ ℝ )
27 26 renegcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) → - ( 𝑙 / ( 1 − 𝑙 ) ) ∈ ℝ )
28 oveq2 ⊢ ( 𝑡 = - ( 𝑙 / ( 1 − 𝑙 ) ) → ( 1 − 𝑡 ) = ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) )
29 28 oveq1d ⊢ ( 𝑡 = - ( 𝑙 / ( 1 − 𝑙 ) ) → ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) )
30 oveq1 ⊢ ( 𝑡 = - ( 𝑙 / ( 1 − 𝑙 ) ) → ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) = ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
31 29 30 oveq12d ⊢ ( 𝑡 = - ( 𝑙 / ( 1 − 𝑙 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
32 31 eqeq2d ⊢ ( 𝑡 = - ( 𝑙 / ( 1 − 𝑙 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
33 32 ralbidv ⊢ ( 𝑡 = - ( 𝑙 / ( 1 − 𝑙 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
34 33 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑡 = - ( 𝑙 / ( 1 − 𝑙 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
35 eqcom ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( 𝑥 ‘ 𝑖 ) )
36 elmapi ⊢ ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
37 36 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
38 37 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
39 38 ffvelrnda ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℝ )
40 39 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
41 15 16 sylbi ⊢ ( 𝑙 ∈ ( 0 [,) 1 ) → 𝑙 ∈ ℝ )
42 41 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑙 ∈ ℝ )
43 42 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑙 ∈ ℂ )
44 eldifi ⊢ ( 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) → 𝑦 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
45 elmapi ⊢ ( 𝑦 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
46 44 45 syl ⊢ ( 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
47 46 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
48 47 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
49 48 ffvelrnda ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℝ )
50 49 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℂ )
51 43 50 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ∈ ℂ )
52 1cnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
53 52 43 subcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑙 ) ∈ ℂ )
54 elmapi ⊢ ( 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ )
55 54 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ )
56 55 ffvelrnda ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℝ )
57 56 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℂ )
58 53 57 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) ∈ ℂ )
59 40 51 58 subadd2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( 𝑥 ‘ 𝑖 ) ) )
60 35 59 bitr4id ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) ) )
61 eqcom ⊢ ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) )
62 40 51 subcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∈ ℂ )
63 15 22 sylbi ⊢ ( 𝑙 ∈ ( 0 [,) 1 ) → 1 ≠ 𝑙 )
64 63 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 1 ≠ 𝑙 )
65 52 43 64 subne0d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑙 ) ≠ 0 )
66 62 53 57 65 divmuld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
67 61 66 bitr4id ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) = ( 𝑝 ‘ 𝑖 ) ) )
68 eqcom ⊢ ( ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) )
69 40 51 53 65 divsubdird ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) = ( ( ( 𝑥 ‘ 𝑖 ) / ( 1 − 𝑙 ) ) − ( ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − 𝑙 ) ) ) )
70 40 53 65 divrec2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) / ( 1 − 𝑙 ) ) = ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
71 43 50 53 65 div23d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − 𝑙 ) ) = ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
72 70 71 oveq12d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) / ( 1 − 𝑙 ) ) − ( ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − 𝑙 ) ) ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
73 69 72 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
74 73 eqeq2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
75 68 74 syl5bb ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
76 43 53 65 divcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑙 / ( 1 − 𝑙 ) ) ∈ ℂ )
77 76 50 mulneg1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) = - ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
78 77 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) = ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
79 78 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) + - ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
80 53 65 reccld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / ( 1 − 𝑙 ) ) ∈ ℂ )
81 80 40 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
82 76 50 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ∈ ℂ )
83 81 82 negsubd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) + - ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
84 52 76 subnegd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) = ( 1 + ( 𝑙 / ( 1 − 𝑙 ) ) ) )
85 muldivdir ⊢ ( ( 1 ∈ ℂ ∧ 𝑙 ∈ ℂ ∧ ( ( 1 − 𝑙 ) ∈ ℂ ∧ ( 1 − 𝑙 ) ≠ 0 ) ) → ( ( ( ( 1 − 𝑙 ) · 1 ) + 𝑙 ) / ( 1 − 𝑙 ) ) = ( 1 + ( 𝑙 / ( 1 − 𝑙 ) ) ) )
86 52 43 53 65 85 syl112anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑙 ) · 1 ) + 𝑙 ) / ( 1 − 𝑙 ) ) = ( 1 + ( 𝑙 / ( 1 − 𝑙 ) ) ) )
87 53 mulid1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑙 ) · 1 ) = ( 1 − 𝑙 ) )
88 87 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑙 ) · 1 ) + 𝑙 ) = ( ( 1 − 𝑙 ) + 𝑙 ) )
89 52 43 npcand ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑙 ) + 𝑙 ) = 1 )
90 88 89 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑙 ) · 1 ) + 𝑙 ) = 1 )
91 90 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑙 ) · 1 ) + 𝑙 ) / ( 1 − 𝑙 ) ) = ( 1 / ( 1 − 𝑙 ) ) )
92 84 86 91 3eqtr2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) = ( 1 / ( 1 − 𝑙 ) ) )
93 92 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / ( 1 − 𝑙 ) ) = ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) )
94 93 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) )
95 94 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
96 79 83 95 3eqtr3d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
97 96 eqeq2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
98 97 biimpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − 𝑙 ) ) · ( 𝑥 ‘ 𝑖 ) ) − ( ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
99 75 98 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − 𝑙 ) ) = ( 𝑝 ‘ 𝑖 ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
100 67 99 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
101 60 100 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
102 101 ralimdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
103 102 imp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − - ( 𝑙 / ( 1 − 𝑙 ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( - ( 𝑙 / ( 1 − 𝑙 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
104 27 34 103 rspcedvd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑙 ∈ ( 0 [,) 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) )
105 104 rexlimdva2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
106 0xr ⊢ 0 ∈ ℝ*
107 1re ⊢ 1 ∈ ℝ
108 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( 𝑚 ∈ ( 0 (,] 1 ) ↔ ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) ) )
109 106 107 108 mp2an ⊢ ( 𝑚 ∈ ( 0 (,] 1 ) ↔ ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) )
110 simp1 ⊢ ( ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) → 𝑚 ∈ ℝ )
111 gt0ne0 ⊢ ( ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ) → 𝑚 ≠ 0 )
112 111 3adant3 ⊢ ( ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) → 𝑚 ≠ 0 )
113 110 112 rereccld ⊢ ( ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) → ( 1 / 𝑚 ) ∈ ℝ )
114 109 113 sylbi ⊢ ( 𝑚 ∈ ( 0 (,] 1 ) → ( 1 / 𝑚 ) ∈ ℝ )
115 114 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
116 oveq2 ⊢ ( 𝑡 = ( 1 / 𝑚 ) → ( 1 − 𝑡 ) = ( 1 − ( 1 / 𝑚 ) ) )
117 116 oveq1d ⊢ ( 𝑡 = ( 1 / 𝑚 ) → ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
118 oveq1 ⊢ ( 𝑡 = ( 1 / 𝑚 ) → ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) = ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) )
119 117 118 oveq12d ⊢ ( 𝑡 = ( 1 / 𝑚 ) → ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) )
120 119 eqeq2d ⊢ ( 𝑡 = ( 1 / 𝑚 ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
121 120 ralbidv ⊢ ( 𝑡 = ( 1 / 𝑚 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
122 121 adantl ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ∧ 𝑡 = ( 1 / 𝑚 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
123 eqcom ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) = ( 𝑦 ‘ 𝑖 ) )
124 47 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
125 124 ffvelrnda ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℝ )
126 125 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℂ )
127 1cnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
128 109 110 sylbi ⊢ ( 𝑚 ∈ ( 0 (,] 1 ) → 𝑚 ∈ ℝ )
129 128 recnd ⊢ ( 𝑚 ∈ ( 0 (,] 1 ) → 𝑚 ∈ ℂ )
130 129 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑚 ∈ ℂ )
131 127 130 subcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑚 ) ∈ ℂ )
132 37 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
133 132 ffvelrnda ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℝ )
134 133 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
135 131 134 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
136 126 135 negsubd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) + - ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) ) )
137 131 134 mulneg1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) = - ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) )
138 127 130 negsubdi2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( 1 − 𝑚 ) = ( 𝑚 − 1 ) )
139 138 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) )
140 137 139 eqtr3d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) )
141 140 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) + - ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) )
142 136 141 eqtr3d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) )
143 142 eqeq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) )
144 54 ad2antlr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ )
145 144 ffvelrnda ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℝ )
146 145 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℂ )
147 130 146 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ∈ ℂ )
148 126 135 147 subaddd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) = ( 𝑦 ‘ 𝑖 ) ) )
149 eqcom ⊢ ( ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) )
150 149 a1i ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) ) )
151 130 127 subcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑚 − 1 ) ∈ ℂ )
152 151 134 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
153 126 152 addcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) ∈ ℂ )
154 elioc1 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( 𝑚 ∈ ( 0 (,] 1 ) ↔ ( 𝑚 ∈ ℝ* ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) ) )
155 106 13 154 mp2an ⊢ ( 𝑚 ∈ ( 0 (,] 1 ) ↔ ( 𝑚 ∈ ℝ* ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) )
156 12 a1i ⊢ ( 𝑚 ∈ ℝ* → 0 ∈ ℝ )
157 156 anim1i ⊢ ( ( 𝑚 ∈ ℝ* ∧ 0 < 𝑚 ) → ( 0 ∈ ℝ ∧ 0 < 𝑚 ) )
158 157 3adant3 ⊢ ( ( 𝑚 ∈ ℝ* ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) → ( 0 ∈ ℝ ∧ 0 < 𝑚 ) )
159 ltne ⊢ ( ( 0 ∈ ℝ ∧ 0 < 𝑚 ) → 𝑚 ≠ 0 )
160 158 159 syl ⊢ ( ( 𝑚 ∈ ℝ* ∧ 0 < 𝑚 ∧ 𝑚 ≤ 1 ) → 𝑚 ≠ 0 )
161 155 160 sylbi ⊢ ( 𝑚 ∈ ( 0 (,] 1 ) → 𝑚 ≠ 0 )
162 161 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑚 ≠ 0 )
163 153 146 130 162 divmul2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) = ( 𝑝 ‘ 𝑖 ) ↔ ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) )
164 126 152 130 162 divdird ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) = ( ( ( 𝑦 ‘ 𝑖 ) / 𝑚 ) + ( ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) / 𝑚 ) ) )
165 126 130 162 divrec2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) / 𝑚 ) = ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) )
166 151 134 130 162 div23d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) / 𝑚 ) = ( ( ( 𝑚 − 1 ) / 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) )
167 130 127 130 162 divsubdird ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑚 − 1 ) / 𝑚 ) = ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) )
168 167 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑚 − 1 ) / 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
169 166 168 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) / 𝑚 ) = ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
170 165 169 oveq12d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) / 𝑚 ) + ( ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) / 𝑚 ) ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) )
171 164 170 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) )
172 171 eqeq2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) / 𝑚 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) ) )
173 150 163 172 3bitr3d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) + ( ( 𝑚 − 1 ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) ) )
174 143 148 173 3bitr3d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) = ( 𝑦 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) ) )
175 123 174 syl5bb ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) ) )
176 130 162 reccld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑚 ) ∈ ℂ )
177 176 126 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ∈ ℂ )
178 127 176 subcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − ( 1 / 𝑚 ) ) ∈ ℂ )
179 178 134 mulcld ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
180 130 162 dividd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑚 / 𝑚 ) = 1 )
181 180 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) = ( 1 − ( 1 / 𝑚 ) ) )
182 181 oveq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
183 182 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) )
184 177 179 183 comraddd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) )
185 184 eqeq2d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
186 185 biimpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( 𝑚 / 𝑚 ) − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
187 175 186 sylbid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
188 187 ralimdva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
189 188 imp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑚 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑚 ) · ( 𝑦 ‘ 𝑖 ) ) ) )
190 115 122 189 rspcedvd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑚 ∈ ( 0 (,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) )
191 190 rexlimdva2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
192 11 105 191 3jaod ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )