Metamath Proof Explorer

Theorem axcontlem4

Description: Lemma for axcont . Given the separation assumption, A is a subset of D . (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypothesis axcontlem4.1 ⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
Assertion axcontlem4 ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ 𝐷 )

Proof

Step Hyp Ref Expression
1 axcontlem4.1 ⊢ 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2 simplr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) )
3 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ 𝐵 )
4 idd ⊢ ( 𝑏 ∈ 𝐵 → ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) → 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ) )
5 ssel ⊢ ( 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) )
6 5 com12 ⊢ ( 𝑏 ∈ 𝐵 → ( 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) )
7 opeq2 ⊢ ( 𝑦 = 𝑏 → ⟨ 𝑍 , 𝑦 ⟩ = ⟨ 𝑍 , 𝑏 ⟩ )
8 7 breq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ↔ 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
9 8 rspcv ⊢ ( 𝑏 ∈ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ → 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
10 9 ralimdv ⊢ ( 𝑏 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ → ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
11 4 6 10 3anim123d ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) → ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) )
12 11 anim2d ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) → ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ) )
13 simplr1 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) )
14 13 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) )
15 simplr2 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑈 ∈ 𝐴 )
16 14 15 sseldd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
17 simpr3 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) → ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
18 simp2 ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) → 𝑈 ∈ 𝐴 )
19 breq1 ⊢ ( 𝑥 = 𝑈 → ( 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
20 19 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑈 ∈ 𝐴 ) → 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
21 17 18 20 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) → 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
22 21 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
23 16 22 jca ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
24 13 sselda ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) )
25 17 adantr ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) → ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
26 breq1 ⊢ ( 𝑥 = 𝑝 → ( 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) )
27 26 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 ∈ 𝐴 ) → 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
28 25 27 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ )
29 23 24 28 jca32 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) )
30 an4 ⊢ ( ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ∧ ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ↔ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) )
31 29 30 sylib ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) )
32 simp2 ⊢ ( ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
33 simpl2r ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → 𝑍 ≠ 𝑈 )
34 33 adantr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) → 𝑍 ≠ 𝑈 )
35 simpl ⊢ ( ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) )
36 35 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) )
37 eqcom ⊢ ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) )
38 oveq2 ⊢ ( 𝑡 = 0 → ( 1 − 𝑡 ) = ( 1 − 0 ) )
39 1m0e1 ⊢ ( 1 − 0 ) = 1
40 38 39 eqtrdi ⊢ ( 𝑡 = 0 → ( 1 − 𝑡 ) = 1 )
41 40 oveq1d ⊢ ( 𝑡 = 0 → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) = ( 1 · ( 𝑍 ‘ 𝑖 ) ) )
42 oveq1 ⊢ ( 𝑡 = 0 → ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) = ( 0 · ( 𝑏 ‘ 𝑖 ) ) )
43 41 42 oveq12d ⊢ ( 𝑡 = 0 → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) )
44 43 eqeq1d ⊢ ( 𝑡 = 0 → ( ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) ↔ ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) ) )
45 37 44 bitrid ⊢ ( 𝑡 = 0 → ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ↔ ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) ) )
46 45 ralbidv ⊢ ( 𝑡 = 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) ) )
47 46 biimpac ⊢ ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ 𝑡 = 0 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) )
48 simpl2l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
49 simpl3l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
50 eqeefv ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
51 48 49 50 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
52 fveecn ⊢ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
53 48 52 sylan ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
54 simp1r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
55 54 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
56 fveecn ⊢ ( ( 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℂ )
57 55 56 sylancom ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℂ )
58 mullid ⊢ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ → ( 1 · ( 𝑍 ‘ 𝑖 ) ) = ( 𝑍 ‘ 𝑖 ) )
59 mul02 ⊢ ( ( 𝑏 ‘ 𝑖 ) ∈ ℂ → ( 0 · ( 𝑏 ‘ 𝑖 ) ) = 0 )
60 58 59 oveqan12d ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( 𝑍 ‘ 𝑖 ) + 0 ) )
61 addrid ⊢ ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ → ( ( 𝑍 ‘ 𝑖 ) + 0 ) = ( 𝑍 ‘ 𝑖 ) )
62 61 adantr ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) → ( ( 𝑍 ‘ 𝑖 ) + 0 ) = ( 𝑍 ‘ 𝑖 ) )
63 60 62 eqtrd ⊢ ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑍 ‘ 𝑖 ) )
64 53 57 63 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑍 ‘ 𝑖 ) )
65 64 eqeq1d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) ↔ ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
66 65 ralbidva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍 ‘ 𝑖 ) = ( 𝑈 ‘ 𝑖 ) ) )
67 51 66 bitr4d ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 1 · ( 𝑍 ‘ 𝑖 ) ) + ( 0 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑈 ‘ 𝑖 ) ) )
68 47 67 imbitrrid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ 𝑡 = 0 ) → 𝑍 = 𝑈 ) )
69 68 expdimp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( 𝑡 = 0 → 𝑍 = 𝑈 ) )
70 36 69 sylan2 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) → ( 𝑡 = 0 → 𝑍 = 𝑈 ) )
71 70 necon3d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) → ( 𝑍 ≠ 𝑈 → 𝑡 ≠ 0 ) )
72 34 71 mpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) → 𝑡 ≠ 0 )
73 simp1l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑁 ∈ ℕ )
74 simp2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
75 73 74 54 3jca ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) )
76 simp2l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑡 ∈ ( 0 [,] 1 ) )
77 elicc01 ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) )
78 77 simp1bi ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℝ )
79 76 78 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑡 ∈ ℝ )
80 simp2r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑠 ∈ ( 0 [,] 1 ) )
81 elicc01 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) ↔ ( 𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ∧ 𝑠 ≤ 1 ) )
82 81 simp1bi ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → 𝑠 ∈ ℝ )
83 80 82 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑠 ∈ ℝ )
84 79 83 letrid ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ( 𝑡 ≤ 𝑠 ∨ 𝑠 ≤ 𝑡 ) )
85 simpr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → 𝑡 ≤ 𝑠 )
86 79 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → 𝑡 ∈ ℝ )
87 77 simp2bi ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑡 )
88 76 87 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 0 ≤ 𝑡 )
89 88 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → 0 ≤ 𝑡 )
90 83 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → 𝑠 ∈ ℝ )
91 0red ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → 0 ∈ ℝ )
92 simp3 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑡 ≠ 0 )
93 79 88 92 ne0gt0d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 0 < 𝑡 )
94 93 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → 0 < 𝑡 )
95 91 86 90 94 85 ltletrd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → 0 < 𝑠 )
96 divelunit ⊢ ( ( ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ) ∧ ( 𝑠 ∈ ℝ ∧ 0 < 𝑠 ) ) → ( ( 𝑡 / 𝑠 ) ∈ ( 0 [,] 1 ) ↔ 𝑡 ≤ 𝑠 ) )
97 86 89 90 95 96 syl22anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → ( ( 𝑡 / 𝑠 ) ∈ ( 0 [,] 1 ) ↔ 𝑡 ≤ 𝑠 ) )
98 85 97 mpbird ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → ( 𝑡 / 𝑠 ) ∈ ( 0 [,] 1 ) )
99 simp12 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
100 99 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
101 100 52 sylancom ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
102 simp13 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
103 102 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
104 103 56 sylancom ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℂ )
105 78 recnd ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℂ )
106 76 105 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑡 ∈ ℂ )
107 106 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
108 82 recnd ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → 𝑠 ∈ ℂ )
109 80 108 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 𝑠 ∈ ℂ )
110 109 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
111 0red ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 0 ∈ ℝ )
112 79 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℝ )
113 83 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℝ )
114 88 ad2antrr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 0 ≤ 𝑡 )
115 simpll3 ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ≠ 0 )
116 112 114 115 ne0gt0d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 0 < 𝑡 )
117 simplr ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ≤ 𝑠 )
118 111 112 113 116 117 ltletrd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 0 < 𝑠 )
119 118 gt0ne0d ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ≠ 0 )
120 divcl ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( 𝑡 / 𝑠 ) ∈ ℂ )
121 120 adantl ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( 𝑡 / 𝑠 ) ∈ ℂ )
122 ax-1cn ⊢ 1 ∈ ℂ
123 simpr2 ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → 𝑠 ∈ ℂ )
124 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 1 − 𝑠 ) ∈ ℂ )
125 122 123 124 sylancr ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( 1 − 𝑠 ) ∈ ℂ )
126 simpll ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
127 125 126 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
128 simplr ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℂ )
129 123 128 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ∈ ℂ )
130 121 127 129 adddid ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
131 130 oveq2d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
132 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑡 / 𝑠 ) ∈ ℂ ) → ( 1 − ( 𝑡 / 𝑠 ) ) ∈ ℂ )
133 122 121 132 sylancr ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( 1 − ( 𝑡 / 𝑠 ) ) ∈ ℂ )
134 133 126 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
135 121 127 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ∈ ℂ )
136 121 129 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ∈ ℂ )
137 134 135 136 addassd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
138 121 125 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) ∈ ℂ )
139 133 138 126 adddird ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) )
140 simp2 ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → 𝑠 ∈ ℂ )
141 subdi ⊢ ( ( ( 𝑡 / 𝑠 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) = ( ( ( 𝑡 / 𝑠 ) · 1 ) − ( ( 𝑡 / 𝑠 ) · 𝑠 ) ) )
142 122 141 mp3an2 ⊢ ( ( ( 𝑡 / 𝑠 ) ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) = ( ( ( 𝑡 / 𝑠 ) · 1 ) − ( ( 𝑡 / 𝑠 ) · 𝑠 ) ) )
143 120 140 142 syl2anc ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) = ( ( ( 𝑡 / 𝑠 ) · 1 ) − ( ( 𝑡 / 𝑠 ) · 𝑠 ) ) )
144 120 mulridd ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 𝑡 / 𝑠 ) · 1 ) = ( 𝑡 / 𝑠 ) )
145 divcan1 ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 𝑡 / 𝑠 ) · 𝑠 ) = 𝑡 )
146 144 145 oveq12d ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( ( 𝑡 / 𝑠 ) · 1 ) − ( ( 𝑡 / 𝑠 ) · 𝑠 ) ) = ( ( 𝑡 / 𝑠 ) − 𝑡 ) )
147 143 146 eqtrd ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) = ( ( 𝑡 / 𝑠 ) − 𝑡 ) )
148 147 oveq2d ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) ) = ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) − 𝑡 ) ) )
149 simp1 ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → 𝑡 ∈ ℂ )
150 npncan ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑡 / 𝑠 ) ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) − 𝑡 ) ) = ( 1 − 𝑡 ) )
151 122 120 149 150 mp3an2i ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) − 𝑡 ) ) = ( 1 − 𝑡 ) )
152 148 151 eqtrd ⊢ ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) → ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) ) = ( 1 − 𝑡 ) )
153 152 adantl ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) ) = ( 1 − 𝑡 ) )
154 153 oveq1d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 1 − ( 𝑡 / 𝑠 ) ) + ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) )
155 121 125 126 mulassd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) )
156 155 oveq2d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑡 / 𝑠 ) · ( 1 − 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) )
157 139 154 156 3eqtr3rd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) = ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) )
158 121 123 128 mulassd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 𝑡 / 𝑠 ) · 𝑠 ) · ( 𝑏 ‘ 𝑖 ) ) = ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) )
159 145 adantl ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 𝑡 / 𝑠 ) · 𝑠 ) = 𝑡 )
160 159 oveq1d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 𝑡 / 𝑠 ) · 𝑠 ) · ( 𝑏 ‘ 𝑖 ) ) = ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) )
161 158 160 eqtr3d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) )
162 157 161 oveq12d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 𝑡 / 𝑠 ) · ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) )
163 131 137 162 3eqtr2rd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 0 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
164 101 104 107 110 119 163 syl23anc ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
165 164 ralrimiva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
166 oveq2 ⊢ ( 𝑟 = ( 𝑡 / 𝑠 ) → ( 1 − 𝑟 ) = ( 1 − ( 𝑡 / 𝑠 ) ) )
167 166 oveq1d ⊢ ( 𝑟 = ( 𝑡 / 𝑠 ) → ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) )
168 oveq1 ⊢ ( 𝑟 = ( 𝑡 / 𝑠 ) → ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
169 167 168 oveq12d ⊢ ( 𝑟 = ( 𝑡 / 𝑠 ) → ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
170 169 eqeq2d ⊢ ( 𝑟 = ( 𝑡 / 𝑠 ) → ( ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ↔ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
171 170 ralbidv ⊢ ( 𝑟 = ( 𝑡 / 𝑠 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
172 171 rspcev ⊢ ( ( ( 𝑡 / 𝑠 ) ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑡 / 𝑠 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑡 / 𝑠 ) · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
173 98 165 172 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑡 ≤ 𝑠 ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
174 173 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ( 𝑡 ≤ 𝑠 → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
175 81 simp2bi ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → 0 ≤ 𝑠 )
176 80 175 syl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → 0 ≤ 𝑠 )
177 divelunit ⊢ ( ( ( 𝑠 ∈ ℝ ∧ 0 ≤ 𝑠 ) ∧ ( 𝑡 ∈ ℝ ∧ 0 < 𝑡 ) ) → ( ( 𝑠 / 𝑡 ) ∈ ( 0 [,] 1 ) ↔ 𝑠 ≤ 𝑡 ) )
178 83 176 79 93 177 syl22anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ( ( 𝑠 / 𝑡 ) ∈ ( 0 [,] 1 ) ↔ 𝑠 ≤ 𝑡 ) )
179 178 biimpar ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ) → ( 𝑠 / 𝑡 ) ∈ ( 0 [,] 1 ) )
180 simp112 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
181 simp3 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑖 ∈ ( 1 ... 𝑁 ) )
182 180 181 52 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
183 simp113 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) )
184 183 181 56 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℂ )
185 simp12r ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
186 185 108 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑠 ∈ ℂ )
187 simp12l ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
188 187 105 syl ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
189 simp13 ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ≠ 0 )
190 divcl ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( 𝑠 / 𝑡 ) ∈ ℂ )
191 190 adantl ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( 𝑠 / 𝑡 ) ∈ ℂ )
192 simpr2 ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → 𝑡 ∈ ℂ )
193 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( 1 − 𝑡 ) ∈ ℂ )
194 122 192 193 sylancr ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
195 simpll ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( 𝑍 ‘ 𝑖 ) ∈ ℂ )
196 194 195 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
197 simplr ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( 𝑏 ‘ 𝑖 ) ∈ ℂ )
198 192 197 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ∈ ℂ )
199 191 196 198 adddid ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
200 199 oveq2d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
201 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑠 / 𝑡 ) ∈ ℂ ) → ( 1 − ( 𝑠 / 𝑡 ) ) ∈ ℂ )
202 122 191 201 sylancr ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( 1 − ( 𝑠 / 𝑡 ) ) ∈ ℂ )
203 202 195 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) ∈ ℂ )
204 191 196 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ∈ ℂ )
205 191 198 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∈ ℂ )
206 203 204 205 addassd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) + ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
207 simp2 ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → 𝑡 ∈ ℂ )
208 subdi ⊢ ( ( ( 𝑠 / 𝑡 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( ( 𝑠 / 𝑡 ) · 1 ) − ( ( 𝑠 / 𝑡 ) · 𝑡 ) ) )
209 122 208 mp3an2 ⊢ ( ( ( 𝑠 / 𝑡 ) ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( ( 𝑠 / 𝑡 ) · 1 ) − ( ( 𝑠 / 𝑡 ) · 𝑡 ) ) )
210 190 207 209 syl2anc ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( ( 𝑠 / 𝑡 ) · 1 ) − ( ( 𝑠 / 𝑡 ) · 𝑡 ) ) )
211 190 mulridd ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 𝑠 / 𝑡 ) · 1 ) = ( 𝑠 / 𝑡 ) )
212 divcan1 ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 𝑠 / 𝑡 ) · 𝑡 ) = 𝑠 )
213 211 212 oveq12d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( ( 𝑠 / 𝑡 ) · 1 ) − ( ( 𝑠 / 𝑡 ) · 𝑡 ) ) = ( ( 𝑠 / 𝑡 ) − 𝑠 ) )
214 210 213 eqtrd ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) = ( ( 𝑠 / 𝑡 ) − 𝑠 ) )
215 214 oveq2d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) ) = ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) − 𝑠 ) ) )
216 simp1 ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → 𝑠 ∈ ℂ )
217 npncan ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑠 / 𝑡 ) ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) − 𝑠 ) ) = ( 1 − 𝑠 ) )
218 122 190 216 217 mp3an2i ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) − 𝑠 ) ) = ( 1 − 𝑠 ) )
219 215 218 eqtr2d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( 1 − 𝑠 ) = ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) ) )
220 219 oveq1d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) )
221 220 adantl ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) )
222 191 194 mulcld ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) ∈ ℂ )
223 202 222 195 adddird ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 1 − ( 𝑠 / 𝑡 ) ) + ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) )
224 191 194 195 mulassd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) )
225 224 oveq2d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( ( 𝑠 / 𝑡 ) · ( 1 − 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) )
226 221 223 225 3eqtrrd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) = ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) )
227 191 192 197 mulassd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 𝑠 / 𝑡 ) · 𝑡 ) · ( 𝑏 ‘ 𝑖 ) ) = ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) )
228 212 oveq1d ⊢ ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) → ( ( ( 𝑠 / 𝑡 ) · 𝑡 ) · ( 𝑏 ‘ 𝑖 ) ) = ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) )
229 228 adantl ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 𝑠 / 𝑡 ) · 𝑡 ) · ( 𝑏 ‘ 𝑖 ) ) = ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) )
230 227 229 eqtr3d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) )
231 226 230 oveq12d ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) ) ) + ( ( 𝑠 / 𝑡 ) · ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) )
232 200 206 231 3eqtr2rd ⊢ ( ( ( ( 𝑍 ‘ 𝑖 ) ∈ ℂ ∧ ( 𝑏 ‘ 𝑖 ) ∈ ℂ ) ∧ ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 0 ) ) → ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
233 182 184 186 188 189 232 syl23anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
234 233 3expa ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
235 234 ralrimiva ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
236 oveq2 ⊢ ( 𝑟 = ( 𝑠 / 𝑡 ) → ( 1 − 𝑟 ) = ( 1 − ( 𝑠 / 𝑡 ) ) )
237 236 oveq1d ⊢ ( 𝑟 = ( 𝑠 / 𝑡 ) → ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) = ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) )
238 oveq1 ⊢ ( 𝑟 = ( 𝑠 / 𝑡 ) → ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) = ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
239 237 238 oveq12d ⊢ ( 𝑟 = ( 𝑠 / 𝑡 ) → ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
240 239 eqeq2d ⊢ ( 𝑟 = ( 𝑠 / 𝑡 ) → ( ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ↔ ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
241 240 ralbidv ⊢ ( 𝑟 = ( 𝑠 / 𝑡 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
242 241 rspcev ⊢ ( ( ( 𝑠 / 𝑡 ) ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − ( 𝑠 / 𝑡 ) ) · ( 𝑍 ‘ 𝑖 ) ) + ( ( 𝑠 / 𝑡 ) · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
243 179 235 242 syl2anc ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) ∧ 𝑠 ≤ 𝑡 ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
244 243 ex ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ( 𝑠 ≤ 𝑡 → ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
245 174 244 orim12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ( ( 𝑡 ≤ 𝑠 ∨ 𝑠 ≤ 𝑡 ) → ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∨ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
246 r19.43 ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∨ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
247 245 246 imbitrrdi ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ( ( 𝑡 ≤ 𝑠 ∨ 𝑠 ≤ 𝑡 ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
248 84 247 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
249 id ⊢ ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) → ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) )
250 oveq2 ⊢ ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) → ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) = ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
251 250 oveq2d ⊢ ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) → ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
252 249 251 eqeqan12d ⊢ ( ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
253 252 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
254 ralbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
255 253 254 syl ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
256 id ⊢ ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) )
257 oveq2 ⊢ ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) → ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) = ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
258 257 oveq2d ⊢ ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) → ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
259 256 258 eqeqan12rd ⊢ ( ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
260 259 ralimi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
261 ralbi ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
262 260 261 syl ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) )
263 255 262 orbi12d ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
264 263 rexbidv ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) ) ) )
265 248 264 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ∧ 𝑡 ≠ 0 ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
266 265 3expia ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( 𝑡 ≠ 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
267 266 com23 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( 𝑡 ≠ 0 → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
268 75 267 sylan ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ( 𝑡 ≠ 0 → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) ) )
269 268 imp ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) → ( 𝑡 ≠ 0 → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
270 72 269 mpd ⊢ ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
271 270 ex ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
272 271 rexlimdvva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) → ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
273 simp3l ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
274 brbtwn ⊢ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
275 273 74 54 274 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
276 simp3r ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) )
277 brbtwn ⊢ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
278 276 74 54 277 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ↔ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
279 275 278 anbi12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
280 r19.26 ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
281 280 2rexbii ⊢ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
282 reeanv ⊢ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
283 281 282 bitri ⊢ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) )
284 279 283 bitr4di ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∃ 𝑠 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑡 · ( 𝑏 ‘ 𝑖 ) ) ) ∧ ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑠 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑠 · ( 𝑏 ‘ 𝑖 ) ) ) ) ) )
285 brbtwn ⊢ ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ) )
286 273 74 276 285 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ) )
287 brbtwn ⊢ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
288 276 74 273 287 syl3anc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
289 286 288 orbi12d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
290 r19.43 ⊢ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ↔ ( ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∃ 𝑟 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) )
291 289 290 bitr4di ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ↔ ∃ 𝑟 ∈ ( 0 [,] 1 ) ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑈 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑝 ‘ 𝑖 ) ) ) ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑝 ‘ 𝑖 ) = ( ( ( 1 − 𝑟 ) · ( 𝑍 ‘ 𝑖 ) ) + ( 𝑟 · ( 𝑈 ‘ 𝑖 ) ) ) ) ) )
292 272 284 291 3imtr4d ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
293 292 3expia ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) )
294 293 impd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
295 32 294 sylanl2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ≠ 𝑈 ) ) → ( ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
296 295 3adantr2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) → ( ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
297 296 adantr ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑈 Btwn ⟨ 𝑍 , 𝑏 ⟩ ∧ 𝑝 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
298 31 297 mpd ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) ∧ 𝑝 ∈ 𝐴 ) → ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
299 298 ralrimiva ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝑍 ≠ 𝑈 ) ) → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
300 299 3exp2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 𝑥 Btwn ⟨ 𝑍 , 𝑏 ⟩ ) ) → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑈 ∈ 𝐴 → ( 𝑍 ≠ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) ) )
301 12 300 syl6 ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑈 ∈ 𝐴 → ( 𝑍 ≠ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) ) ) )
302 301 exlimiv ⊢ ( ∃ 𝑏 𝑏 ∈ 𝐵 → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑈 ∈ 𝐴 → ( 𝑍 ≠ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) ) ) )
303 3 302 sylbi ⊢ ( 𝐵 ≠ ∅ → ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑈 ∈ 𝐴 → ( 𝑍 ≠ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) ) ) )
304 303 com4l ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) → ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑈 ∈ 𝐴 → ( 𝐵 ≠ ∅ → ( 𝑍 ≠ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) ) ) )
305 304 3impd ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) → ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) → ( 𝑍 ≠ 𝑈 → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) ) )
306 305 imp32 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) )
307 1 sseq2i ⊢ ( 𝐴 ⊆ 𝐷 ↔ 𝐴 ⊆ { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) } )
308 ssrab ⊢ ( 𝐴 ⊆ { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) } ↔ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
309 307 308 bitri ⊢ ( 𝐴 ⊆ 𝐷 ↔ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑝 ∈ 𝐴 ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) ) )
310 2 306 309 sylanbrc ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ⊆ ( 𝔼 ‘ 𝑁 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝑥 Btwn ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ 𝐷 )