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

Theorem axcontlem8 27067
Description: Lemma for axcont 27072. 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 27065 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑃𝐷) → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
43ex 416 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑃𝐷 → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
51, 2axcontlem6 27065 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑄𝐷) → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
65ex 416 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑄𝐷 → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
71, 2axcontlem6 27065 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑅𝐷) → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
87ex 416 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑅𝐷 → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
94, 6, 83anim123d 1445 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ((𝑃𝐷𝑄𝐷𝑅𝐷) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
109imp 410 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
1110adantr 484 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
12 3an6 1448 . . . . 5 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
13 0elunit 13062 . . . . . . . . . . . 12 0 ∈ (0[,]1)
14 simplr1 1217 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑃) ∈ (0[,)+∞))
1514ad2antlr 727 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
16 elrege0 13047 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) ∈ (0[,)+∞) ↔ ((𝐹𝑃) ∈ ℝ ∧ 0 ≤ (𝐹𝑃)))
1716simplbi 501 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℝ)
1815, 17syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℝ)
1918recnd 10866 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
20 simprrl 781 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
2120adantr 484 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≤ (𝐹𝑄))
22 simprrr 782 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
23 simpl 486 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) = (𝐹𝑅))
2422, 23breqtrrd 5086 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑃))
2524adantr 484 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ≤ (𝐹𝑃))
26 simplr2 1218 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑄) ∈ (0[,)+∞))
2726ad2antlr 727 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
28 elrege0 13047 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑄) ∈ (0[,)+∞) ↔ ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
2928simplbi 501 . . . . . . . . . . . . . . . . 17 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℝ)
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℝ)
3118, 30letri3d 10979 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹𝑃) = (𝐹𝑄) ↔ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑃))))
3221, 25, 31mpbir2and 713 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑄))
33 simpll 767 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑅))
34 simpll2 1215 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
3534adantr 484 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
3635ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37 fveecn 26998 . . . . . . . . . . . . . . 15 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3836, 37sylancom 591 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
39 simpll3 1216 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
4039adantr 484 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
4140ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42 fveecn 26998 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
4341, 42sylancom 591 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
44 ax-1cn 10792 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
45 simpl 486 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
46 subcl 11082 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (1 − (𝐹𝑃)) ∈ ℂ)
4744, 45, 46sylancr 590 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
48 simprl 771 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
4947, 48mulcld 10858 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
50 mulcl 10818 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5150adantrl 716 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5249, 51addcld 10857 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
5352mulid2d 10856 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5452mul02d 11035 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = 0)
5553, 54oveq12d 7236 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0))
5652addid1d 11037 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5755, 56eqtr2d 2778 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
58573adant2 1133 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
59 oveq2 7226 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑄) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑄)))
6059oveq1d 7233 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑄)) · (𝑍𝑖)))
61 oveq1 7225 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑄) · (𝑈𝑖)))
6260, 61oveq12d 7236 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑄) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
63 oveq2 7226 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑃) = (𝐹𝑅) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑅)))
6463oveq1d 7233 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑅)) · (𝑍𝑖)))
65 oveq1 7225 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑅) · (𝑈𝑖)))
6664, 65oveq12d 7236 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑅) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))
6766oveq2d 7234 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑅) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
6867oveq2d 7234 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑅) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
6962, 68eqeqan12d 2751 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
70693ad2ant2 1136 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
7158, 70mpbid 235 . . . . . . . . . . . . . 14 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7219, 32, 33, 38, 43, 71syl122anc 1381 . . . . . . . . . . . . 13 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7372ralrimiva 3105 . . . . . . . . . . . 12 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
74 oveq2 7226 . . . . . . . . . . . . . . . . . 18 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75 1m0e1 11956 . . . . . . . . . . . . . . . . . 18 (1 − 0) = 1
7674, 75eqtrdi 2794 . . . . . . . . . . . . . . . . 17 (𝑡 = 0 → (1 − 𝑡) = 1)
7776oveq1d 7233 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
78 oveq1 7225 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
7977, 78oveq12d 7236 . . . . . . . . . . . . . . 15 (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8079eqeq2d 2748 . . . . . . . . . . . . . 14 (𝑡 = 0 → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8180ralbidv 3118 . . . . . . . . . . . . 13 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8281rspcev 3542 . . . . . . . . . . . 12 ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8313, 73, 82sylancr 590 . . . . . . . . . . 11 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8483ex 416 . . . . . . . . . 10 ((𝐹𝑃) = (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8526adantl 485 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ (0[,)+∞))
8685, 29syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ ℝ)
87 simplr3 1219 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑅) ∈ (0[,)+∞))
8887adantl 485 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ (0[,)+∞))
89 elrege0 13047 . . . . . . . . . . . . . . . 16 ((𝐹𝑅) ∈ (0[,)+∞) ↔ ((𝐹𝑅) ∈ ℝ ∧ 0 ≤ (𝐹𝑅)))
9089simplbi 501 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℝ)
9188, 90syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ ℝ)
9214adantl 485 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ (0[,)+∞))
9392, 17syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ ℝ)
94 simprrr 782 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
9586, 91, 93, 94lesub1dd 11453 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃)))
9686, 93resubcld 11265 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ)
97 simprrl 781 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
9886, 93subge0d 11427 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (0 ≤ ((𝐹𝑄) − (𝐹𝑃)) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
9997, 98mpbird 260 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 ≤ ((𝐹𝑄) − (𝐹𝑃)))
10091, 93resubcld 11265 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ)
10193, 86, 91, 97, 94letrd 10994 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑅))
102 simpl 486 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≠ (𝐹𝑅))
103102necomd 2996 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ≠ (𝐹𝑃))
10493, 91, 101, 103leneltd 10991 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) < (𝐹𝑅))
10593, 91posdifd 11424 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑃) < (𝐹𝑅) ↔ 0 < ((𝐹𝑅) − (𝐹𝑃))))
106104, 105mpbid 235 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 < ((𝐹𝑅) − (𝐹𝑃)))
107 divelunit 13087 . . . . . . . . . . . . . 14 (((((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑄) − (𝐹𝑃))) ∧ (((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ ∧ 0 < ((𝐹𝑅) − (𝐹𝑃)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10896, 99, 100, 106, 107syl22anc 839 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10995, 108mpbird 260 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1))
11014ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
11117recnd 10866 . . . . . . . . . . . . . . 15 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℂ)
112110, 111syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
113 simpll 767 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≠ (𝐹𝑅))
11426ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
11529recnd 10866 . . . . . . . . . . . . . . 15 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℂ)
116114, 115syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℂ)
11787ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ (0[,)+∞))
11890recnd 10866 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℂ)
119117, 118syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ ℂ)
12034ad2antrl 728 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
121120, 37sylan 583 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
12239ad2antrl 728 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
123122, 42sylan 583 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
124 simp2r 1202 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ∈ ℂ)
125 simp2l 1201 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) ∈ ℂ)
126124, 125subcld 11194 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ)
127 simp1l 1199 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
12844, 127, 46sylancr 590 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
129126, 128mulcld 10858 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) ∈ ℂ)
130125, 127subcld 11194 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ)
131 subcl 11082 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (1 − (𝐹𝑅)) ∈ ℂ)
13244, 124, 131sylancr 590 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑅)) ∈ ℂ)
133130, 132mulcld 10858 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) ∈ ℂ)
134124, 127subcld 11194 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ)
135 simp1r 1200 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ≠ (𝐹𝑅))
136135necomd 2996 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ≠ (𝐹𝑃))
137124, 127, 136subne0d 11203 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ≠ 0)
138129, 133, 134, 137divdird 11651 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))))
139134mulid1d 10855 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · 1) = ((𝐹𝑅) − (𝐹𝑃)))
140134, 125mulcomd 10859 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))))
141125, 124, 127subdid 11293 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
142140, 141eqtrd 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
143139, 142oveq12d 7236 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
144 subdi 11270 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
14544, 144mp3an2 1451 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
146134, 125, 145syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
147 subdi 11270 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
14844, 147mp3an2 1451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
149126, 127, 148syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
150126mulid1d 10855 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · 1) = ((𝐹𝑅) − (𝐹𝑄)))
151124, 125, 127subdird 11294 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))))
152124, 127mulcomd 10859 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝐹𝑃)) = ((𝐹𝑃) · (𝐹𝑅)))
153152oveq1d 7233 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
154151, 153eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
155150, 154oveq12d 7236 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
156149, 155eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
157 subdi 11270 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
15844, 157mp3an2 1451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
159130, 124, 158syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
160130mulid1d 10855 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · 1) = ((𝐹𝑄) − (𝐹𝑃)))
161125, 127, 124subdird 11294 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))
162160, 161oveq12d 7236 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
163159, 162eqtrd 2777 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
164156, 163oveq12d 7236 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
165127, 124mulcld 10858 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝐹𝑅)) ∈ ℂ)
166125, 127mulcld 10858 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑃)) ∈ ℂ)
167165, 166subcld 11194 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) ∈ ℂ)
168 mulcl 10818 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
1691683ad2ant2 1136 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
170169, 165subcld 11194 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))) ∈ ℂ)
171126, 130, 167, 170addsub4d 11241 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
172124, 125, 127npncand 11218 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑃)))
173165, 166, 169npncan3d 11230 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
174172, 173oveq12d 7236 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
175164, 171, 1743eqtr2d 2783 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
176143, 146, 1753eqtr4d 2787 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))))
177129, 133addcld 10857 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) ∈ ℂ)
178 subcl 11082 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑄)) ∈ ℂ)
17944, 125, 178sylancr 590 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) ∈ ℂ)
180177, 134, 179, 137divmuld 11635 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))))))
181176, 180mpbird 260 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)))
182126, 128, 134, 137div23d 11650 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))))
183134, 130, 134, 137divsubdird 11652 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
184124, 125, 127nnncan2d 11229 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑄)))
185184oveq1d 7233 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))))
186134, 137dividd 11611 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = 1)
187186oveq1d 7233 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
188183, 185, 1873eqtr3d 2785 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
189188oveq1d 7233 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
190182, 189eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
191130, 132, 134, 137div23d 11650 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))))
192190, 191oveq12d 7236 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
193138, 181, 1923eqtr3d 2785 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
194193oveq1d 7233 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑄)) · (𝑍𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)))
195126, 127mulcld 10858 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) ∈ ℂ)
196130, 124mulcld 10858 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) ∈ ℂ)
197195, 196, 134, 137divdird 11651 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))))
198154, 161oveq12d 7236 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
199173, 198, 1423eqtr4rd 2788 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
200195, 196addcld 10857 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) ∈ ℂ)
201200, 134, 125, 137divmuld 11635 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)))))
202199, 201mpbird 260 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄))
203126, 127, 134, 137div23d 11650 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)))
204188oveq1d 7233 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
205203, 204eqtrd 2777 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
206130, 124, 134, 137div23d 11650 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)))
207205, 206oveq12d 7236 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
208197, 202, 2073eqtr3d 2785 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
209208oveq1d 7233 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝑈𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)))
210194, 209oveq12d 7236 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
211130, 134, 137divcld 11613 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ)
212 subcl 11082 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
21344, 211, 212sylancr 590 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
214 simp3l 1203 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
215128, 214mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
216213, 215mulcld 10858 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) ∈ ℂ)
217132, 214mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑅)) · (𝑍𝑖)) ∈ ℂ)
218211, 217mulcld 10858 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) ∈ ℂ)
219 simp3r 1204 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
220127, 219mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
221213, 220mulcld 10858 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
222124, 219mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝑈𝑖)) ∈ ℂ)
223211, 222mulcld 10858 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))) ∈ ℂ)
224216, 218, 221, 223add4d 11065 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
225213, 128mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) ∈ ℂ)
226211, 132mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) ∈ ℂ)
227213, 128, 214mulassd 10861 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))))
228211, 132, 214mulassd 10861 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))))
229227, 228oveq12d 7236 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
230225, 214, 226, 229joinlmuladdmuld 10865 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
231213, 127mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) ∈ ℂ)
232211, 124mulcld 10858 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) ∈ ℂ)
233213, 127, 219mulassd 10861 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))))
234211, 124, 219mulassd 10861 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))
235233, 234oveq12d 7236 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
236231, 219, 232, 235joinlmuladdmuld 10865 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
237230, 236oveq12d 7236 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
238213, 215, 220adddid 10862 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))))
239211, 217, 222adddid 10862 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
240238, 239oveq12d 7236 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
241224, 237, 2403eqtr4rd 2788 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
242210, 241eqtr4d 2780 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
243112, 113, 116, 119, 121, 123, 242syl222anc 1388 . . . . . . . . . . . . 13 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
244243ralrimiva 3105 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
245 oveq2 7226 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (1 − 𝑡) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
246245oveq1d 7233 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
247 oveq1 7225 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
248246, 247oveq12d 7236 . . . . . . . . . . . . . . 15 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
249248eqeq2d 2748 . . . . . . . . . . . . . 14 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
250249ralbidv 3118 . . . . . . . . . . . . 13 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
251250rspcev 3542 . . . . . . . . . . . 12 (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
252109, 244, 251syl2anc 587 . . . . . . . . . . 11 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
253252ex 416 . . . . . . . . . 10 ((𝐹𝑃) ≠ (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
25484, 253pm2.61ine 3025 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
255 r19.26-3 3094 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
256 simp2 1139 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
257 oveq2 7226 . . . . . . . . . . . . . . . . 17 ((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) → ((1 − 𝑡) · (𝑃𝑖)) = ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
258 oveq2 7226 . . . . . . . . . . . . . . . . 17 ((𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))) → (𝑡 · (𝑅𝑖)) = (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
259257, 258oveqan12d 7237 . . . . . . . . . . . . . . . 16 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
2602593adant2 1133 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
261256, 260eqeq12d 2753 . . . . . . . . . . . . . 14 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
262261ralimi 3083 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
263 ralbi 3090 . . . . . . . . . . . . 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 3221 . . . . . . . . . . 11 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
266265biimprcd 253 . . . . . . . . . 10 (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
267255, 266syl5bir 246 . . . . . . . . 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 652 . . . . . . 7 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
270269expimpd 457 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
271270adantlr 715 . . . . 5 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27212, 271syl5bi 245 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27311, 272mpd 15 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))))
274 simpl1 1193 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑁 ∈ ℕ)
2751ssrab3 4000 . . . . . . . 8 𝐷 ⊆ (𝔼‘𝑁)
276275sseli 3901 . . . . . . 7 (𝑄𝐷𝑄 ∈ (𝔼‘𝑁))
277275sseli 3901 . . . . . . 7 (𝑃𝐷𝑃 ∈ (𝔼‘𝑁))
278275sseli 3901 . . . . . . 7 (𝑅𝐷𝑅 ∈ (𝔼‘𝑁))
279276, 277, 2783anim123i 1153 . . . . . 6 ((𝑄𝐷𝑃𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
2802793com12 1125 . . . . 5 ((𝑃𝐷𝑄𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
281 brbtwn 26995 . . . . . 6 ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
282281adantl 485 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
283274, 280, 282syl2an 599 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
284283adantr 484 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
285273, 284mpbird 260 . 2 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
286285ex 416 1 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 847  w3a 1089   = wceq 1543  wcel 2110  wne 2940  wral 3061  wrex 3062  {crab 3065  cop 4552   class class class wbr 5058  {copab 5120  cfv 6385  (class class class)co 7218  cc 10732  cr 10733  0cc0 10734  1c1 10735   + caddc 10737   · cmul 10739  +∞cpnf 10869   < clt 10872  cle 10873  cmin 11067   / cdiv 11494  cn 11835  [,)cico 12942  [,]cicc 12943  ...cfz 13100  𝔼cee 26984   Btwn cbtwn 26985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-er 8396  df-map 8515  df-en 8632  df-dom 8633  df-sdom 8634  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-div 11495  df-nn 11836  df-z 12182  df-uz 12444  df-ico 12946  df-icc 12947  df-fz 13101  df-ee 26987  df-btwn 26988
This theorem is referenced by:  axcontlem10  27069
  Copyright terms: Public domain W3C validator