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 ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ) ∧ 𝑍 ≠ 𝑈 ) ) → 𝐴 ⊆ 𝐷 )