Metamath Proof Explorer

Theorem eenglngeehlnmlem2

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

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

Proof

Step Hyp Ref Expression
1 0red ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → 0 ∈ ℝ )
2 1red ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → 1 ∈ ℝ )
3 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
4 reorelicc ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 𝑡 < 0 ∨ 𝑡 ∈ ( 0 [,] 1 ) ∨ 1 < 𝑡 ) )
5 1 2 3 4 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( 𝑡 < 0 ∨ 𝑡 ∈ ( 0 [,] 1 ) ∨ 1 < 𝑡 ) )
6 0xr ⊢ 0 ∈ ℝ*
7 6 a1i ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → 0 ∈ ℝ* )
8 1xr ⊢ 1 ∈ ℝ*
9 8 a1i ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → 1 ∈ ℝ* )
10 simpl ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 ∈ ℝ )
11 10 recnd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 ∈ ℂ )
12 0red ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 0 ∈ ℝ )
13 1red ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 1 ∈ ℝ )
14 simpr ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 < 0 )
15 0lt1 ⊢ 0 < 1
16 15 a1i ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 0 < 1 )
17 10 12 13 14 16 lttrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 < 1 )
18 10 17 ltned ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 ≠ 1 )
19 1subrec1sub ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 1 ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) = ( 𝑡 / ( 𝑡 − 1 ) ) )
20 11 18 19 syl2anc ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) = ( 𝑡 / ( 𝑡 − 1 ) ) )
21 10 13 resubcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − 1 ) ∈ ℝ )
22 1cnd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 1 ∈ ℂ )
23 11 22 18 subne0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − 1 ) ≠ 0 )
24 10 21 23 redivcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 / ( 𝑡 − 1 ) ) ∈ ℝ )
25 24 rexrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 / ( 𝑡 − 1 ) ) ∈ ℝ* )
26 20 25 eqeltrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ∈ ℝ* )
27 26 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ∈ ℝ* )
28 10 renegcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → - 𝑡 ∈ ℝ )
29 10 13 sublt0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − 1 ) < 0 ↔ 𝑡 < 1 ) )
30 17 29 mpbird ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − 1 ) < 0 )
31 21 30 negelrpd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → - ( 𝑡 − 1 ) ∈ ℝ+ )
32 10 12 14 ltled ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 ≤ 0 )
33 10 le0neg1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 ≤ 0 ↔ 0 ≤ - 𝑡 ) )
34 32 33 mpbid ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 0 ≤ - 𝑡 )
35 28 31 34 divge0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 0 ≤ ( - 𝑡 / - ( 𝑡 − 1 ) ) )
36 21 recnd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − 1 ) ∈ ℂ )
37 11 36 23 div2negd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( - 𝑡 / - ( 𝑡 − 1 ) ) = ( 𝑡 / ( 𝑡 − 1 ) ) )
38 20 37 eqtr4d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) = ( - 𝑡 / - ( 𝑡 − 1 ) ) )
39 35 38 breqtrrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 0 ≤ ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) )
40 39 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → 0 ≤ ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) )
41 1red ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → 1 ∈ ℝ )
42 13 10 resubcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − 𝑡 ) ∈ ℝ )
43 10 13 posdifd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 < 1 ↔ 0 < ( 1 − 𝑡 ) ) )
44 17 43 mpbid ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 0 < ( 1 − 𝑡 ) )
45 42 44 elrpd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − 𝑡 ) ∈ ℝ+ )
46 45 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 1 − 𝑡 ) ∈ ℝ+ )
47 46 rpreccld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 1 / ( 1 − 𝑡 ) ) ∈ ℝ+ )
48 41 47 ltsubrpd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) < 1 )
49 7 9 27 40 48 elicod ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ∈ ( 0 [,) 1 ) )
50 oveq2 ⊢ ( 𝑙 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) → ( 1 − 𝑙 ) = ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) )
51 50 oveq1d ⊢ ( 𝑙 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) → ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) )
52 oveq1 ⊢ ( 𝑙 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) → ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) = ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) )
53 51 52 oveq12d ⊢ ( 𝑙 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) → ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
54 53 eqeq2d ⊢ ( 𝑙 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
55 54 ralbidv ⊢ ( 𝑙 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
56 55 adantl ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑙 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
57 22 11 subcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − 𝑡 ) ∈ ℂ )
58 10 17 gtned ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 1 ≠ 𝑡 )
59 22 11 58 subne0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − 𝑡 ) ≠ 0 )
60 57 59 reccld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 / ( 1 − 𝑡 ) ) ∈ ℂ )
61 22 60 nncand ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) = ( 1 / ( 1 − 𝑡 ) ) )
62 61 60 eqeltrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ∈ ℂ )
63 22 60 subcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ∈ ℂ )
64 16 gt0ne0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 1 ≠ 0 )
65 36 11 subeq0ad ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 − 1 ) − 𝑡 ) = 0 ↔ ( 𝑡 − 1 ) = 𝑡 ) )
66 11 22 11 sub32d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − 1 ) − 𝑡 ) = ( ( 𝑡 − 𝑡 ) − 1 ) )
67 66 eqeq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 − 1 ) − 𝑡 ) = 0 ↔ ( ( 𝑡 − 𝑡 ) − 1 ) = 0 ) )
68 11 subidd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − 𝑡 ) = 0 )
69 68 oveq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − 𝑡 ) − 1 ) = ( 0 − 1 ) )
70 69 eqeq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 − 𝑡 ) − 1 ) = 0 ↔ ( 0 − 1 ) = 0 ) )
71 0cnd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 0 ∈ ℂ )
72 71 22 71 subaddd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 0 − 1 ) = 0 ↔ ( 1 + 0 ) = 0 ) )
73 22 addid1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 + 0 ) = 1 )
74 73 eqeq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 1 + 0 ) = 0 ↔ 1 = 0 ) )
75 72 74 bitrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 0 − 1 ) = 0 ↔ 1 = 0 ) )
76 67 70 75 3bitrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 − 1 ) − 𝑡 ) = 0 ↔ 1 = 0 ) )
77 65 76 bitr3d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − 1 ) = 𝑡 ↔ 1 = 0 ) )
78 77 necon3bid ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − 1 ) ≠ 𝑡 ↔ 1 ≠ 0 ) )
79 64 78 mpbird ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − 1 ) ≠ 𝑡 )
80 20 eqeq2d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ↔ 1 = ( 𝑡 / ( 𝑡 − 1 ) ) ) )
81 eqcom ⊢ ( 1 = ( 𝑡 / ( 𝑡 − 1 ) ) ↔ ( 𝑡 / ( 𝑡 − 1 ) ) = 1 )
82 11 36 22 23 divmuld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 / ( 𝑡 − 1 ) ) = 1 ↔ ( ( 𝑡 − 1 ) · 1 ) = 𝑡 ) )
83 81 82 syl5bb ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 = ( 𝑡 / ( 𝑡 − 1 ) ) ↔ ( ( 𝑡 − 1 ) · 1 ) = 𝑡 ) )
84 36 mulid1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − 1 ) · 1 ) = ( 𝑡 − 1 ) )
85 84 eqeq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 − 1 ) · 1 ) = 𝑡 ↔ ( 𝑡 − 1 ) = 𝑡 ) )
86 80 83 85 3bitrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 = ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ↔ ( 𝑡 − 1 ) = 𝑡 ) )
87 86 necon3bid ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 ≠ ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ↔ ( 𝑡 − 1 ) ≠ 𝑡 ) )
88 79 87 mpbird ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 1 ≠ ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) )
89 22 63 88 subne0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ≠ 0 )
90 61 oveq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 1 − 𝑡 ) ) = ( ( 1 / ( 1 − 𝑡 ) ) · ( 1 − 𝑡 ) ) )
91 57 59 recid2d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 1 / ( 1 − 𝑡 ) ) · ( 1 − 𝑡 ) ) = 1 )
92 90 91 eqtrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 1 − 𝑡 ) ) = 1 )
93 62 57 89 92 mvllmuld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − 𝑡 ) = ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) )
94 93 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) = ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) )
95 94 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) )
96 20 oveq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) = ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) )
97 20 96 oveq12d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) = ( ( 𝑡 / ( 𝑡 − 1 ) ) / ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) ) )
98 subdivcomb2 ⊢ ( ( 𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( 𝑡 − 1 ) ∈ ℂ ∧ ( 𝑡 − 1 ) ≠ 0 ) ) → ( ( 𝑡 − ( ( 𝑡 − 1 ) · 1 ) ) / ( 𝑡 − 1 ) ) = ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) )
99 11 22 36 23 98 syl112anc ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − ( ( 𝑡 − 1 ) · 1 ) ) / ( 𝑡 − 1 ) ) = ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) )
100 84 oveq2d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − ( ( 𝑡 − 1 ) · 1 ) ) = ( 𝑡 − ( 𝑡 − 1 ) ) )
101 11 22 nncand ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − ( 𝑡 − 1 ) ) = 1 )
102 100 101 eqtrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 − ( ( 𝑡 − 1 ) · 1 ) ) = 1 )
103 102 oveq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 − ( ( 𝑡 − 1 ) · 1 ) ) / ( 𝑡 − 1 ) ) = ( 1 / ( 𝑡 − 1 ) ) )
104 99 103 eqtr3d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) = ( 1 / ( 𝑡 − 1 ) ) )
105 104 oveq1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) · 𝑡 ) = ( ( 1 / ( 𝑡 − 1 ) ) · 𝑡 ) )
106 11 36 23 divrec2d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 / ( 𝑡 − 1 ) ) = ( ( 1 / ( 𝑡 − 1 ) ) · 𝑡 ) )
107 105 106 eqtr4d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) · 𝑡 ) = ( 𝑡 / ( 𝑡 − 1 ) ) )
108 20 63 eqeltrrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 / ( 𝑡 − 1 ) ) ∈ ℂ )
109 108 22 subcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) ∈ ℂ )
110 79 necomd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 ≠ ( 𝑡 − 1 ) )
111 11 36 23 110 divne1d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 𝑡 / ( 𝑡 − 1 ) ) ≠ 1 )
112 108 22 111 subne0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) ≠ 0 )
113 108 109 11 112 divmuld ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( ( 𝑡 / ( 𝑡 − 1 ) ) / ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) ) = 𝑡 ↔ ( ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) · 𝑡 ) = ( 𝑡 / ( 𝑡 − 1 ) ) ) )
114 107 113 mpbird ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 𝑡 / ( 𝑡 − 1 ) ) / ( ( 𝑡 / ( 𝑡 − 1 ) ) − 1 ) ) = 𝑡 )
115 97 114 eqtr2d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → 𝑡 = ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) )
116 115 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 = ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) )
117 116 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) = ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
118 95 117 oveq12d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
119 118 eqeq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
120 119 biimpd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
121 eqcom ⊢ ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( 𝑥 ‘ 𝑖 ) )
122 elmapi ⊢ ( 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
123 122 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
124 123 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
125 124 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
126 125 ffvelrnda ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℝ )
127 126 recnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
128 1cnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
129 11 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
130 128 129 subcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
131 58 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 1 ≠ 𝑡 )
132 128 129 131 subne0d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) ≠ 0 )
133 130 132 reccld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / ( 1 − 𝑡 ) ) ∈ ℂ )
134 128 133 subcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ∈ ℂ )
135 eldifi ⊢ ( 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) → 𝑦 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) )
136 elmapi ⊢ ( 𝑦 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
137 135 136 syl ⊢ ( 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
138 137 3ad2ant3 ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
139 138 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
140 139 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
141 140 ffvelrnda ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℝ )
142 141 recnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℂ )
143 134 142 mulcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ∈ ℂ )
144 62 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ∈ ℂ )
145 elmapi ⊢ ( 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ )
146 145 adantl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ )
147 146 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ )
148 147 ffvelrnda ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℝ )
149 148 recnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℂ )
150 144 149 mulcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) ∈ ℂ )
151 127 143 150 subadd2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( 𝑥 ‘ 𝑖 ) ) )
152 121 151 bitr4id ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) ) )
153 eqcom ⊢ ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
154 127 143 subcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ∈ ℂ )
155 89 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ≠ 0 )
156 154 144 149 155 divmuld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
157 eqcom ⊢ ( ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) )
158 127 143 144 155 divsubdird ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( ( ( 𝑥 ‘ 𝑖 ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) − ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) ) )
159 127 144 155 divcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) ∈ ℂ )
160 143 144 155 divcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) ∈ ℂ )
161 159 160 negsubd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) + - ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) ) = ( ( ( 𝑥 ‘ 𝑖 ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) − ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) ) )
162 127 144 155 divrec2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) )
163 143 144 155 divneg2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / - ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) )
164 128 134 negsubdi2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) = ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) )
165 164 oveq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / - ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) )
166 134 128 subcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ∈ ℂ )
167 88 necomd ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ≠ 1 )
168 63 22 167 subne0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 𝑡 < 0 ) → ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ≠ 0 )
169 168 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ≠ 0 )
170 134 142 166 169 div23d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) = ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
171 163 165 170 3eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
172 162 171 oveq12d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) + - ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
173 158 161 172 3eqtr2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
174 173 eqeq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
175 157 174 syl5bb ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
176 156 175 bitr3d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
177 153 176 syl5bb ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) − ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
178 152 177 bitrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 / ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) / ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) − 1 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
179 120 178 sylibrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
180 179 ralimdva ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
181 180 imp ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) ) · ( 𝑝 ‘ 𝑖 ) ) + ( ( 1 − ( 1 / ( 1 − 𝑡 ) ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
182 49 56 181 rspcedvd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) )
183 182 3mix2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑡 < 0 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) )
184 183 exp31 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( 𝑡 < 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) )
185 184 com23 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( 𝑡 < 0 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) )
186 185 imp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 𝑡 < 0 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) )
187 simpr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
188 oveq2 ⊢ ( 𝑘 = 𝑡 → ( 1 − 𝑘 ) = ( 1 − 𝑡 ) )
189 188 oveq1d ⊢ ( 𝑘 = 𝑡 → ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) )
190 oveq1 ⊢ ( 𝑘 = 𝑡 → ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) )
191 189 190 oveq12d ⊢ ( 𝑘 = 𝑡 → ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) )
192 191 eqeq2d ⊢ ( 𝑘 = 𝑡 → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
193 192 ralbidv ⊢ ( 𝑘 = 𝑡 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
194 193 adantl ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ∧ 𝑘 = 𝑡 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) )
195 simplr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) )
196 187 194 195 rspcedvd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) )
197 196 3mix1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) )
198 197 ex ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 𝑡 ∈ ( 0 [,] 1 ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) )
199 1red ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 1 ∈ ℝ )
200 simpl ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 𝑡 ∈ ℝ )
201 0red ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 0 ∈ ℝ )
202 15 a1i ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 0 < 1 )
203 simpr ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 1 < 𝑡 )
204 201 199 200 202 203 lttrd ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 0 < 𝑡 )
205 204 gt0ne0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 𝑡 ≠ 0 )
206 199 200 205 redivcld ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → ( 1 / 𝑡 ) ∈ ℝ )
207 200 204 recgt0d ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → 0 < ( 1 / 𝑡 ) )
208 recgt1i ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → ( 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) < 1 ) )
209 206 adantr ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) ∧ ( 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) < 1 ) ) → ( 1 / 𝑡 ) ∈ ℝ )
210 1red ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) ∧ ( 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) < 1 ) ) → 1 ∈ ℝ )
211 simprr ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) ∧ ( 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) < 1 ) ) → ( 1 / 𝑡 ) < 1 )
212 209 210 211 ltled ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) ∧ ( 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) < 1 ) ) → ( 1 / 𝑡 ) ≤ 1 )
213 208 212 mpdan ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → ( 1 / 𝑡 ) ≤ 1 )
214 206 207 213 3jca ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → ( ( 1 / 𝑡 ) ∈ ℝ ∧ 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) ≤ 1 ) )
215 1re ⊢ 1 ∈ ℝ
216 6 215 pm3.2i ⊢ ( 0 ∈ ℝ* ∧ 1 ∈ ℝ )
217 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 1 ∈ ℝ ) → ( ( 1 / 𝑡 ) ∈ ( 0 (,] 1 ) ↔ ( ( 1 / 𝑡 ) ∈ ℝ ∧ 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) ≤ 1 ) ) )
218 216 217 mp1i ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → ( ( 1 / 𝑡 ) ∈ ( 0 (,] 1 ) ↔ ( ( 1 / 𝑡 ) ∈ ℝ ∧ 0 < ( 1 / 𝑡 ) ∧ ( 1 / 𝑡 ) ≤ 1 ) ) )
219 214 218 mpbird ⊢ ( ( 𝑡 ∈ ℝ ∧ 1 < 𝑡 ) → ( 1 / 𝑡 ) ∈ ( 0 (,] 1 ) )
220 219 ad4ant23 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 1 / 𝑡 ) ∈ ( 0 (,] 1 ) )
221 oveq2 ⊢ ( 𝑚 = ( 1 / 𝑡 ) → ( 1 − 𝑚 ) = ( 1 − ( 1 / 𝑡 ) ) )
222 221 oveq1d ⊢ ( 𝑚 = ( 1 / 𝑡 ) → ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
223 oveq1 ⊢ ( 𝑚 = ( 1 / 𝑡 ) → ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) = ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) )
224 222 223 oveq12d ⊢ ( 𝑚 = ( 1 / 𝑡 ) → ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) )
225 224 eqeq2d ⊢ ( 𝑚 = ( 1 / 𝑡 ) → ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ) )
226 225 ralbidv ⊢ ( 𝑚 = ( 1 / 𝑡 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ) )
227 226 adantl ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) ∧ 𝑚 = ( 1 / 𝑡 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ) )
228 simplr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → 𝑡 ∈ ℝ )
229 228 recnd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → 𝑡 ∈ ℂ )
230 229 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
231 204 ex ⊢ ( 𝑡 ∈ ℝ → ( 1 < 𝑡 → 0 < 𝑡 ) )
232 gt0ne0 ⊢ ( ( 𝑡 ∈ ℝ ∧ 0 < 𝑡 ) → 𝑡 ≠ 0 )
233 232 ex ⊢ ( 𝑡 ∈ ℝ → ( 0 < 𝑡 → 𝑡 ≠ 0 ) )
234 231 233 syld ⊢ ( 𝑡 ∈ ℝ → ( 1 < 𝑡 → 𝑡 ≠ 0 ) )
235 234 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( 1 < 𝑡 → 𝑡 ≠ 0 ) )
236 235 imp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → 𝑡 ≠ 0 )
237 236 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ≠ 0 )
238 230 237 reccld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑡 ) ∈ ℂ )
239 1cnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ℂ )
240 230 237 recne0d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / 𝑡 ) ≠ 0 )
241 238 239 238 240 divsubdird ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) = ( ( ( 1 / 𝑡 ) / ( 1 / 𝑡 ) ) − ( 1 / ( 1 / 𝑡 ) ) ) )
242 238 240 dividd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 / 𝑡 ) / ( 1 / 𝑡 ) ) = 1 )
243 230 237 recrecd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / ( 1 / 𝑡 ) ) = 𝑡 )
244 242 243 oveq12d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / 𝑡 ) / ( 1 / 𝑡 ) ) − ( 1 / ( 1 / 𝑡 ) ) ) = ( 1 − 𝑡 ) )
245 241 244 eqtr2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − 𝑡 ) = ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) )
246 245 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
247 229 236 recrecd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → ( 1 / ( 1 / 𝑡 ) ) = 𝑡 )
248 247 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → 𝑡 = ( 1 / ( 1 / 𝑡 ) ) )
249 248 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 = ( 1 / ( 1 / 𝑡 ) ) )
250 249 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) = ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
251 246 250 oveq12d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
252 251 eqeq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
253 252 biimpd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
254 eqcom ⊢ ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) = ( 𝑦 ‘ 𝑖 ) )
255 139 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → 𝑦 : ( 1 ... 𝑁 ) ⟶ ℝ )
256 255 ffvelrnda ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℝ )
257 256 recnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑦 ‘ 𝑖 ) ∈ ℂ )
258 239 238 subcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 − ( 1 / 𝑡 ) ) ∈ ℂ )
259 124 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → 𝑥 : ( 1 ... 𝑁 ) ⟶ ℝ )
260 259 ffvelrnda ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℝ )
261 260 recnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
262 258 261 mulcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
263 146 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → 𝑝 : ( 1 ... 𝑁 ) ⟶ ℝ )
264 263 ffvelrnda ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℝ )
265 264 recnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑝 ‘ 𝑖 ) ∈ ℂ )
266 238 265 mulcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ∈ ℂ )
267 257 262 266 subaddd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) = ( 𝑦 ‘ 𝑖 ) ) )
268 254 267 bitr4id ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) )
269 eqcom ⊢ ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) )
270 257 262 subcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) ∈ ℂ )
271 270 238 265 240 divmuld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) = ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) ) )
272 269 271 bitr4id ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ↔ ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) = ( 𝑝 ‘ 𝑖 ) ) )
273 eqcom ⊢ ( ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) )
274 257 262 238 240 divsubdird ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) = ( ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) − ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) ) )
275 257 238 240 divcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) ∈ ℂ )
276 262 238 240 divcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) ∈ ℂ )
277 275 276 negsubd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) + - ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) ) = ( ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) − ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) ) )
278 262 238 240 divnegd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) = ( - ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) )
279 258 261 mulneg1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) = - ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
280 279 eqcomd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) = ( - ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
281 280 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) = ( ( - ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) )
282 239 238 negsubdi2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( 1 − ( 1 / 𝑡 ) ) = ( ( 1 / 𝑡 ) − 1 ) )
283 282 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( - ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( ( 1 / 𝑡 ) − 1 ) · ( 𝑥 ‘ 𝑖 ) ) )
284 283 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( - ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) = ( ( ( ( 1 / 𝑡 ) − 1 ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) )
285 238 239 subcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 / 𝑡 ) − 1 ) ∈ ℂ )
286 285 261 238 240 div23d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 / 𝑡 ) − 1 ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) = ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
287 284 286 eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( - ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) = ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
288 278 281 287 3eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → - ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) = ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) )
289 288 oveq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) + - ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) ) = ( ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) + ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) )
290 257 238 240 divrec2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) = ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) )
291 290 oveq1d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) + ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) )
292 238 240 reccld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 1 / ( 1 / 𝑡 ) ) ∈ ℂ )
293 292 257 mulcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ∈ ℂ )
294 285 238 240 divcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) ∈ ℂ )
295 294 261 mulcld ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
296 293 295 addcomd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) + ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
297 289 291 296 3eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) / ( 1 / 𝑡 ) ) + - ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) / ( 1 / 𝑡 ) ) ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
298 274 277 297 3eqtr2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) )
299 298 eqeq2d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
300 273 299 syl5bb ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝑦 ‘ 𝑖 ) − ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) ) / ( 1 / 𝑡 ) ) = ( 𝑝 ‘ 𝑖 ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
301 268 272 300 3bitrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( 𝑝 ‘ 𝑖 ) = ( ( ( ( ( 1 / 𝑡 ) − 1 ) / ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / ( 1 / 𝑡 ) ) · ( 𝑦 ‘ 𝑖 ) ) ) ) )
302 253 301 sylibrd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ) )
303 302 ralimdva ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) ) )
304 303 imp ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑥 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( 𝑝 ‘ 𝑖 ) ) ) )
305 220 227 304 rspcedvd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) )
306 305 3mix3d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ 1 < 𝑡 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) )
307 306 exp31 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( 1 < 𝑡 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) )
308 307 com23 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( 1 < 𝑡 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) )
309 308 imp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( 1 < 𝑡 → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) )
310 186 198 309 3jaod ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) ) → ( ( 𝑡 < 0 ∨ 𝑡 ∈ ( 0 [,] 1 ) ∨ 1 < 𝑡 ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) )
311 310 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ( 𝑡 < 0 ∨ 𝑡 ∈ ( 0 [,] 1 ) ∨ 1 < 𝑡 ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) ) )
312 5 311 mpid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ℝ ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) )
313 312 rexlimdva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑥 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ∧ 𝑦 ∈ ( ( ℝ ↑m ( 1 ... 𝑁 ) ) ∖ { 𝑥 } ) ) ∧ 𝑝 ∈ ( ℝ ↑m ( 1 ... 𝑁 ) ) ) → ( ∃ 𝑡 ∈ ℝ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑦 ‘ 𝑖 ) ) ) → ( ∃ 𝑘 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑘 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑘 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑙 ∈ ( 0 [,) 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑙 ) · ( 𝑝 ‘ 𝑖 ) ) + ( 𝑙 · ( 𝑦 ‘ 𝑖 ) ) ) ∨ ∃ 𝑚 ∈ ( 0 (,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑚 ) · ( 𝑥 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝑝 ‘ 𝑖 ) ) ) ) ) )