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 mulrid ⊢ ( 𝑡 ∈ ℂ → ( 𝑡 · 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 bitrid ⊢ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍 ≠ 𝑈 ) ∧ ( ( ( 𝐹 ‘ 𝑃 ) ∈ ( 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 mullidd ⊢ ( ( ( ( 𝐹 ‘ 𝑃 ) ∈ ( 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 ⟨ 𝑍 , 𝑄 ⟩ ↔ ( 𝐹 ‘ 𝑃 ) ≤ ( 𝐹 ‘ 𝑄 ) ) )