Metamath Proof Explorer

Theorem axcontlem2

Description: Lemma for axcont . The idea here is to set up a mapping F that will allow to transfer dedekind to two sets of points. Here, we set up F and show its domain and codomain. (Contributed by Scott Fenton, 17-Jun-2013)

Ref Expression
Hypotheses axcontlem2.1 ⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
axcontlem2.2 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
Assertion axcontlem2 ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) )

Proof

Step Hyp Ref Expression
1 axcontlem2.1 ⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2 axcontlem2.2 ⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
3 opeq2 ⊢ ( 𝑝 = 𝑥 → ⟨ 𝑍 , 𝑝 ⟩ = ⟨ 𝑍 , 𝑥 ⟩ )
4 3 breq2d ⊢ ( 𝑝 = 𝑥 → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ↔ 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ) )
5 breq1 ⊢ ( 𝑝 = 𝑥 → ( 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
6 4 5 orbi12d ⊢ ( 𝑝 = 𝑥 → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ↔ ( 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
7 6 1 elrab2 ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
8 simpll3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
9 simpll2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
11 brbtwn ⊢ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
12 8 9 10 11 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
13 12 biimpa ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ) → ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) )
14 simp-4r ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) → 𝑍 ≠ 𝑈 )
15 oveq2 ⊢ ( 𝑠 = 0 → ( 1 − 𝑠 ) = ( 1 − 0 ) )
16 1m0e1 ⊢ ( 1 − 0 ) = 1
17 15 16 eqtrdi ⊢ ( 𝑠 = 0 → ( 1 − 𝑠 ) = 1 )
18 17 oveq1d ⊢ ( 𝑠 = 0 → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( 1 · ( 𝑍 ‘ 𝑖 ) ) )
19 oveq1 ⊢ ( 𝑠 = 0 → ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) = ( 0 · ( 𝑥 ‘ 𝑖 ) ) )
20 18 19 oveq12d ⊢ ( 𝑠 = 0 → ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) )
21 20 eqeq2d ⊢ ( 𝑠 = 0 → ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
22 21 ralbidv ⊢ ( 𝑠 = 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
23 22 biimpac ⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ 𝑠 = 0 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) )
24 eqcom ⊢ ( 𝑍 = 𝑈 ↔ 𝑈 = 𝑍 )
25 8 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
26 9 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
27 eqeefv ⊢ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑈 = 𝑍 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
28 25 26 27 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑈 = 𝑍 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
29 9 ad2antrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
30 fveecn ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
31 29 30 sylancom ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
32 fveecn ⊢ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
33 32 ad4ant24 ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
34 mullid ⊢ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝑍 ‘ 𝑖 ) ) = ( 𝑍 ‘ 𝑖 ) )
35 mul02 ⊢ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ → ( 0 · ( 𝑥 ‘ 𝑖 ) ) = 0 )
36 34 35 oveqan12d ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) = ( ( 𝑍 ‘ 𝑖 ) + 0 ) )
37 addrid ⊢ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ → ( ( 𝑍 ‘ 𝑖 ) + 0 ) = ( 𝑍 ‘ 𝑖 ) )
38 37 adantr ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝑍 ‘ 𝑖 ) + 0 ) = ( 𝑍 ‘ 𝑖 ) )
39 36 38 eqtrd ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) = ( 𝑍 ‘ 𝑖 ) )
40 39 eqeq2d ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑥 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝑈 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
41 31 33 40 syl2anc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ( 𝑈 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
42 41 ralbidva ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
43 28 42 bitr4d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑈 = 𝑍 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
44 24 43 bitrid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
45 23 44 imbitrrid ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ∧ 𝑠 = 0 ) → 𝑍 = 𝑈 ) )
46 45 expdimp ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) → ( 𝑠 = 0 → 𝑍 = 𝑈 ) )
47 46 necon3d ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) → ( 𝑍 ≠ 𝑈 → 𝑠 ≠ 0 ) )
48 14 47 mpd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) → 𝑠 ≠ 0 )
49 elicc01 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) ↔ ( 𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1 ) )
50 49 simp1bi ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → 𝑠 ∈ ℝ )
51 rereccl ⊢ ( ( 𝑠 ∈ ℝ ∧ 𝑠 ≠ 0 ) → ( 1 / 𝑠 ) ∈ ℝ )
52 50 51 sylan ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≠ 0 ) → ( 1 / 𝑠 ) ∈ ℝ )
53 50 adantr ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≠ 0 ) → 𝑠 ∈ ℝ )
54 49 simp2bi ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑠 )
55 54 adantr ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≠ 0 ) → 0 ≤ 𝑠 )
56 simpr ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≠ 0 ) → 𝑠 ≠ 0 )
57 53 55 56 ne0gt0d ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≠ 0 ) → 0 < 𝑠 )
58 1re ⊢ 1 ∈ ℝ
59 0le1 ⊢ 0 ≤ 1
60 divge0 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝑠 ∈ ℝ ∧ 0 < 𝑠 ) ) → 0 ≤ ( 1 / 𝑠 ) )
61 58 59 60 mpanl12 ⊢ ( ( 𝑠 ∈ ℝ ∧ 0 < 𝑠 ) → 0 ≤ ( 1 / 𝑠 ) )
62 53 57 61 syl2anc ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≠ 0 ) → 0 ≤ ( 1 / 𝑠 ) )
63 elrege0 ⊢ ( ( 1 / 𝑠 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 1 / 𝑠 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝑠 ) ) )
64 52 62 63 sylanbrc ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 𝑠 ≠ 0 ) → ( 1 / 𝑠 ) ∈ ( 0 [,) +∞ ) )
65 64 adantll ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) → ( 1 / 𝑠 ) ∈ ( 0 [,) +∞ ) )
66 50 ad3antlr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℝ )
67 66 recnd ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
68 simplr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ≠ 0 )
69 32 ad5ant25 ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
70 9 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
71 70 30 sylancom ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
72 ax-1cn ⊢ 1 ∈ ℂ
73 reccl ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( 1 / 𝑠 ) ∈ ℂ )
74 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 1 / 𝑠 ) ∈ ℂ ) → ( 1 − ( 1 / 𝑠 ) ) ∈ ℂ )
75 72 73 74 sylancr ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( 1 − ( 1 / 𝑠 ) ) ∈ ℂ )
76 75 adantr ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 − ( 1 / 𝑠 ) ) ∈ ℂ )
77 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 1 − 𝑠 ) ∈ ℂ )
78 72 77 mpan ⊢ ( 𝑠 ∈ ℂ → ( 1 − 𝑠 ) ∈ ℂ )
79 78 adantr ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( 1 − 𝑠 ) ∈ ℂ )
80 73 79 mulcld ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) ∈ ℂ )
81 80 adantr ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) ∈ ℂ )
82 simprr ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
83 76 81 82 adddird ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) )
84 simpl ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → 𝑠 ∈ ℂ )
85 subdi ⊢ ( ( ( 1 / 𝑠 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) = ( ( ( 1 / 𝑠 ) · 1 ) − ( ( 1 / 𝑠 ) · 𝑠 ) ) )
86 72 85 mp3an2 ⊢ ( ( ( 1 / 𝑠 ) ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) = ( ( ( 1 / 𝑠 ) · 1 ) − ( ( 1 / 𝑠 ) · 𝑠 ) ) )
87 73 84 86 syl2anc ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) = ( ( ( 1 / 𝑠 ) · 1 ) − ( ( 1 / 𝑠 ) · 𝑠 ) ) )
88 87 oveq2d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) ) = ( ( 1 − ( 1 / 𝑠 ) ) + ( ( ( 1 / 𝑠 ) · 1 ) − ( ( 1 / 𝑠 ) · 𝑠 ) ) ) )
89 73 mulridd ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 / 𝑠 ) · 1 ) = ( 1 / 𝑠 ) )
90 recid2 ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 / 𝑠 ) · 𝑠 ) = 1 )
91 89 90 oveq12d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( ( 1 / 𝑠 ) · 1 ) − ( ( 1 / 𝑠 ) · 𝑠 ) ) = ( ( 1 / 𝑠 ) − 1 ) )
92 91 oveq2d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( ( ( 1 / 𝑠 ) · 1 ) − ( ( 1 / 𝑠 ) · 𝑠 ) ) ) = ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) − 1 ) ) )
93 addsubass ⊢ ( ( ( 1 − ( 1 / 𝑠 ) ) ∈ ℂ ∧ ( 1 / 𝑠 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 1 − ( 1 / 𝑠 ) ) + ( 1 / 𝑠 ) ) − 1 ) = ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) − 1 ) ) )
94 72 93 mp3an3 ⊢ ( ( ( 1 − ( 1 / 𝑠 ) ) ∈ ℂ ∧ ( 1 / 𝑠 ) ∈ ℂ ) → ( ( ( 1 − ( 1 / 𝑠 ) ) + ( 1 / 𝑠 ) ) − 1 ) = ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) − 1 ) ) )
95 75 73 94 syl2anc ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( ( 1 − ( 1 / 𝑠 ) ) + ( 1 / 𝑠 ) ) − 1 ) = ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) − 1 ) ) )
96 75 73 addcld ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( 1 / 𝑠 ) ) ∈ ℂ )
97 npcan ⊢ ( ( 1 ∈ ℂ ∧ ( 1 / 𝑠 ) ∈ ℂ ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( 1 / 𝑠 ) ) = 1 )
98 72 73 97 sylancr ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( 1 / 𝑠 ) ) = 1 )
99 96 98 subeq0bd ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( ( 1 − ( 1 / 𝑠 ) ) + ( 1 / 𝑠 ) ) − 1 ) = 0 )
100 92 95 99 3eqtr2d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( ( ( 1 / 𝑠 ) · 1 ) − ( ( 1 / 𝑠 ) · 𝑠 ) ) ) = 0 )
101 88 100 eqtrd ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) ) = 0 )
102 101 adantr ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) ) = 0 )
103 102 oveq1d ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑠 ) ) + ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( 0 · ( 𝑍 ‘ 𝑖 ) ) )
104 73 adantr ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 / 𝑠 ) ∈ ℂ )
105 78 ad2antrr ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 − 𝑠 ) ∈ ℂ )
106 104 105 82 mulassd ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) )
107 106 oveq2d ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑠 ) · ( 1 − 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) )
108 83 103 107 3eqtr3rd ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) = ( 0 · ( 𝑍 ‘ 𝑖 ) ) )
109 mul02 ⊢ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ → ( 0 · ( 𝑍 ‘ 𝑖 ) ) = 0 )
110 109 ad2antll ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 0 · ( 𝑍 ‘ 𝑖 ) ) = 0 )
111 108 110 eqtrd ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) = 0 )
112 simpll ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → 𝑠 ∈ ℂ )
113 simprl ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑥 ‘ 𝑖 ) ∈ ℂ )
114 104 112 113 mulassd ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 / 𝑠 ) · 𝑠 ) · ( 𝑥 ‘ 𝑖 ) ) = ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) )
115 90 oveq1d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( ( 1 / 𝑠 ) · 𝑠 ) · ( 𝑥 ‘ 𝑖 ) ) = ( 1 · ( 𝑥 ‘ 𝑖 ) ) )
116 mullid ⊢ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑥 ‘ 𝑖 ) )
117 116 adantr ⊢ ( ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) → ( 1 · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑥 ‘ 𝑖 ) )
118 115 117 sylan9eq ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 / 𝑠 ) · 𝑠 ) · ( 𝑥 ‘ 𝑖 ) ) = ( 𝑥 ‘ 𝑖 ) )
119 114 118 eqtr3d ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) = ( 𝑥 ‘ 𝑖 ) )
120 111 119 oveq12d ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) = ( 0 + ( 𝑥 ‘ 𝑖 ) ) )
121 76 82 mulcld ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
122 simpr ⊢ ( ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
123 mulcl ⊢ ( ( ( 1 − 𝑠 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
124 79 122 123 syl2an ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
125 104 124 mulcld ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ∈ ℂ )
126 mulcl ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑥 ‘ 𝑖 ) ∈ ℂ ) → ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
127 126 ad2ant2r ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ∈ ℂ )
128 104 127 mulcld ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ∈ ℂ )
129 121 125 128 addassd ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
130 104 124 127 adddid ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) = ( ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
131 130 oveq2d ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
132 129 131 eqtr4d ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 1 / 𝑠 ) · ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
133 addlid ⊢ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ → ( 0 + ( 𝑥 ‘ 𝑖 ) ) = ( 𝑥 ‘ 𝑖 ) )
134 133 ad2antrl ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 0 + ( 𝑥 ‘ 𝑖 ) ) = ( 𝑥 ‘ 𝑖 ) )
135 120 132 134 3eqtr3rd ⊢ ( ( ( 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ∧ ( ( 𝑥 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
136 67 68 69 71 135 syl22anc ⊢ ( ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
137 136 ralrimiva ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
138 oveq2 ⊢ ( 𝑡 = ( 1 / 𝑠 ) → ( 1 − 𝑡 ) = ( 1 − ( 1 / 𝑠 ) ) )
139 138 oveq1d ⊢ ( 𝑡 = ( 1 / 𝑠 ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) )
140 oveq1 ⊢ ( 𝑡 = ( 1 / 𝑠 ) → ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) = ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
141 139 140 oveq12d ⊢ ( 𝑡 = ( 1 / 𝑠 ) → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
142 141 eqeq2d ⊢ ( 𝑡 = ( 1 / 𝑠 ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) )
143 142 ralbidv ⊢ ( 𝑡 = ( 1 / 𝑠 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) )
144 143 rspcev ⊢ ( ( ( 1 / 𝑠 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
145 65 137 144 syl2anc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
146 oveq2 ⊢ ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) → ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) )
147 146 oveq2d ⊢ ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) )
148 147 eqeq2d ⊢ ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) )
149 148 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) )
150 ralbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) )
151 149 150 syl ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) )
152 151 rexbidv ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) ) ) )
153 145 152 syl5ibrcom ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑠 ≠ 0 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
154 153 impancom ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) → ( 𝑠 ≠ 0 → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
155 48 154 mpd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
156 155 r19.29an ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑥 ‘ 𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
157 13 156 syldan ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
158 3simpa ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
159 elicc01 ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ∧ 𝑥 ≤ 1 ) )
160 elrege0 ⊢ ( 𝑥 ∈ ( 0 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
161 158 159 160 3imtr4i ⊢ ( 𝑥 ∈ ( 0 [,] 1 ) → 𝑥 ∈ ( 0 [,) +∞ ) )
162 161 ssriv ⊢ ( 0 [,] 1 ) ⊆ ( 0 [,) +∞ )
163 brbtwn ⊢ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
164 10 9 8 163 syl3anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
165 164 biimpa ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
166 ssrexv ⊢ ( ( 0 [,] 1 ) ⊆ ( 0 [,) +∞ ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
167 162 165 166 mpsyl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
168 157 167 jaodan ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
169 168 anasss ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑥 ⟩ ∨ 𝑥 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
170 7 169 sylan2b ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ 𝐷 ) → ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
171 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
172 eqtr2 ⊢ ( ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
173 172 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
174 171 173 sylbir ⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
175 elrege0 ⊢ ( 𝑡 ∈ ( 0 [,) +∞ ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) )
176 175 simplbi ⊢ ( 𝑡 ∈ ( 0 [,) +∞ ) → 𝑡 ∈ ℝ )
177 176 recnd ⊢ ( 𝑡 ∈ ( 0 [,) +∞ ) → 𝑡 ∈ ℂ )
178 elrege0 ⊢ ( 𝑠 ∈ ( 0 [,) +∞ ) ↔ ( 𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ) )
179 178 simplbi ⊢ ( 𝑠 ∈ ( 0 [,) +∞ ) → 𝑠 ∈ ℝ )
180 179 recnd ⊢ ( 𝑠 ∈ ( 0 [,) +∞ ) → 𝑠 ∈ ℂ )
181 177 180 anim12i ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 𝑠 ∈ ( 0 [,) +∞ ) ) → ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) )
182 simplr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) )
183 simpl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
184 183 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
185 184 30 sylancom ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
186 simpl3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
187 186 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
188 fveecn ⊢ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 ‘ 𝑖 ) ∈ ℂ )
189 187 188 sylancom ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 ‘ 𝑖 ) ∈ ℂ )
190 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( 1 − 𝑡 ) ∈ ℂ )
191 72 190 mpan ⊢ ( 𝑡 ∈ ℂ → ( 1 − 𝑡 ) ∈ ℂ )
192 191 adantr ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 1 − 𝑡 ) ∈ ℂ )
193 simpl ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
194 mulcl ⊢ ( ( ( 1 − 𝑡 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
195 192 193 194 syl2an ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
196 mulcl ⊢ ( ( 𝑡 ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) → ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ∈ ℂ )
197 196 ad2ant2rl ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ∈ ℂ )
198 78 adantl ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 1 − 𝑠 ) ∈ ℂ )
199 198 193 123 syl2an ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
200 mulcl ⊢ ( ( 𝑠 ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) → ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ∈ ℂ )
201 200 ad2ant2l ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ∈ ℂ )
202 195 197 199 201 addsubeq4d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) − ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) = ( ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) − ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
203 nnncan1 ⊢ ( ( 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 1 − 𝑠 ) − ( 1 − 𝑡 ) ) = ( 𝑡 − 𝑠 ) )
204 72 203 mp3an1 ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 1 − 𝑠 ) − ( 1 − 𝑡 ) ) = ( 𝑡 − 𝑠 ) )
205 204 ancoms ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( 1 − 𝑠 ) − ( 1 − 𝑡 ) ) = ( 𝑡 − 𝑠 ) )
206 205 oveq1d ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( ( 1 − 𝑠 ) − ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 𝑡 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) )
207 206 adantr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − 𝑠 ) − ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 𝑡 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) )
208 78 ad2antlr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 − 𝑠 ) ∈ ℂ )
209 191 ad2antrr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 − 𝑡 ) ∈ ℂ )
210 simprl ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
211 208 209 210 subdird ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − 𝑠 ) − ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) − ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) )
212 207 211 eqtr3d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 𝑡 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) − ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) )
213 simpll ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → 𝑡 ∈ ℂ )
214 simplr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → 𝑠 ∈ ℂ )
215 simprr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑈 ‘ 𝑖 ) ∈ ℂ )
216 213 214 215 subdird ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 𝑡 − 𝑠 ) · ( 𝑈 ‘ 𝑖 ) ) = ( ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) − ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
217 212 216 eqeq12d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 𝑡 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 𝑡 − 𝑠 ) · ( 𝑈 ‘ 𝑖 ) ) ↔ ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) − ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) = ( ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) − ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
218 subcl ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 𝑡 − 𝑠 ) ∈ ℂ )
219 218 adantr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑡 − 𝑠 ) ∈ ℂ )
220 mulcan1g ⊢ ( ( ( 𝑡 − 𝑠 ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) → ( ( ( 𝑡 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 𝑡 − 𝑠 ) · ( 𝑈 ‘ 𝑖 ) ) ↔ ( ( 𝑡 − 𝑠 ) = 0 ∨ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) )
221 219 210 215 220 syl3anc ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 𝑡 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 𝑡 − 𝑠 ) · ( 𝑈 ‘ 𝑖 ) ) ↔ ( ( 𝑡 − 𝑠 ) = 0 ∨ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) )
222 202 217 221 3bitr2d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( 𝑡 − 𝑠 ) = 0 ∨ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) )
223 182 185 189 222 syl12anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( 𝑡 − 𝑠 ) = 0 ∨ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) )
224 223 ralbidva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑡 − 𝑠 ) = 0 ∨ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ) )
225 r19.32v ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑡 − 𝑠 ) = 0 ∨ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) ↔ ( ( 𝑡 − 𝑠 ) = 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
226 simplr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → 𝑍 ≠ 𝑈 )
227 226 neneqd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ¬ 𝑍 = 𝑈 )
228 simpll2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
229 simpll3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
230 eqeefv ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
231 228 229 230 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
232 227 231 mtbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) )
233 orel2 ⊢ ( ¬ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) → ( ( ( 𝑡 − 𝑠 ) = 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) → ( 𝑡 − 𝑠 ) = 0 ) )
234 232 233 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ( ( ( 𝑡 − 𝑠 ) = 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) → ( 𝑡 − 𝑠 ) = 0 ) )
235 subeq0 ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( 𝑡 − 𝑠 ) = 0 ↔ 𝑡 = 𝑠 ) )
236 235 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ( ( 𝑡 − 𝑠 ) = 0 ↔ 𝑡 = 𝑠 ) )
237 234 236 sylibd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ( ( ( 𝑡 − 𝑠 ) = 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) → 𝑡 = 𝑠 ) )
238 225 237 biimtrid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑡 − 𝑠 ) = 0 ∨ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) → 𝑡 = 𝑠 ) )
239 224 238 sylbid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) → 𝑡 = 𝑠 ) )
240 181 239 sylan2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 𝑠 ∈ ( 0 [,) +∞ ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) → 𝑡 = 𝑠 ) )
241 174 240 syl5 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 𝑠 ∈ ( 0 [,) +∞ ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑡 = 𝑠 ) )
242 241 ralrimivva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → ∀ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑠 ∈ ( 0 [,) +∞ ) ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑡 = 𝑠 ) )
243 242 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ 𝐷 ) → ∀ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑠 ∈ ( 0 [,) +∞ ) ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑡 = 𝑠 ) )
244 oveq2 ⊢ ( 𝑡 = 𝑠 → ( 1 − 𝑡 ) = ( 1 − 𝑠 ) )
245 244 oveq1d ⊢ ( 𝑡 = 𝑠 → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) )
246 oveq1 ⊢ ( 𝑡 = 𝑠 → ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) )
247 245 246 oveq12d ⊢ ( 𝑡 = 𝑠 → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
248 247 eqeq2d ⊢ ( 𝑡 = 𝑠 → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
249 248 ralbidv ⊢ ( 𝑡 = 𝑠 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
250 249 reu4 ⊢ ( ∃! 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑠 ∈ ( 0 [,) +∞ ) ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑡 = 𝑠 ) ) )
251 170 243 250 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ 𝐷 ) → ∃! 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
252 df-reu ⊢ ( ∃! 𝑡 ∈ ( 0 [,) +∞ ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∃! 𝑡 ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
253 251 252 sylib ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑥 ∈ 𝐷 ) → ∃! 𝑡 ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
254 253 ralrimiva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → ∀ 𝑥 ∈ 𝐷 ∃! 𝑡 ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
255 2 fnopabg ⊢ ( ∀ 𝑥 ∈ 𝐷 ∃! 𝑡 ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ 𝐹 Fn 𝐷 )
256 254 255 sylib ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 Fn 𝐷 )
257 176 ad2antlr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℝ )
258 183 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
259 fveere ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑘 ) ∈ ℝ )
260 258 259 sylancom ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑘 ) ∈ ℝ )
261 186 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
262 fveere ⊢ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 ‘ 𝑘 ) ∈ ℝ )
263 261 262 sylancom ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 ‘ 𝑘 ) ∈ ℝ )
264 resubcl ⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) ∈ ℝ )
265 58 264 mpan ⊢ ( 𝑡 ∈ ℝ → ( 1 − 𝑡 ) ∈ ℝ )
266 remulcl ⊢ ( ( ( 1 − 𝑡 ) ∈ ℝ ∧ ( 𝑍 ‘ 𝑘 ) ∈ ℝ ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) ∈ ℝ )
267 265 266 sylan ⊢ ( ( 𝑡 ∈ ℝ ∧ ( 𝑍 ‘ 𝑘 ) ∈ ℝ ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) ∈ ℝ )
268 267 3adant3 ⊢ ( ( 𝑡 ∈ ℝ ∧ ( 𝑍 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑈 ‘ 𝑘 ) ∈ ℝ ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) ∈ ℝ )
269 remulcl ⊢ ( ( 𝑡 ∈ ℝ ∧ ( 𝑈 ‘ 𝑘 ) ∈ ℝ ) → ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ∈ ℝ )
270 269 3adant2 ⊢ ( ( 𝑡 ∈ ℝ ∧ ( 𝑍 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑈 ‘ 𝑘 ) ∈ ℝ ) → ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ∈ ℝ )
271 268 270 readdcld ⊢ ( ( 𝑡 ∈ ℝ ∧ ( 𝑍 ‘ 𝑘 ) ∈ ℝ ∧ ( 𝑈 ‘ 𝑘 ) ∈ ℝ ) → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ∈ ℝ )
272 257 260 263 271 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ∈ ℝ )
273 272 ralrimiva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ∈ ℝ )
274 simpll1 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → 𝑁 ∈ ℕ )
275 mptelee ⊢ ( 𝑁 ∈ ℕ → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ∈ ℝ ) )
276 274 275 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ∈ ℝ ) )
277 273 276 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
278 letric ⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 ≤ 𝑡 ∨ 𝑡 ≤ 1 ) )
279 58 176 278 sylancr ⊢ ( 𝑡 ∈ ( 0 [,) +∞ ) → ( 1 ≤ 𝑡 ∨ 𝑡 ≤ 1 ) )
280 279 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( 1 ≤ 𝑡 ∨ 𝑡 ≤ 1 ) )
281 simpr ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → 1 ≤ 𝑡 )
282 176 adantr ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → 𝑡 ∈ ℝ )
283 0red ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → 0 ∈ ℝ )
284 1red ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → 1 ∈ ℝ )
285 0lt1 ⊢ 0 < 1
286 285 a1i ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → 0 < 1 )
287 283 284 282 286 281 ltletrd ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → 0 < 𝑡 )
288 divelunit ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 𝑡 ∈ ℝ ∧ 0 < 𝑡 ) ) → ( ( 1 / 𝑡 ) ∈ ( 0 [,] 1 ) ↔ 1 ≤ 𝑡 ) )
289 58 59 288 mpanl12 ⊢ ( ( 𝑡 ∈ ℝ ∧ 0 < 𝑡 ) → ( ( 1 / 𝑡 ) ∈ ( 0 [,] 1 ) ↔ 1 ≤ 𝑡 ) )
290 282 287 289 syl2anc ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → ( ( 1 / 𝑡 ) ∈ ( 0 [,] 1 ) ↔ 1 ≤ 𝑡 ) )
291 281 290 mpbird ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → ( 1 / 𝑡 ) ∈ ( 0 [,] 1 ) )
292 291 adantll ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → ( 1 / 𝑡 ) ∈ ( 0 [,] 1 ) )
293 176 ad3antlr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℝ )
294 293 recnd ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
295 287 gt0ne0d ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 1 ≤ 𝑡 ) → 𝑡 ≠ 0 )
296 295 adantll ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → 𝑡 ≠ 0 )
297 296 adantr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ≠ 0 )
298 183 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
299 298 30 sylancom ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
300 186 ad3antrrr ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
301 300 188 sylancom ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 ‘ 𝑖 ) ∈ ℂ )
302 reccl ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( 1 / 𝑡 ) ∈ ℂ )
303 302 adantr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 / 𝑡 ) ∈ ℂ )
304 191 adantr ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( 1 − 𝑡 ) ∈ ℂ )
305 304 193 194 syl2an ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
306 196 ad2ant2rl ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ∈ ℂ )
307 303 305 306 adddid ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) = ( ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
308 307 oveq2d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
309 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 1 / 𝑡 ) ∈ ℂ ) → ( 1 − ( 1 / 𝑡 ) ) ∈ ℂ )
310 72 302 309 sylancr ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( 1 − ( 1 / 𝑡 ) ) ∈ ℂ )
311 mulcl ⊢ ( ( ( 1 − ( 1 / 𝑡 ) ) ∈ ℂ ∧ ( 𝑍 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
312 310 193 311 syl2an ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
313 303 305 mulcld ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ∈ ℂ )
314 recid2 ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 / 𝑡 ) · 𝑡 ) = 1 )
315 314 oveq1d ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( ( 1 / 𝑡 ) · 𝑡 ) · ( 𝑈 ‘ 𝑖 ) ) = ( 1 · ( 𝑈 ‘ 𝑖 ) ) )
316 315 adantr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 / 𝑡 ) · 𝑡 ) · ( 𝑈 ‘ 𝑖 ) ) = ( 1 · ( 𝑈 ‘ 𝑖 ) ) )
317 simpll ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → 𝑡 ∈ ℂ )
318 simprr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑈 ‘ 𝑖 ) ∈ ℂ )
319 303 317 318 mulassd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 / 𝑡 ) · 𝑡 ) · ( 𝑈 ‘ 𝑖 ) ) = ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
320 mullid ⊢ ( ( 𝑈 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑈 ‘ 𝑖 ) )
321 320 ad2antll ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑈 ‘ 𝑖 ) )
322 316 319 321 3eqtr3d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) )
323 322 318 eqeltrd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∈ ℂ )
324 312 313 323 addassd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
325 310 adantr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 − ( 1 / 𝑡 ) ) ∈ ℂ )
326 302 304 mulcld ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ∈ ℂ )
327 326 adantr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ∈ ℂ )
328 simprl ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
329 325 327 328 adddird ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) )
330 simpl ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → 𝑡 ∈ ℂ )
331 subdi ⊢ ( ( ( 1 / 𝑡 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( ( 1 / 𝑡 ) · 1 ) − ( ( 1 / 𝑡 ) · 𝑡 ) ) )
332 72 331 mp3an2 ⊢ ( ( ( 1 / 𝑡 ) ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( ( 1 / 𝑡 ) · 1 ) − ( ( 1 / 𝑡 ) · 𝑡 ) ) )
333 302 330 332 syl2anc ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( ( 1 / 𝑡 ) · 1 ) − ( ( 1 / 𝑡 ) · 𝑡 ) ) )
334 302 mulridd ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 / 𝑡 ) · 1 ) = ( 1 / 𝑡 ) )
335 334 314 oveq12d ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( ( 1 / 𝑡 ) · 1 ) − ( ( 1 / 𝑡 ) · 𝑡 ) ) = ( ( 1 / 𝑡 ) − 1 ) )
336 333 335 eqtrd ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( 1 / 𝑡 ) − 1 ) )
337 336 oveq2d ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ) = ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) − 1 ) ) )
338 npncan2 ⊢ ( ( 1 ∈ ℂ ∧ ( 1 / 𝑡 ) ∈ ℂ ) → ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) − 1 ) ) = 0 )
339 72 302 338 sylancr ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) − 1 ) ) = 0 )
340 337 339 eqtrd ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ) = 0 )
341 340 adantr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ) = 0 )
342 341 oveq1d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( 0 · ( 𝑍 ‘ 𝑖 ) ) )
343 109 ad2antrl ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 0 · ( 𝑍 ‘ 𝑖 ) ) = 0 )
344 342 343 eqtrd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑡 ) ) + ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = 0 )
345 191 ad2antrr ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 1 − 𝑡 ) ∈ ℂ )
346 303 345 328 mulassd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) )
347 346 oveq2d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 1 / 𝑡 ) · ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) )
348 329 344 347 3eqtr3rd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) = 0 )
349 348 322 oveq12d ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) = ( 0 + ( 𝑈 ‘ 𝑖 ) ) )
350 addlid ⊢ ( ( 𝑈 ‘ 𝑖 ) ∈ ℂ → ( 0 + ( 𝑈 ‘ 𝑖 ) ) = ( 𝑈 ‘ 𝑖 ) )
351 350 ad2antll ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 0 + ( 𝑈 ‘ 𝑖 ) ) = ( 𝑈 ‘ 𝑖 ) )
352 349 351 eqtrd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 1 / 𝑡 ) · ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) = ( 𝑈 ‘ 𝑖 ) )
353 308 324 352 3eqtr2rd ⊢ ( ( ( 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ∧ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑈 ‘ 𝑖 ) ∈ ℂ ) ) → ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
354 294 297 299 301 353 syl22anc ⊢ ( ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
355 354 ralrimiva ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
356 oveq2 ⊢ ( 𝑠 = ( 1 / 𝑡 ) → ( 1 − 𝑠 ) = ( 1 − ( 1 / 𝑡 ) ) )
357 356 oveq1d ⊢ ( 𝑠 = ( 1 / 𝑡 ) → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) )
358 oveq1 ⊢ ( 𝑠 = ( 1 / 𝑡 ) → ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) = ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) )
359 357 358 oveq12d ⊢ ( 𝑠 = ( 1 / 𝑡 ) → ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) )
360 359 eqeq2d ⊢ ( 𝑠 = ( 1 / 𝑡 ) → ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ↔ ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ) )
361 360 ralbidv ⊢ ( 𝑠 = ( 1 / 𝑡 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ) )
362 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑍 ‘ 𝑘 ) = ( 𝑍 ‘ 𝑖 ) )
363 362 oveq2d ⊢ ( 𝑘 = 𝑖 → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) = ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) )
364 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝑈 ‘ 𝑘 ) = ( 𝑈 ‘ 𝑖 ) )
365 364 oveq2d ⊢ ( 𝑘 = 𝑖 → ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) = ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) )
366 363 365 oveq12d ⊢ ( 𝑘 = 𝑖 → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
367 eqid ⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) )
368 ovex ⊢ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∈ V
369 366 367 368 fvmpt ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
370 369 oveq2d ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) = ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
371 370 oveq2d ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
372 371 eqeq2d ⊢ ( 𝑖 ∈ ( 1 ... 𝑁 ) → ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ↔ ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
373 372 ralbiia ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
374 361 373 bitrdi ⊢ ( 𝑠 = ( 1 / 𝑡 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
375 374 rspcev ⊢ ( ( ( 1 / 𝑡 ) ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − ( 1 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 1 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) → ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) )
376 292 355 375 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) )
377 186 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
378 183 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
379 277 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
380 brbtwn ⊢ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ) )
381 377 378 379 380 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → ( 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) ) ) ) )
382 376 381 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 1 ≤ 𝑡 ) → 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ )
383 382 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( 1 ≤ 𝑡 → 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ) )
384 simpll ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) ∧ 𝑡 ≤ 1 ) → 𝑡 ∈ ℝ )
385 simplr ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) ∧ 𝑡 ≤ 1 ) → 0 ≤ 𝑡 )
386 simpr ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) ∧ 𝑡 ≤ 1 ) → 𝑡 ≤ 1 )
387 384 385 386 3jca ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) ∧ 𝑡 ≤ 1 ) → ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) )
388 175 anbi1i ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 𝑡 ≤ 1 ) ↔ ( ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) ∧ 𝑡 ≤ 1 ) )
389 elicc01 ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) )
390 387 388 389 3imtr4i ⊢ ( ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ 𝑡 ≤ 1 ) → 𝑡 ∈ ( 0 [,] 1 ) )
391 390 adantll ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ≤ 1 ) → 𝑡 ∈ ( 0 [,] 1 ) )
392 369 rgen ⊢ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) )
393 oveq2 ⊢ ( 𝑠 = 𝑡 → ( 1 − 𝑠 ) = ( 1 − 𝑡 ) )
394 393 oveq1d ⊢ ( 𝑠 = 𝑡 → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) )
395 oveq1 ⊢ ( 𝑠 = 𝑡 → ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) )
396 394 395 oveq12d ⊢ ( 𝑠 = 𝑡 → ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
397 396 eqeq2d ⊢ ( 𝑠 = 𝑡 → ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
398 397 ralbidv ⊢ ( 𝑠 = 𝑡 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
399 398 rspcev ⊢ ( ( 𝑡 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
400 391 392 399 sylancl ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ≤ 1 ) → ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) )
401 277 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ≤ 1 ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) )
402 183 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ≤ 1 ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
403 186 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ≤ 1 ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
404 brbtwn ⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
405 401 402 403 404 syl3anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ≤ 1 ) → ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
406 400 405 mpbird ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ≤ 1 ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ )
407 406 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( 𝑡 ≤ 1 → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
408 383 407 orim12d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( ( 1 ≤ 𝑡 ∨ 𝑡 ≤ 1 ) → ( 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ∨ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
409 280 408 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ∨ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
410 opeq2 ⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) → ⟨ 𝑍 , 𝑝 ⟩ = ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ )
411 410 breq2d ⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ↔ 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ) )
412 breq1 ⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) → ( 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
413 411 412 orbi12d ⊢ ( 𝑝 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ↔ ( 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ∨ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
414 413 1 elrab2 ⊢ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ 𝐷 ↔ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ ( 𝔼 ‘ 𝑁 ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ⟩ ∨ ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
415 277 409 414 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ 𝐷 )
416 fveq1 ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) )
417 416 eqeq1d ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
418 417 ralbidv ⊢ ( 𝑥 = ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
419 418 rspcev ⊢ ( ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑘 ∈ ( 1 ... 𝑁 ) ↦ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑘 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑘 ) ) ) ) ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ∃ 𝑥 ∈ 𝐷 ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
420 415 392 419 sylancl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ∃ 𝑥 ∈ 𝐷 ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) )
421 7 simplbi ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) )
422 1 ssrab3 ⊢ 𝐷 ⊆ ( 𝔼 ‘ 𝑁 )
423 422 sseli ⊢ ( 𝑦 ∈ 𝐷 → 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) )
424 421 423 anim12i ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) )
425 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
426 eqtr3 ⊢ ( ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
427 426 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
428 425 427 sylbir ⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
429 eqeefv ⊢ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) )
430 429 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) )
431 428 430 imbitrrid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑥 = 𝑦 ) )
432 424 431 sylan2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑥 = 𝑦 ) )
433 432 ralrimivva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑥 = 𝑦 ) )
434 433 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑥 = 𝑦 ) )
435 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐷 ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
436 fveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
437 436 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
438 437 ralbidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
439 438 reu4 ⊢ ( ∃! 𝑥 ∈ 𝐷 ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐷 ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑥 = 𝑦 ) ) )
440 435 439 bitr3i ⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐷 ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑦 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) → 𝑥 = 𝑦 ) ) )
441 420 434 440 sylanbrc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ 𝑡 ∈ ( 0 [,) +∞ ) ) → ∃! 𝑥 ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
442 441 ralrimiva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → ∀ 𝑡 ∈ ( 0 [,) +∞ ) ∃! 𝑥 ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
443 an12 ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ↔ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
444 443 opabbii ⊢ { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ 𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) } = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
445 2 444 eqtri ⊢ 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
446 445 cnveqi ⊢ ◡ 𝐹 = ◡ { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
447 cnvopab ⊢ ◡ { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) } = { ⟨ 𝑡 , 𝑥 ⟩ ∣ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
448 446 447 eqtri ⊢ ◡ 𝐹 = { ⟨ 𝑡 , 𝑥 ⟩ ∣ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) }
449 448 fnopabg ⊢ ( ∀ 𝑡 ∈ ( 0 [,) +∞ ) ∃! 𝑥 ( 𝑥 ∈ 𝐷 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ◡ 𝐹 Fn ( 0 [,) +∞ ) )
450 442 449 sylib ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → ◡ 𝐹 Fn ( 0 [,) +∞ ) )
451 dff1o4 ⊢ ( 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) ↔ ( 𝐹 Fn 𝐷 ∧ ◡ 𝐹 Fn ( 0 [,) +∞ ) ) )
452 256 450 451 sylanbrc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) → 𝐹 : 𝐷 –1-1-onto→ ( 0 [,) +∞ ) )