Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axcontlem8 Structured version   Visualization version   GIF version

Theorem axcontlem8 26759
 Description: Lemma for axcont 26764. A point in 𝐷 is between two others if its function value falls in the middle. (Contributed by Scott Fenton, 18-Jun-2013.)
Hypotheses
Ref Expression
axcontlem8.1 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
axcontlem8.2 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
Assertion
Ref Expression
axcontlem8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))
Distinct variable groups:   𝐷,𝑝,𝑡,𝑥   𝐹,𝑝,𝑖,𝑡   𝑥,𝑖,𝑁,𝑝,𝑡   𝑃,𝑖,𝑝,𝑡,𝑥   𝑄,𝑖,𝑝,𝑡,𝑥   𝑅,𝑖,𝑝,𝑡,𝑥   𝑈,𝑖,𝑝,𝑡,𝑥   𝑖,𝑍,𝑝,𝑡,𝑥
Allowed substitution hints:   𝐷(𝑖)   𝐹(𝑥)

Proof of Theorem axcontlem8
StepHypRef Expression
1 axcontlem8.1 . . . . . . . . 9 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
2 axcontlem8.2 . . . . . . . . 9 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥𝑖) = (((1 − 𝑡) · (𝑍𝑖)) + (𝑡 · (𝑈𝑖)))))}
31, 2axcontlem6 26757 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑃𝐷) → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
43ex 415 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑃𝐷 → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
51, 2axcontlem6 26757 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑄𝐷) → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
65ex 415 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑄𝐷 → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
71, 2axcontlem6 26757 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑅𝐷) → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
87ex 415 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑅𝐷 → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
94, 6, 83anim123d 1439 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ((𝑃𝐷𝑄𝐷𝑅𝐷) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
109imp 409 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
1110adantr 483 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
12 3an6 1442 . . . . 5 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
13 0elunit 12858 . . . . . . . . . . . 12 0 ∈ (0[,]1)
14 simplr1 1211 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑃) ∈ (0[,)+∞))
1514ad2antlr 725 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
16 elrege0 12845 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) ∈ (0[,)+∞) ↔ ((𝐹𝑃) ∈ ℝ ∧ 0 ≤ (𝐹𝑃)))
1716simplbi 500 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℝ)
1815, 17syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℝ)
1918recnd 10671 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
20 simprrl 779 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
2120adantr 483 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≤ (𝐹𝑄))
22 simprrr 780 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
23 simpl 485 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) = (𝐹𝑅))
2422, 23breqtrrd 5096 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑃))
2524adantr 483 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ≤ (𝐹𝑃))
26 simplr2 1212 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑄) ∈ (0[,)+∞))
2726ad2antlr 725 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
28 elrege0 12845 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑄) ∈ (0[,)+∞) ↔ ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
2928simplbi 500 . . . . . . . . . . . . . . . . 17 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℝ)
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℝ)
3118, 30letri3d 10784 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹𝑃) = (𝐹𝑄) ↔ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑃))))
3221, 25, 31mpbir2and 711 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑄))
33 simpll 765 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑅))
34 simpll2 1209 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
3534adantr 483 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
3635ad2antlr 725 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37 fveecn 26690 . . . . . . . . . . . . . . 15 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3836, 37sylancom 590 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
39 simpll3 1210 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
4039adantr 483 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
4140ad2antlr 725 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42 fveecn 26690 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
4341, 42sylancom 590 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
44 ax-1cn 10597 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
45 simpl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
46 subcl 10887 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (1 − (𝐹𝑃)) ∈ ℂ)
4744, 45, 46sylancr 589 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
48 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
4947, 48mulcld 10663 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
50 mulcl 10623 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5150adantrl 714 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5249, 51addcld 10662 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
5352mulid2d 10661 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5452mul02d 10840 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = 0)
5553, 54oveq12d 7176 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0))
5652addid1d 10842 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5755, 56eqtr2d 2859 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
58573adant2 1127 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
59 oveq2 7166 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑄) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑄)))
6059oveq1d 7173 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑄)) · (𝑍𝑖)))
61 oveq1 7165 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑄) · (𝑈𝑖)))
6260, 61oveq12d 7176 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑄) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
63 oveq2 7166 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑃) = (𝐹𝑅) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑅)))
6463oveq1d 7173 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑅)) · (𝑍𝑖)))
65 oveq1 7165 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑅) · (𝑈𝑖)))
6664, 65oveq12d 7176 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑅) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))
6766oveq2d 7174 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑅) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
6867oveq2d 7174 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑅) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
6962, 68eqeqan12d 2840 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
70693ad2ant2 1130 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
7158, 70mpbid 234 . . . . . . . . . . . . . 14 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7219, 32, 33, 38, 43, 71syl122anc 1375 . . . . . . . . . . . . 13 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7372ralrimiva 3184 . . . . . . . . . . . 12 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
74 oveq2 7166 . . . . . . . . . . . . . . . . . 18 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75 1m0e1 11761 . . . . . . . . . . . . . . . . . 18 (1 − 0) = 1
7674, 75syl6eq 2874 . . . . . . . . . . . . . . . . 17 (𝑡 = 0 → (1 − 𝑡) = 1)
7776oveq1d 7173 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
78 oveq1 7165 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
7977, 78oveq12d 7176 . . . . . . . . . . . . . . 15 (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8079eqeq2d 2834 . . . . . . . . . . . . . 14 (𝑡 = 0 → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8180ralbidv 3199 . . . . . . . . . . . . 13 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8281rspcev 3625 . . . . . . . . . . . 12 ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8313, 73, 82sylancr 589 . . . . . . . . . . 11 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8483ex 415 . . . . . . . . . 10 ((𝐹𝑃) = (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8526adantl 484 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ (0[,)+∞))
8685, 29syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ ℝ)
87 simplr3 1213 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑅) ∈ (0[,)+∞))
8887adantl 484 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ (0[,)+∞))
89 elrege0 12845 . . . . . . . . . . . . . . . 16 ((𝐹𝑅) ∈ (0[,)+∞) ↔ ((𝐹𝑅) ∈ ℝ ∧ 0 ≤ (𝐹𝑅)))
9089simplbi 500 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℝ)
9188, 90syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ ℝ)
9214adantl 484 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ (0[,)+∞))
9392, 17syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ ℝ)
94 simprrr 780 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
9586, 91, 93, 94lesub1dd 11258 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃)))
9686, 93resubcld 11070 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ)
97 simprrl 779 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
9886, 93subge0d 11232 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (0 ≤ ((𝐹𝑄) − (𝐹𝑃)) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
9997, 98mpbird 259 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 ≤ ((𝐹𝑄) − (𝐹𝑃)))
10091, 93resubcld 11070 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ)
10193, 86, 91, 97, 94letrd 10799 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑅))
102 simpl 485 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≠ (𝐹𝑅))
103102necomd 3073 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ≠ (𝐹𝑃))
10493, 91, 101, 103leneltd 10796 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) < (𝐹𝑅))
10593, 91posdifd 11229 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑃) < (𝐹𝑅) ↔ 0 < ((𝐹𝑅) − (𝐹𝑃))))
106104, 105mpbid 234 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 < ((𝐹𝑅) − (𝐹𝑃)))
107 divelunit 12883 . . . . . . . . . . . . . 14 (((((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑄) − (𝐹𝑃))) ∧ (((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ ∧ 0 < ((𝐹𝑅) − (𝐹𝑃)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10896, 99, 100, 106, 107syl22anc 836 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10995, 108mpbird 259 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1))
11014ad2antlr 725 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
11117recnd 10671 . . . . . . . . . . . . . . 15 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℂ)
112110, 111syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
113 simpll 765 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≠ (𝐹𝑅))
11426ad2antlr 725 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
11529recnd 10671 . . . . . . . . . . . . . . 15 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℂ)
116114, 115syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℂ)
11787ad2antlr 725 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ (0[,)+∞))
11890recnd 10671 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℂ)
119117, 118syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ ℂ)
12034ad2antrl 726 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
121120, 37sylan 582 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
12239ad2antrl 726 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
123122, 42sylan 582 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
124 simp2r 1196 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ∈ ℂ)
125 simp2l 1195 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) ∈ ℂ)
126124, 125subcld 10999 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ)
127 simp1l 1193 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
12844, 127, 46sylancr 589 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
129126, 128mulcld 10663 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) ∈ ℂ)
130125, 127subcld 10999 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ)
131 subcl 10887 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (1 − (𝐹𝑅)) ∈ ℂ)
13244, 124, 131sylancr 589 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑅)) ∈ ℂ)
133130, 132mulcld 10663 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) ∈ ℂ)
134124, 127subcld 10999 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ)
135 simp1r 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ≠ (𝐹𝑅))
136135necomd 3073 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ≠ (𝐹𝑃))
137124, 127, 136subne0d 11008 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ≠ 0)
138129, 133, 134, 137divdird 11456 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))))
139134mulid1d 10660 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · 1) = ((𝐹𝑅) − (𝐹𝑃)))
140134, 125mulcomd 10664 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))))
141125, 124, 127subdid 11098 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
142140, 141eqtrd 2858 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
143139, 142oveq12d 7176 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
144 subdi 11075 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
14544, 144mp3an2 1445 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
146134, 125, 145syl2anc 586 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
147 subdi 11075 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
14844, 147mp3an2 1445 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
149126, 127, 148syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
150126mulid1d 10660 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · 1) = ((𝐹𝑅) − (𝐹𝑄)))
151124, 125, 127subdird 11099 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))))
152124, 127mulcomd 10664 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝐹𝑃)) = ((𝐹𝑃) · (𝐹𝑅)))
153152oveq1d 7173 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
154151, 153eqtrd 2858 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
155150, 154oveq12d 7176 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
156149, 155eqtrd 2858 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
157 subdi 11075 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
15844, 157mp3an2 1445 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
159130, 124, 158syl2anc 586 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
160130mulid1d 10660 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · 1) = ((𝐹𝑄) − (𝐹𝑃)))
161125, 127, 124subdird 11099 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))
162160, 161oveq12d 7176 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
163159, 162eqtrd 2858 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
164156, 163oveq12d 7176 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
165127, 124mulcld 10663 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝐹𝑅)) ∈ ℂ)
166125, 127mulcld 10663 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑃)) ∈ ℂ)
167165, 166subcld 10999 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) ∈ ℂ)
168 mulcl 10623 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
1691683ad2ant2 1130 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
170169, 165subcld 10999 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))) ∈ ℂ)
171126, 130, 167, 170addsub4d 11046 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
172124, 125, 127npncand 11023 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑃)))
173165, 166, 169npncan3d 11035 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
174172, 173oveq12d 7176 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
175164, 171, 1743eqtr2d 2864 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
176143, 146, 1753eqtr4d 2868 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))))
177129, 133addcld 10662 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) ∈ ℂ)
178 subcl 10887 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑄)) ∈ ℂ)
17944, 125, 178sylancr 589 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) ∈ ℂ)
180177, 134, 179, 137divmuld 11440 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))))))
181176, 180mpbird 259 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)))
182126, 128, 134, 137div23d 11455 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))))
183134, 130, 134, 137divsubdird 11457 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
184124, 125, 127nnncan2d 11034 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑄)))
185184oveq1d 7173 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))))
186134, 137dividd 11416 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = 1)
187186oveq1d 7173 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
188183, 185, 1873eqtr3d 2866 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
189188oveq1d 7173 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
190182, 189eqtrd 2858 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
191130, 132, 134, 137div23d 11455 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))))
192190, 191oveq12d 7176 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
193138, 181, 1923eqtr3d 2866 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
194193oveq1d 7173 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑄)) · (𝑍𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)))
195126, 127mulcld 10663 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) ∈ ℂ)
196130, 124mulcld 10663 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) ∈ ℂ)
197195, 196, 134, 137divdird 11456 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))))
198154, 161oveq12d 7176 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
199173, 198, 1423eqtr4rd 2869 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
200195, 196addcld 10662 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) ∈ ℂ)
201200, 134, 125, 137divmuld 11440 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)))))
202199, 201mpbird 259 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄))
203126, 127, 134, 137div23d 11455 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)))
204188oveq1d 7173 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
205203, 204eqtrd 2858 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
206130, 124, 134, 137div23d 11455 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)))
207205, 206oveq12d 7176 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
208197, 202, 2073eqtr3d 2866 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
209208oveq1d 7173 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝑈𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)))
210194, 209oveq12d 7176 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
211130, 134, 137divcld 11418 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ)
212 subcl 10887 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
21344, 211, 212sylancr 589 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
214 simp3l 1197 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
215128, 214mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
216213, 215mulcld 10663 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) ∈ ℂ)
217132, 214mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑅)) · (𝑍𝑖)) ∈ ℂ)
218211, 217mulcld 10663 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) ∈ ℂ)
219 simp3r 1198 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
220127, 219mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
221213, 220mulcld 10663 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
222124, 219mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝑈𝑖)) ∈ ℂ)
223211, 222mulcld 10663 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))) ∈ ℂ)
224216, 218, 221, 223add4d 10870 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
225213, 128mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) ∈ ℂ)
226211, 132mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) ∈ ℂ)
227213, 128, 214mulassd 10666 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))))
228211, 132, 214mulassd 10666 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))))
229227, 228oveq12d 7176 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
230225, 214, 226, 229joinlmuladdmuld 10670 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
231213, 127mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) ∈ ℂ)
232211, 124mulcld 10663 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) ∈ ℂ)
233213, 127, 219mulassd 10666 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))))
234211, 124, 219mulassd 10666 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))
235233, 234oveq12d 7176 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
236231, 219, 232, 235joinlmuladdmuld 10670 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
237230, 236oveq12d 7176 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
238213, 215, 220adddid 10667 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))))
239211, 217, 222adddid 10667 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
240238, 239oveq12d 7176 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
241224, 237, 2403eqtr4rd 2869 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
242210, 241eqtr4d 2861 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
243112, 113, 116, 119, 121, 123, 242syl222anc 1382 . . . . . . . . . . . . 13 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
244243ralrimiva 3184 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
245 oveq2 7166 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (1 − 𝑡) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
246245oveq1d 7173 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
247 oveq1 7165 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
248246, 247oveq12d 7176 . . . . . . . . . . . . . . 15 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
249248eqeq2d 2834 . . . . . . . . . . . . . 14 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
250249ralbidv 3199 . . . . . . . . . . . . 13 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
251250rspcev 3625 . . . . . . . . . . . 12 (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
252109, 244, 251syl2anc 586 . . . . . . . . . . 11 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
253252ex 415 . . . . . . . . . 10 ((𝐹𝑃) ≠ (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
25484, 253pm2.61ine 3102 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
255 r19.26-3 3174 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
256 simp2 1133 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
257 oveq2 7166 . . . . . . . . . . . . . . . . 17 ((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) → ((1 − 𝑡) · (𝑃𝑖)) = ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
258 oveq2 7166 . . . . . . . . . . . . . . . . 17 ((𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))) → (𝑡 · (𝑅𝑖)) = (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
259257, 258oveqan12d 7177 . . . . . . . . . . . . . . . 16 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
2602593adant2 1127 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
261256, 260eqeq12d 2839 . . . . . . . . . . . . . 14 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
262261ralimi 3162 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
263 ralbi 3169 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
264262, 263syl 17 . . . . . . . . . . . 12 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
265264rexbidv 3299 . . . . . . . . . . 11 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
266265biimprcd 252 . . . . . . . . . 10 (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
267255, 266syl5bir 245 . . . . . . . . 9 (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
268254, 267syl 17 . . . . . . . 8 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
269268an32s 650 . . . . . . 7 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
270269expimpd 456 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
271270adantlr 713 . . . . 5 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27212, 271syl5bi 244 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27311, 272mpd 15 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))))
274 simpl1 1187 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑁 ∈ ℕ)
2751ssrab3 4059 . . . . . . . 8 𝐷 ⊆ (𝔼‘𝑁)
276275sseli 3965 . . . . . . 7 (𝑄𝐷𝑄 ∈ (𝔼‘𝑁))
277275sseli 3965 . . . . . . 7 (𝑃𝐷𝑃 ∈ (𝔼‘𝑁))
278275sseli 3965 . . . . . . 7 (𝑅𝐷𝑅 ∈ (𝔼‘𝑁))
279276, 277, 2783anim123i 1147 . . . . . 6 ((𝑄𝐷𝑃𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
2802793com12 1119 . . . . 5 ((𝑃𝐷𝑄𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
281 brbtwn 26687 . . . . . 6 ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
282281adantl 484 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
283274, 280, 282syl2an 597 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
284283adantr 483 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
285273, 284mpbird 259 . 2 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
286285ex 415 1 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  ∀wral 3140  ∃wrex 3141  {crab 3144  ⟨cop 4575   class class class wbr 5068  {copab 5130  ‘cfv 6357  (class class class)co 7158  ℂcc 10537  ℝcr 10538  0cc0 10539  1c1 10540   + caddc 10542   · cmul 10544  +∞cpnf 10674   < clt 10677   ≤ cle 10678   − cmin 10872   / cdiv 11299  ℕcn 11640  [,)cico 12743  [,]cicc 12744  ...cfz 12895  𝔼cee 26676   Btwn cbtwn 26677 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-er 8291  df-map 8410  df-en 8512  df-dom 8513  df-sdom 8514  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-div 11300  df-nn 11641  df-z 11985  df-uz 12247  df-ico 12747  df-icc 12748  df-fz 12896  df-ee 26679  df-btwn 26680 This theorem is referenced by:  axcontlem10  26761
 Copyright terms: Public domain W3C validator