Metamath Proof Explorer


Theorem axcontlem7

Description: Lemma for axcont . Given two points in D , one preceeds the other iff its scaling constant is less than the other point's. (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypotheses axcontlem7.1 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
axcontlem7.2 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑈𝑖 ) ) ) ) ) }
Assertion axcontlem7 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → ( 𝑃 Btwn ⟨ 𝑍 , 𝑄 ⟩ ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 axcontlem7.1 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2 axcontlem7.2 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑈𝑖 ) ) ) ) ) }
3 1 ssrab3 𝐷 ⊆ ( 𝔼 ‘ 𝑁 )
4 3 sseli ( 𝑃𝐷𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
5 4 ad2antrl ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
6 simpll2 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
7 3 sseli ( 𝑄𝐷𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
8 7 ad2antll ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
9 brbtwn ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑃 Btwn ⟨ 𝑍 , 𝑄 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ) )
10 5 6 8 9 syl3anc ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → ( 𝑃 Btwn ⟨ 𝑍 , 𝑄 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ) )
11 1 2 axcontlem6 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ 𝑃𝐷 ) → ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) )
12 1 2 axcontlem6 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ 𝑄𝐷 ) → ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) )
13 11 12 anim12dan ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
14 an4 ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
15 r19.26 ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) )
16 15 anbi2i ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
17 14 16 bitr4i ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
18 id ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) → ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) )
19 oveq2 ( ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) → ( 𝑡 · ( 𝑄𝑖 ) ) = ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) )
20 19 oveq2d ( ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
21 18 20 eqeqan12d ( ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) → ( ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
22 21 ralimi ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
23 ralbi ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
24 22 23 syl ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
25 24 rexbidv ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
26 simpll2 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
27 fveecn ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍𝑖 ) ∈ ℂ )
28 26 27 sylan ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍𝑖 ) ∈ ℂ )
29 simpll3 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
30 fveecn ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈𝑖 ) ∈ ℂ )
31 29 30 sylan ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈𝑖 ) ∈ ℂ )
32 elicc01 ( 𝑡 ∈ ( 0 [,] 1 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡𝑡 ≤ 1 ) )
33 32 simp1bi ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℝ )
34 33 recnd ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ∈ ℂ )
35 34 ad2antll ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → 𝑡 ∈ ℂ )
36 35 adantr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑡 ∈ ℂ )
37 elrege0 ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹𝑃 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑃 ) ) )
38 37 simplbi ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑃 ) ∈ ℝ )
39 38 recnd ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑃 ) ∈ ℂ )
40 39 adantr ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( 𝐹𝑃 ) ∈ ℂ )
41 40 ad2antrl ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹𝑃 ) ∈ ℂ )
42 41 adantr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ∈ ℂ )
43 elrege0 ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹𝑄 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑄 ) ) )
44 43 simplbi ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑄 ) ∈ ℝ )
45 44 recnd ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑄 ) ∈ ℂ )
46 45 adantl ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( 𝐹𝑄 ) ∈ ℂ )
47 46 ad2antrl ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹𝑄 ) ∈ ℂ )
48 47 adantr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑄 ) ∈ ℂ )
49 ax-1cn 1 ∈ ℂ
50 simpr1 ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → 𝑡 ∈ ℂ )
51 simpr3 ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝐹𝑄 ) ∈ ℂ )
52 50 51 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑡 · ( 𝐹𝑄 ) ) ∈ ℂ )
53 subcl ( ( 1 ∈ ℂ ∧ ( 𝑡 · ( 𝐹𝑄 ) ) ∈ ℂ ) → ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) ∈ ℂ )
54 49 52 53 sylancr ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) ∈ ℂ )
55 subcl ( ( 1 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ) → ( 1 − ( 𝐹𝑃 ) ) ∈ ℂ )
56 49 55 mpan ( ( 𝐹𝑃 ) ∈ ℂ → ( 1 − ( 𝐹𝑃 ) ) ∈ ℂ )
57 56 3ad2ant2 ( ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 1 − ( 𝐹𝑃 ) ) ∈ ℂ )
58 57 adantl ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 1 − ( 𝐹𝑃 ) ) ∈ ℂ )
59 simpll ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑍𝑖 ) ∈ ℂ )
60 54 58 59 subdird ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) − ( 1 − ( 𝐹𝑃 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) − ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) )
61 simpr2 ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝐹𝑃 ) ∈ ℂ )
62 nnncan1 ( ( 1 ∈ ℂ ∧ ( 𝑡 · ( 𝐹𝑄 ) ) ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ) → ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) − ( 1 − ( 𝐹𝑃 ) ) ) = ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
63 49 52 61 62 mp3an2i ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) − ( 1 − ( 𝐹𝑃 ) ) ) = ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
64 63 oveq1d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) − ( 1 − ( 𝐹𝑃 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) )
65 subdi ( ( 𝑡 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) = ( ( 𝑡 · 1 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
66 49 65 mp3an2 ( ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) = ( ( 𝑡 · 1 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
67 mulid1 ( 𝑡 ∈ ℂ → ( 𝑡 · 1 ) = 𝑡 )
68 67 adantr ( ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 𝑡 · 1 ) = 𝑡 )
69 68 oveq1d ( ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( ( 𝑡 · 1 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = ( 𝑡 − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
70 66 69 eqtrd ( ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) = ( 𝑡 − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
71 50 51 70 syl2anc ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) = ( 𝑡 − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
72 71 oveq2d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − 𝑡 ) + ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) ) = ( ( 1 − 𝑡 ) + ( 𝑡 − ( 𝑡 · ( 𝐹𝑄 ) ) ) ) )
73 npncan ( ( 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ∧ ( 𝑡 · ( 𝐹𝑄 ) ) ∈ ℂ ) → ( ( 1 − 𝑡 ) + ( 𝑡 − ( 𝑡 · ( 𝐹𝑄 ) ) ) ) = ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
74 49 50 52 73 mp3an2i ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − 𝑡 ) + ( 𝑡 − ( 𝑡 · ( 𝐹𝑄 ) ) ) ) = ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) )
75 72 74 eqtr2d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) = ( ( 1 − 𝑡 ) + ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) ) )
76 75 oveq1d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 1 − 𝑡 ) + ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) ) · ( 𝑍𝑖 ) ) )
77 subcl ( ( 1 ∈ ℂ ∧ 𝑡 ∈ ℂ ) → ( 1 − 𝑡 ) ∈ ℂ )
78 49 77 mpan ( 𝑡 ∈ ℂ → ( 1 − 𝑡 ) ∈ ℂ )
79 78 3ad2ant1 ( ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 1 − 𝑡 ) ∈ ℂ )
80 79 adantl ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 1 − 𝑡 ) ∈ ℂ )
81 subcl ( ( 1 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 1 − ( 𝐹𝑄 ) ) ∈ ℂ )
82 49 81 mpan ( ( 𝐹𝑄 ) ∈ ℂ → ( 1 − ( 𝐹𝑄 ) ) ∈ ℂ )
83 82 3ad2ant3 ( ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 1 − ( 𝐹𝑄 ) ) ∈ ℂ )
84 83 adantl ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 1 − ( 𝐹𝑄 ) ) ∈ ℂ )
85 50 84 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) ∈ ℂ )
86 80 85 59 adddird ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 1 − 𝑡 ) + ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) ) )
87 50 84 59 mulassd ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) )
88 87 oveq2d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( ( 𝑡 · ( 1 − ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) )
89 76 86 88 3eqtrd ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) )
90 89 oveq1d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) − ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) = ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) − ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) )
91 60 64 90 3eqtr3d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) − ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) )
92 simplr ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑈𝑖 ) ∈ ℂ )
93 61 52 92 subdird ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) = ( ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) − ( ( 𝑡 · ( 𝐹𝑄 ) ) · ( 𝑈𝑖 ) ) ) )
94 50 51 92 mulassd ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 𝑡 · ( 𝐹𝑄 ) ) · ( 𝑈𝑖 ) ) = ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) )
95 94 oveq2d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) − ( ( 𝑡 · ( 𝐹𝑄 ) ) · ( 𝑈𝑖 ) ) ) = ( ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) − ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) )
96 93 95 eqtrd ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) = ( ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) − ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) )
97 91 96 eqeq12d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) ↔ ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) − ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) = ( ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) − ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
98 58 59 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ∈ ℂ )
99 61 92 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ∈ ℂ )
100 80 59 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) ∈ ℂ )
101 84 59 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ∈ ℂ )
102 50 101 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ∈ ℂ )
103 100 102 addcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) ∈ ℂ )
104 51 92 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ∈ ℂ )
105 50 104 mulcld ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∈ ℂ )
106 98 99 103 105 addsubeq4d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) + ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ↔ ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) − ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) = ( ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) − ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
107 100 102 105 addassd ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) + ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) + ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
108 50 101 104 adddid ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) = ( ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) + ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) )
109 108 oveq2d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) + ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
110 107 109 eqtr4d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) + ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
111 110 eqeq2d ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) ) ) + ( 𝑡 · ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
112 97 106 111 3bitr2rd ( ( ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ∧ ( 𝑡 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) ) )
113 28 31 36 42 48 112 syl23anc ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) ) )
114 113 ralbidva ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) ) )
115 36 48 mulcld ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑡 · ( 𝐹𝑄 ) ) ∈ ℂ )
116 42 115 subcld ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) ∈ ℂ )
117 mulcan1g ( ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) ∈ ℂ ∧ ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) → ( ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) ) )
118 116 28 31 117 syl3anc ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) ) )
119 118 ralbidva ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) · ( 𝑈𝑖 ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) ) )
120 r19.32v ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) )
121 simplr ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → 𝑍𝑈 )
122 121 neneqd ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ¬ 𝑍 = 𝑈 )
123 biorf ( ¬ 𝑍 = 𝑈 → ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ↔ ( 𝑍 = 𝑈 ∨ ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ) ) )
124 orcom ( ( 𝑍 = 𝑈 ∨ ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ) ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ 𝑍 = 𝑈 ) )
125 123 124 bitrdi ( ¬ 𝑍 = 𝑈 → ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ 𝑍 = 𝑈 ) ) )
126 122 125 syl ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ 𝑍 = 𝑈 ) ) )
127 35 47 mulcld ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝑡 · ( 𝐹𝑄 ) ) ∈ ℂ )
128 41 127 subeq0ad ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ↔ ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
129 eqeefv ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) )
130 129 3adant1 ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) )
131 130 adantr ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) )
132 131 adantr ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝑍 = 𝑈 ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) )
133 132 orbi2d ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ 𝑍 = 𝑈 ) ↔ ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) ) )
134 126 128 133 3bitr3rd ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) ↔ ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
135 120 134 syl5bb ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐹𝑃 ) − ( 𝑡 · ( 𝐹𝑄 ) ) ) = 0 ∨ ( 𝑍𝑖 ) = ( 𝑈𝑖 ) ) ↔ ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
136 114 119 135 3bitrd ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
137 136 anassrs ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
138 137 rexbidva ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
139 33 adantl ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ℝ )
140 1red ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 1 ∈ ℝ )
141 43 biimpi ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) → ( ( 𝐹𝑄 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑄 ) ) )
142 141 ad2antlr ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹𝑄 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑄 ) ) )
143 32 simp3bi ( 𝑡 ∈ ( 0 [,] 1 ) → 𝑡 ≤ 1 )
144 143 adantl ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ≤ 1 )
145 lemul1a ( ( ( 𝑡 ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 𝐹𝑄 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑄 ) ) ) ∧ 𝑡 ≤ 1 ) → ( 𝑡 · ( 𝐹𝑄 ) ) ≤ ( 1 · ( 𝐹𝑄 ) ) )
146 139 140 142 144 145 syl31anc ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑡 · ( 𝐹𝑄 ) ) ≤ ( 1 · ( 𝐹𝑄 ) ) )
147 45 ad2antlr ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝐹𝑄 ) ∈ ℂ )
148 147 mulid2d ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 𝐹𝑄 ) ) = ( 𝐹𝑄 ) )
149 146 148 breqtrd ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑡 · ( 𝐹𝑄 ) ) ≤ ( 𝐹𝑄 ) )
150 breq1 ( ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) → ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ↔ ( 𝑡 · ( 𝐹𝑄 ) ) ≤ ( 𝐹𝑄 ) ) )
151 149 150 syl5ibrcom ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) → ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
152 151 rexlimdva ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) → ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
153 0elunit 0 ∈ ( 0 [,] 1 )
154 simpl ( ( ( 𝐹𝑃 ) = 0 ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( 𝐹𝑃 ) = 0 )
155 45 mul02d ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) → ( 0 · ( 𝐹𝑄 ) ) = 0 )
156 155 adantl ( ( ( 𝐹𝑃 ) = 0 ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( 0 · ( 𝐹𝑄 ) ) = 0 )
157 154 156 eqtr4d ( ( ( 𝐹𝑃 ) = 0 ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( 𝐹𝑃 ) = ( 0 · ( 𝐹𝑄 ) ) )
158 oveq1 ( 𝑡 = 0 → ( 𝑡 · ( 𝐹𝑄 ) ) = ( 0 · ( 𝐹𝑄 ) ) )
159 158 rspceeqv ( ( 0 ∈ ( 0 [,] 1 ) ∧ ( 𝐹𝑃 ) = ( 0 · ( 𝐹𝑄 ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) )
160 153 157 159 sylancr ( ( ( 𝐹𝑃 ) = 0 ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) )
161 160 adantrl ( ( ( 𝐹𝑃 ) = 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) )
162 161 a1d ( ( ( 𝐹𝑃 ) = 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ) → ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
163 162 ex ( ( 𝐹𝑃 ) = 0 → ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) ) )
164 simp3 ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) )
165 38 adantr ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( 𝐹𝑃 ) ∈ ℝ )
166 165 3ad2ant2 ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑃 ) ∈ ℝ )
167 37 simprbi ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) → 0 ≤ ( 𝐹𝑃 ) )
168 167 adantr ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → 0 ≤ ( 𝐹𝑃 ) )
169 168 3ad2ant2 ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → 0 ≤ ( 𝐹𝑃 ) )
170 44 adantl ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( 𝐹𝑄 ) ∈ ℝ )
171 170 3ad2ant2 ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑄 ) ∈ ℝ )
172 0red ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → 0 ∈ ℝ )
173 simp1 ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑃 ) ≠ 0 )
174 166 169 173 ne0gt0d ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → 0 < ( 𝐹𝑃 ) )
175 172 166 171 174 164 ltletrd ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → 0 < ( 𝐹𝑄 ) )
176 divelunit ( ( ( ( 𝐹𝑃 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑃 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℝ ∧ 0 < ( 𝐹𝑄 ) ) ) → ( ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) ∈ ( 0 [,] 1 ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
177 166 169 171 175 176 syl22anc ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) ∈ ( 0 [,] 1 ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
178 164 177 mpbird ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) ∈ ( 0 [,] 1 ) )
179 40 3ad2ant2 ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑃 ) ∈ ℂ )
180 46 3ad2ant2 ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑄 ) ∈ ℂ )
181 175 gt0ne0d ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑄 ) ≠ 0 )
182 179 180 181 divcan1d ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) · ( 𝐹𝑄 ) ) = ( 𝐹𝑃 ) )
183 182 eqcomd ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ( 𝐹𝑃 ) = ( ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) · ( 𝐹𝑄 ) ) )
184 oveq1 ( 𝑡 = ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) → ( 𝑡 · ( 𝐹𝑄 ) ) = ( ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) · ( 𝐹𝑄 ) ) )
185 184 rspceeqv ( ( ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) ∈ ( 0 [,] 1 ) ∧ ( 𝐹𝑃 ) = ( ( ( 𝐹𝑃 ) / ( 𝐹𝑄 ) ) · ( 𝐹𝑄 ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) )
186 178 183 185 syl2anc ( ( ( 𝐹𝑃 ) ≠ 0 ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) )
187 186 3exp ( ( 𝐹𝑃 ) ≠ 0 → ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) ) )
188 163 187 pm2.61ine ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ) )
189 152 188 impbid ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
190 189 adantl ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ( 𝐹𝑃 ) = ( 𝑡 · ( 𝐹𝑄 ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
191 138 190 bitrd ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
192 25 191 sylan9bbr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
193 192 anasss ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
194 17 193 sylan2b ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
195 13 194 syldan ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑄𝑖 ) ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
196 10 195 bitrd ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷 ) ) → ( 𝑃 Btwn ⟨ 𝑍 , 𝑄 ⟩ ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )