Metamath Proof Explorer


Theorem axcontlem8

Description: Lemma for axcont . A point in D is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 axcontlem8.1 𝐷 = { 𝑝 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑈 Btwn ⟨ 𝑍 , 𝑝 ⟩ ∨ 𝑝 Btwn ⟨ 𝑍 , 𝑈 ⟩ ) }
2 axcontlem8.2 𝐹 = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥𝐷 ∧ ( 𝑡 ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑥𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑍𝑖 ) ) + ( 𝑡 · ( 𝑈𝑖 ) ) ) ) ) }
3 1 2 axcontlem6 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ 𝑃𝐷 ) → ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) )
4 3 ex ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) → ( 𝑃𝐷 → ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ) )
5 1 2 axcontlem6 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ 𝑄𝐷 ) → ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) )
6 5 ex ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) → ( 𝑄𝐷 → ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ) )
7 1 2 axcontlem6 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ 𝑅𝐷 ) → ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
8 7 ex ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) → ( 𝑅𝐷 → ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
9 4 6 8 3anim123d ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) → ( ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) → ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
10 9 imp ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) → ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
11 10 adantr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
12 3an6 ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
13 0elunit 0 ∈ ( 0 [,] 1 )
14 simplr1 ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) )
15 14 ad2antlr ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) )
16 elrege0 ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹𝑃 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑃 ) ) )
17 16 simplbi ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑃 ) ∈ ℝ )
18 15 17 syl ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ∈ ℝ )
19 18 recnd ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ∈ ℂ )
20 simprrl ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) )
21 20 adantr ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) )
22 simprrr ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) )
23 simpl ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) = ( 𝐹𝑅 ) )
24 22 23 breqtrrd ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑄 ) ≤ ( 𝐹𝑃 ) )
25 24 adantr ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑄 ) ≤ ( 𝐹𝑃 ) )
26 simplr2 ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) )
27 26 ad2antlr ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) )
28 elrege0 ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹𝑄 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑄 ) ) )
29 28 simplbi ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑄 ) ∈ ℝ )
30 27 29 syl ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑄 ) ∈ ℝ )
31 18 30 letri3d ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) ↔ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑃 ) ) ) )
32 21 25 31 mpbir2and ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) = ( 𝐹𝑄 ) )
33 simpll ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) = ( 𝐹𝑅 ) )
34 simpll2 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
35 34 adantr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
36 35 ad2antlr ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
37 fveecn ( ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍𝑖 ) ∈ ℂ )
38 36 37 sylancom ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍𝑖 ) ∈ ℂ )
39 simpll3 ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
40 39 adantr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
41 40 ad2antlr ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
42 fveecn ( ( 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈𝑖 ) ∈ ℂ )
43 41 42 sylancom ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈𝑖 ) ∈ ℂ )
44 ax-1cn 1 ∈ ℂ
45 simpl ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝐹𝑃 ) ∈ ℂ )
46 subcl ( ( 1 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ) → ( 1 − ( 𝐹𝑃 ) ) ∈ ℂ )
47 44 45 46 sylancr ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 1 − ( 𝐹𝑃 ) ) ∈ ℂ )
48 simprl ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝑍𝑖 ) ∈ ℂ )
49 47 48 mulcld ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ∈ ℂ )
50 mulcl ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) → ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ∈ ℂ )
51 50 adantrl ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ∈ ℂ )
52 49 51 addcld ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∈ ℂ )
53 52 mulid2d ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) )
54 52 mul02d ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) = 0 )
55 53 54 oveq12d ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) + 0 ) )
56 52 addid1d ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) + 0 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) )
57 55 56 eqtr2d ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ) )
58 57 3adant2 ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) ∧ ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ) )
59 oveq2 ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) → ( 1 − ( 𝐹𝑃 ) ) = ( 1 − ( 𝐹𝑄 ) ) )
60 59 oveq1d ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) → ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) = ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) )
61 oveq1 ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) → ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) = ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) )
62 60 61 oveq12d ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) → ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) )
63 oveq2 ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) → ( 1 − ( 𝐹𝑃 ) ) = ( 1 − ( 𝐹𝑅 ) ) )
64 63 oveq1d ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) → ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) = ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) )
65 oveq1 ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) → ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) = ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) )
66 64 65 oveq12d ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) → ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) )
67 66 oveq2d ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) → ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) = ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
68 67 oveq2d ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) → ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
69 62 68 eqeqan12d ( ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) ∧ ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ) → ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
70 69 3ad2ant2 ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) ∧ ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
71 58 70 mpbid ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( ( 𝐹𝑃 ) = ( 𝐹𝑄 ) ∧ ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
72 19 32 33 38 43 71 syl122anc ( ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
73 72 ralrimiva ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
74 oveq2 ( 𝑡 = 0 → ( 1 − 𝑡 ) = ( 1 − 0 ) )
75 1m0e1 ( 1 − 0 ) = 1
76 74 75 eqtrdi ( 𝑡 = 0 → ( 1 − 𝑡 ) = 1 )
77 76 oveq1d ( 𝑡 = 0 → ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) = ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) )
78 oveq1 ( 𝑡 = 0 → ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) = ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
79 77 78 oveq12d ( 𝑡 = 0 → ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
80 79 eqeq2d ( 𝑡 = 0 → ( ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
81 80 ralbidv ( 𝑡 = 0 → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
82 81 rspcev ( ( 0 ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( 1 · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 0 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
83 13 73 82 sylancr ( ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
84 83 ex ( ( 𝐹𝑃 ) = ( 𝐹𝑅 ) → ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
85 26 adantl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) )
86 85 29 syl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑄 ) ∈ ℝ )
87 simplr3 ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) )
88 87 adantl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) )
89 elrege0 ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹𝑅 ) ∈ ℝ ∧ 0 ≤ ( 𝐹𝑅 ) ) )
90 89 simplbi ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑅 ) ∈ ℝ )
91 88 90 syl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑅 ) ∈ ℝ )
92 14 adantl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) )
93 92 17 syl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) ∈ ℝ )
94 simprrr ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) )
95 86 91 93 94 lesub1dd ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ≤ ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) )
96 86 93 resubcld ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ∈ ℝ )
97 simprrl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) )
98 86 93 subge0d ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 0 ≤ ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ↔ ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ) )
99 97 98 mpbird ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → 0 ≤ ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) )
100 91 93 resubcld ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ∈ ℝ )
101 93 86 91 97 94 letrd ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) ≤ ( 𝐹𝑅 ) )
102 simpl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) )
103 102 necomd ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑅 ) ≠ ( 𝐹𝑃 ) )
104 93 91 101 103 leneltd ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( 𝐹𝑃 ) < ( 𝐹𝑅 ) )
105 93 91 posdifd ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( ( 𝐹𝑃 ) < ( 𝐹𝑅 ) ↔ 0 < ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) )
106 104 105 mpbid ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → 0 < ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) )
107 divelunit ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ) ∧ ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ∈ ℝ ∧ 0 < ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ≤ ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) )
108 96 99 100 106 107 syl22anc ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ∈ ( 0 [,] 1 ) ↔ ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ≤ ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) )
109 95 108 mpbird ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ∈ ( 0 [,] 1 ) )
110 14 ad2antlr ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) )
111 17 recnd ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑃 ) ∈ ℂ )
112 110 111 syl ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ∈ ℂ )
113 simpll ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) )
114 26 ad2antlr ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) )
115 29 recnd ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑄 ) ∈ ℂ )
116 114 115 syl ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑄 ) ∈ ℂ )
117 87 ad2antlr ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) )
118 90 recnd ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) → ( 𝐹𝑅 ) ∈ ℂ )
119 117 118 syl ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹𝑅 ) ∈ ℂ )
120 34 ad2antrl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) )
121 120 37 sylan ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍𝑖 ) ∈ ℂ )
122 39 ad2antrl ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) )
123 122 42 sylan ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( 𝑈𝑖 ) ∈ ℂ )
124 simp2r ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝐹𝑅 ) ∈ ℂ )
125 simp2l ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝐹𝑄 ) ∈ ℂ )
126 124 125 subcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) ∈ ℂ )
127 simp1l ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝐹𝑃 ) ∈ ℂ )
128 44 127 46 sylancr ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 1 − ( 𝐹𝑃 ) ) ∈ ℂ )
129 126 128 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) ∈ ℂ )
130 125 127 subcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ∈ ℂ )
131 subcl ( ( 1 ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) → ( 1 − ( 𝐹𝑅 ) ) ∈ ℂ )
132 44 124 131 sylancr ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 1 − ( 𝐹𝑅 ) ) ∈ ℂ )
133 130 132 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ∈ ℂ )
134 124 127 subcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ∈ ℂ )
135 simp1r ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) )
136 135 necomd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝐹𝑅 ) ≠ ( 𝐹𝑃 ) )
137 124 127 136 subne0d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ≠ 0 )
138 129 133 134 137 divdird ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) )
139 134 mulid1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · 1 ) = ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) )
140 134 125 mulcomd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) = ( ( 𝐹𝑄 ) · ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) )
141 125 124 127 subdid ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑄 ) · ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) )
142 140 141 eqtrd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) = ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) )
143 139 142 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) ) = ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) − ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ) )
144 subdi ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑄 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) ) )
145 44 144 mp3an2 ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑄 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) ) )
146 134 125 145 syl2anc ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑄 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) ) )
147 subdi ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) ) )
148 44 147 mp3an2 ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) ∈ ℂ ∧ ( 𝐹𝑃 ) ∈ ℂ ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) ) )
149 126 127 148 syl2anc ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) ) )
150 126 mulid1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · 1 ) = ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) )
151 124 125 127 subdird ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) = ( ( ( 𝐹𝑅 ) · ( 𝐹𝑃 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) )
152 124 127 mulcomd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑅 ) · ( 𝐹𝑃 ) ) = ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) )
153 152 oveq1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) · ( 𝐹𝑃 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) = ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) )
154 151 153 eqtrd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) = ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) )
155 150 154 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · 1 ) − ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) ) = ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) − ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ) )
156 149 155 eqtrd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) = ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) − ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ) )
157 subdi ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) )
158 44 157 mp3an2 ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) )
159 130 124 158 syl2anc ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) )
160 130 mulid1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · 1 ) = ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) )
161 125 127 124 subdird ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) = ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) )
162 160 161 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · 1 ) − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) − ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) )
163 159 162 eqtrd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) − ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) )
164 156 163 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) − ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) − ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) ) )
165 127 124 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ∈ ℂ )
166 125 127 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ∈ ℂ )
167 165 166 subcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ∈ ℂ )
168 mulcl ( ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) → ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) ∈ ℂ )
169 168 3ad2ant2 ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) ∈ ℂ )
170 169 165 subcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ∈ ℂ )
171 126 130 167 170 addsub4d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) + ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ) − ( ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) − ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) − ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) ) )
172 124 125 127 npncand ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) + ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ) = ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) )
173 165 166 169 npncan3d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) = ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) )
174 172 173 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) + ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ) − ( ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) ) = ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) − ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ) )
175 164 171 174 3eqtr2d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) = ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) − ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) ) )
176 143 146 175 3eqtr4d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑄 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) )
177 129 133 addcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) ∈ ℂ )
178 subcl ( ( 1 ∈ ℂ ∧ ( 𝐹𝑄 ) ∈ ℂ ) → ( 1 − ( 𝐹𝑄 ) ) ∈ ℂ )
179 44 125 178 sylancr ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 1 − ( 𝐹𝑄 ) ) ∈ ℂ )
180 177 134 179 137 divmuld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( 1 − ( 𝐹𝑄 ) ) ↔ ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑄 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) ) )
181 176 180 mpbird ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( 1 − ( 𝐹𝑄 ) ) )
182 126 128 134 137 div23d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) )
183 134 130 134 137 divsubdird ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) − ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) )
184 124 125 127 nnncan2d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) − ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ) = ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) )
185 184 oveq1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) − ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) )
186 134 137 dividd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = 1 )
187 186 oveq1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) = ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) )
188 183 185 187 3eqtr3d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) )
189 188 oveq1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) = ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) )
190 182 189 eqtrd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) )
191 130 132 134 137 div23d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) )
192 190 191 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 1 − ( 𝐹𝑃 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 1 − ( 𝐹𝑅 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) )
193 138 181 192 3eqtr3d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 1 − ( 𝐹𝑄 ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) )
194 193 oveq1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) = ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) · ( 𝑍𝑖 ) ) )
195 126 127 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) ∈ ℂ )
196 130 124 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ∈ ℂ )
197 195 196 134 137 divdird ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) )
198 154 161 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) = ( ( ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑄 ) · ( 𝐹𝑃 ) ) ) + ( ( ( 𝐹𝑄 ) · ( 𝐹𝑅 ) ) − ( ( 𝐹𝑃 ) · ( 𝐹𝑅 ) ) ) ) )
199 173 198 142 3eqtr4rd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) )
200 195 196 addcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) ∈ ℂ )
201 200 134 125 137 divmuld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( 𝐹𝑄 ) ↔ ( ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑄 ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) ) )
202 199 201 mpbird ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) + ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( 𝐹𝑄 ) )
203 126 127 134 137 div23d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑃 ) ) )
204 188 oveq1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑃 ) ) = ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) )
205 203 204 eqtrd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) )
206 130 124 134 137 div23d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) )
207 205 206 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑅 ) − ( 𝐹𝑄 ) ) · ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) · ( 𝐹𝑅 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ) )
208 197 202 207 3eqtr3d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝐹𝑄 ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ) )
209 208 oveq1d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) = ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ) · ( 𝑈𝑖 ) ) )
210 194 209 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) · ( 𝑍𝑖 ) ) + ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ) · ( 𝑈𝑖 ) ) ) )
211 130 134 137 divcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ∈ ℂ )
212 subcl ( ( 1 ∈ ℂ ∧ ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ∈ ℂ ) → ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) ∈ ℂ )
213 44 211 212 sylancr ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) ∈ ℂ )
214 simp3l ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝑍𝑖 ) ∈ ℂ )
215 128 214 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ∈ ℂ )
216 213 215 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) ∈ ℂ )
217 132 214 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ∈ ℂ )
218 211 217 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) ∈ ℂ )
219 simp3r ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( 𝑈𝑖 ) ∈ ℂ )
220 127 219 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ∈ ℂ )
221 213 220 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∈ ℂ )
222 124 219 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ∈ ℂ )
223 211 222 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ∈ ℂ )
224 216 218 221 223 add4d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) ) + ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) + ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
225 213 128 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) ∈ ℂ )
226 211 132 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ∈ ℂ )
227 213 128 214 mulassd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) · ( 𝑍𝑖 ) ) = ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) )
228 211 132 214 mulassd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) )
229 227 228 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) · ( 𝑍𝑖 ) ) + ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) · ( 𝑍𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) ) )
230 225 214 226 229 joinlmuladdmuld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) · ( 𝑍𝑖 ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) ) )
231 213 127 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) ∈ ℂ )
232 211 124 mulcld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ∈ ℂ )
233 213 127 219 mulassd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) · ( 𝑈𝑖 ) ) = ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) )
234 211 124 219 mulassd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) · ( 𝑈𝑖 ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) )
235 233 234 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) · ( 𝑈𝑖 ) ) + ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
236 231 219 232 235 joinlmuladdmuld ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ) · ( 𝑈𝑖 ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
237 230 236 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) · ( 𝑍𝑖 ) ) + ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ) · ( 𝑈𝑖 ) ) ) = ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) ) + ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
238 213 215 220 adddid ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) + ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) )
239 211 217 222 adddid ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) = ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
240 238 239 oveq12d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) ) + ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
241 224 237 240 3eqtr4rd ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 1 − ( 𝐹𝑃 ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 1 − ( 𝐹𝑅 ) ) ) ) · ( 𝑍𝑖 ) ) + ( ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( 𝐹𝑃 ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( 𝐹𝑅 ) ) ) · ( 𝑈𝑖 ) ) ) )
242 210 241 eqtr4d ( ( ( ( 𝐹𝑃 ) ∈ ℂ ∧ ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ) ∧ ( ( 𝐹𝑄 ) ∈ ℂ ∧ ( 𝐹𝑅 ) ∈ ℂ ) ∧ ( ( 𝑍𝑖 ) ∈ ℂ ∧ ( 𝑈𝑖 ) ∈ ℂ ) ) → ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
243 112 113 116 119 121 123 242 syl222anc ( ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
244 243 ralrimiva ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
245 oveq2 ( 𝑡 = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) → ( 1 − 𝑡 ) = ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) )
246 245 oveq1d ( 𝑡 = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) → ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) = ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) )
247 oveq1 ( 𝑡 = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) → ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) = ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
248 246 247 oveq12d ( 𝑡 = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) → ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
249 248 eqeq2d ( 𝑡 = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) → ( ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
250 249 ralbidv ( 𝑡 = ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
251 250 rspcev ( ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ∈ ( 0 [,] 1 ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( ( ( ( 𝐹𝑄 ) − ( 𝐹𝑃 ) ) / ( ( 𝐹𝑅 ) − ( 𝐹𝑃 ) ) ) · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
252 109 244 251 syl2anc ( ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) ∧ ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
253 252 ex ( ( 𝐹𝑃 ) ≠ ( 𝐹𝑅 ) → ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
254 84 253 pm2.61ine ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
255 r19.26-3 ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
256 simp2 ( ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) )
257 oveq2 ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) → ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) = ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) )
258 oveq2 ( ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) → ( 𝑡 · ( 𝑅𝑖 ) ) = ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) )
259 257 258 oveqan12d ( ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
260 259 3adant2 ( ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) )
261 256 260 eqeq12d ( ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ( ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
262 261 ralimi ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
263 ralbi ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ↔ ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
264 262 263 syl ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
265 264 rexbidv ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) ) )
266 265 biimprcd ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
267 255 266 syl5bir ( ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) = ( ( ( 1 − 𝑡 ) · ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) + ( 𝑡 · ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
268 254 267 syl ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
269 268 an32s ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) ∧ ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
270 269 expimpd ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
271 270 adantlr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
272 12 271 syl5bi ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( ( ( ( 𝐹𝑃 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑃𝑖 ) = ( ( ( 1 − ( 𝐹𝑃 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑃 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑄 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − ( 𝐹𝑄 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑄 ) · ( 𝑈𝑖 ) ) ) ) ∧ ( ( 𝐹𝑅 ) ∈ ( 0 [,) +∞ ) ∧ ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑅𝑖 ) = ( ( ( 1 − ( 𝐹𝑅 ) ) · ( 𝑍𝑖 ) ) + ( ( 𝐹𝑅 ) · ( 𝑈𝑖 ) ) ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
273 11 272 mpd ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) )
274 simpl1 ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) → 𝑁 ∈ ℕ )
275 1 ssrab3 𝐷 ⊆ ( 𝔼 ‘ 𝑁 )
276 275 sseli ( 𝑄𝐷𝑄 ∈ ( 𝔼 ‘ 𝑁 ) )
277 275 sseli ( 𝑃𝐷𝑃 ∈ ( 𝔼 ‘ 𝑁 ) )
278 275 sseli ( 𝑅𝐷𝑅 ∈ ( 𝔼 ‘ 𝑁 ) )
279 276 277 278 3anim123i ( ( 𝑄𝐷𝑃𝐷𝑅𝐷 ) → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) )
280 279 3com12 ( ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) → ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) )
281 brbtwn ( ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( 𝑄 Btwn ⟨ 𝑃 , 𝑅 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
282 281 adantl ( ( 𝑁 ∈ ℕ ∧ ( 𝑄 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑃 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( 𝑄 Btwn ⟨ 𝑃 , 𝑅 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
283 274 280 282 syl2an ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) → ( 𝑄 Btwn ⟨ 𝑃 , 𝑅 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
284 283 adantr ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → ( 𝑄 Btwn ⟨ 𝑃 , 𝑅 ⟩ ↔ ∃ 𝑡 ∈ ( 0 [,] 1 ) ∀ 𝑖 ∈ ( 1 ... 𝑁 ) ( 𝑄𝑖 ) = ( ( ( 1 − 𝑡 ) · ( 𝑃𝑖 ) ) + ( 𝑡 · ( 𝑅𝑖 ) ) ) ) )
285 273 284 mpbird ( ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) ∧ ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) ) → 𝑄 Btwn ⟨ 𝑃 , 𝑅 ⟩ )
286 285 ex ( ( ( ( 𝑁 ∈ ℕ ∧ 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝑈 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ 𝑍𝑈 ) ∧ ( 𝑃𝐷𝑄𝐷𝑅𝐷 ) ) → ( ( ( 𝐹𝑃 ) ≤ ( 𝐹𝑄 ) ∧ ( 𝐹𝑄 ) ≤ ( 𝐹𝑅 ) ) → 𝑄 Btwn ⟨ 𝑃 , 𝑅 ⟩ ) )