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 syl5bb ( 𝑡 = 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 mulid2 ( ( 𝑍𝑖 ) ∈ ℂ → ( 1 · ( 𝑍𝑖 ) ) = ( 𝑍𝑖 ) )
59 mul02 ( ( 𝑏𝑖 ) ∈ ℂ → ( 0 · ( 𝑏𝑖 ) ) = 0 )
60 58 59 oveqan12d ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑏𝑖 ) ∈ ℂ ) → ( ( 1 · ( 𝑍𝑖 ) ) + ( 0 · ( 𝑏𝑖 ) ) ) = ( ( 𝑍𝑖 ) + 0 ) )
61 addid1 ( ( 𝑍𝑖 ) ∈ ℂ → ( ( 𝑍𝑖 ) + 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 syl5ibr ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍𝑈 ) ∧ ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝑡 ∈ ( 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 mulid1d ( ( 𝑡 ∈ ℂ ∧ 𝑠 ∈ ℂ ∧ 𝑠 ≠ 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 mulid1d ( ( 𝑠 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ 𝑡 ≠ 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 syl6ibr ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑡 ∈ ( 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 ⟨ 𝑍 , 𝑦 ⟩ ) ) ∧ ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈𝐴𝐵 ≠ ∅ ) ∧ 𝑍𝑈 ) ) → 𝐴𝐷 )