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

Theorem axcontlem8 29001
Description: Lemma for axcont 29006. 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 28999 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑃𝐷) → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
43ex 412 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑃𝐷 → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
51, 2axcontlem6 28999 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑄𝐷) → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
65ex 412 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑄𝐷 → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
71, 2axcontlem6 28999 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑅𝐷) → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
87ex 412 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑅𝐷 → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
94, 6, 83anim123d 1442 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ((𝑃𝐷𝑄𝐷𝑅𝐷) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
109imp 406 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
1110adantr 480 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
12 3an6 1445 . . . . 5 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
13 0elunit 13506 . . . . . . . . . . . 12 0 ∈ (0[,]1)
14 simplr1 1214 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑃) ∈ (0[,)+∞))
1514ad2antlr 727 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
16 elrege0 13491 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) ∈ (0[,)+∞) ↔ ((𝐹𝑃) ∈ ℝ ∧ 0 ≤ (𝐹𝑃)))
1716simplbi 497 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℝ)
1815, 17syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℝ)
1918recnd 11287 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
20 simprrl 781 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
2120adantr 480 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≤ (𝐹𝑄))
22 simprrr 782 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
23 simpl 482 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) = (𝐹𝑅))
2422, 23breqtrrd 5176 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑃))
2524adantr 480 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ≤ (𝐹𝑃))
26 simplr2 1215 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑄) ∈ (0[,)+∞))
2726ad2antlr 727 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
28 elrege0 13491 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑄) ∈ (0[,)+∞) ↔ ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
2928simplbi 497 . . . . . . . . . . . . . . . . 17 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℝ)
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℝ)
3118, 30letri3d 11401 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹𝑃) = (𝐹𝑄) ↔ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑃))))
3221, 25, 31mpbir2and 713 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑄))
33 simpll 767 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑅))
34 simpll2 1212 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
3534adantr 480 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
3635ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37 fveecn 28932 . . . . . . . . . . . . . . 15 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3836, 37sylancom 588 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
39 simpll3 1213 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
4039adantr 480 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
4140ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42 fveecn 28932 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
4341, 42sylancom 588 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
44 ax-1cn 11211 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
45 simpl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
46 subcl 11505 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (1 − (𝐹𝑃)) ∈ ℂ)
4744, 45, 46sylancr 587 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
48 simprl 771 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
4947, 48mulcld 11279 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
50 mulcl 11237 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5150adantrl 716 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5249, 51addcld 11278 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
5352mullidd 11277 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5452mul02d 11457 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = 0)
5553, 54oveq12d 7449 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0))
5652addridd 11459 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5755, 56eqtr2d 2776 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
58573adant2 1130 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
59 oveq2 7439 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑄) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑄)))
6059oveq1d 7446 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑄)) · (𝑍𝑖)))
61 oveq1 7438 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑄) · (𝑈𝑖)))
6260, 61oveq12d 7449 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑄) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
63 oveq2 7439 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑃) = (𝐹𝑅) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑅)))
6463oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑅)) · (𝑍𝑖)))
65 oveq1 7438 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑅) · (𝑈𝑖)))
6664, 65oveq12d 7449 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑅) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))
6766oveq2d 7447 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑅) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
6867oveq2d 7447 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑅) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
6962, 68eqeqan12d 2749 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
70693ad2ant2 1133 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
7158, 70mpbid 232 . . . . . . . . . . . . . 14 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7219, 32, 33, 38, 43, 71syl122anc 1378 . . . . . . . . . . . . 13 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7372ralrimiva 3144 . . . . . . . . . . . 12 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
74 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75 1m0e1 12385 . . . . . . . . . . . . . . . . . 18 (1 − 0) = 1
7674, 75eqtrdi 2791 . . . . . . . . . . . . . . . . 17 (𝑡 = 0 → (1 − 𝑡) = 1)
7776oveq1d 7446 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
78 oveq1 7438 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
7977, 78oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8079eqeq2d 2746 . . . . . . . . . . . . . 14 (𝑡 = 0 → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8180ralbidv 3176 . . . . . . . . . . . . 13 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8281rspcev 3622 . . . . . . . . . . . 12 ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8313, 73, 82sylancr 587 . . . . . . . . . . 11 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8483ex 412 . . . . . . . . . 10 ((𝐹𝑃) = (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8526adantl 481 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ (0[,)+∞))
8685, 29syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ ℝ)
87 simplr3 1216 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑅) ∈ (0[,)+∞))
8887adantl 481 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ (0[,)+∞))
89 elrege0 13491 . . . . . . . . . . . . . . . 16 ((𝐹𝑅) ∈ (0[,)+∞) ↔ ((𝐹𝑅) ∈ ℝ ∧ 0 ≤ (𝐹𝑅)))
9089simplbi 497 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℝ)
9188, 90syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ ℝ)
9214adantl 481 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ (0[,)+∞))
9392, 17syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ ℝ)
94 simprrr 782 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
9586, 91, 93, 94lesub1dd 11877 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃)))
9686, 93resubcld 11689 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ)
97 simprrl 781 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
9886, 93subge0d 11851 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (0 ≤ ((𝐹𝑄) − (𝐹𝑃)) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
9997, 98mpbird 257 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 ≤ ((𝐹𝑄) − (𝐹𝑃)))
10091, 93resubcld 11689 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ)
10193, 86, 91, 97, 94letrd 11416 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑅))
102 simpl 482 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≠ (𝐹𝑅))
103102necomd 2994 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ≠ (𝐹𝑃))
10493, 91, 101, 103leneltd 11413 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) < (𝐹𝑅))
10593, 91posdifd 11848 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑃) < (𝐹𝑅) ↔ 0 < ((𝐹𝑅) − (𝐹𝑃))))
106104, 105mpbid 232 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 < ((𝐹𝑅) − (𝐹𝑃)))
107 divelunit 13531 . . . . . . . . . . . . . 14 (((((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑄) − (𝐹𝑃))) ∧ (((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ ∧ 0 < ((𝐹𝑅) − (𝐹𝑃)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10896, 99, 100, 106, 107syl22anc 839 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10995, 108mpbird 257 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1))
11014ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
11117recnd 11287 . . . . . . . . . . . . . . 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 11287 . . . . . . . . . . . . . . 15 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℂ)
116114, 115syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℂ)
11787ad2antlr 727 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ (0[,)+∞))
11890recnd 11287 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℂ)
119117, 118syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ ℂ)
12034ad2antrl 728 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
121120, 37sylan 580 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
12239ad2antrl 728 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
123122, 42sylan 580 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
124 simp2r 1199 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ∈ ℂ)
125 simp2l 1198 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) ∈ ℂ)
126124, 125subcld 11618 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ)
127 simp1l 1196 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
12844, 127, 46sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
129126, 128mulcld 11279 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) ∈ ℂ)
130125, 127subcld 11618 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ)
131 subcl 11505 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (1 − (𝐹𝑅)) ∈ ℂ)
13244, 124, 131sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑅)) ∈ ℂ)
133130, 132mulcld 11279 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) ∈ ℂ)
134124, 127subcld 11618 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ)
135 simp1r 1197 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ≠ (𝐹𝑅))
136135necomd 2994 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ≠ (𝐹𝑃))
137124, 127, 136subne0d 11627 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ≠ 0)
138129, 133, 134, 137divdird 12079 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))))
139134mulridd 11276 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · 1) = ((𝐹𝑅) − (𝐹𝑃)))
140134, 125mulcomd 11280 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))))
141125, 124, 127subdid 11717 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
142140, 141eqtrd 2775 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
143139, 142oveq12d 7449 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
144 subdi 11694 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
14544, 144mp3an2 1448 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
146134, 125, 145syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
147 subdi 11694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
14844, 147mp3an2 1448 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
149126, 127, 148syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
150126mulridd 11276 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · 1) = ((𝐹𝑅) − (𝐹𝑄)))
151124, 125, 127subdird 11718 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))))
152124, 127mulcomd 11280 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝐹𝑃)) = ((𝐹𝑃) · (𝐹𝑅)))
153152oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
154151, 153eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
155150, 154oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
156149, 155eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
157 subdi 11694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
15844, 157mp3an2 1448 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
159130, 124, 158syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
160130mulridd 11276 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · 1) = ((𝐹𝑄) − (𝐹𝑃)))
161125, 127, 124subdird 11718 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))
162160, 161oveq12d 7449 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
163159, 162eqtrd 2775 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
164156, 163oveq12d 7449 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
165127, 124mulcld 11279 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝐹𝑅)) ∈ ℂ)
166125, 127mulcld 11279 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑃)) ∈ ℂ)
167165, 166subcld 11618 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) ∈ ℂ)
168 mulcl 11237 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
1691683ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
170169, 165subcld 11618 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))) ∈ ℂ)
171126, 130, 167, 170addsub4d 11665 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
172124, 125, 127npncand 11642 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑃)))
173165, 166, 169npncan3d 11654 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
174172, 173oveq12d 7449 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
175164, 171, 1743eqtr2d 2781 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
176143, 146, 1753eqtr4d 2785 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))))
177129, 133addcld 11278 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) ∈ ℂ)
178 subcl 11505 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑄)) ∈ ℂ)
17944, 125, 178sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) ∈ ℂ)
180177, 134, 179, 137divmuld 12063 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))))))
181176, 180mpbird 257 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)))
182126, 128, 134, 137div23d 12078 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))))
183134, 130, 134, 137divsubdird 12080 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
184124, 125, 127nnncan2d 11653 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑄)))
185184oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))))
186134, 137dividd 12039 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = 1)
187186oveq1d 7446 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
188183, 185, 1873eqtr3d 2783 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
189188oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
190182, 189eqtrd 2775 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
191130, 132, 134, 137div23d 12078 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))))
192190, 191oveq12d 7449 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
193138, 181, 1923eqtr3d 2783 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
194193oveq1d 7446 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑄)) · (𝑍𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)))
195126, 127mulcld 11279 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) ∈ ℂ)
196130, 124mulcld 11279 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) ∈ ℂ)
197195, 196, 134, 137divdird 12079 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))))
198154, 161oveq12d 7449 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
199173, 198, 1423eqtr4rd 2786 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
200195, 196addcld 11278 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) ∈ ℂ)
201200, 134, 125, 137divmuld 12063 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)))))
202199, 201mpbird 257 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄))
203126, 127, 134, 137div23d 12078 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)))
204188oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
205203, 204eqtrd 2775 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
206130, 124, 134, 137div23d 12078 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)))
207205, 206oveq12d 7449 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
208197, 202, 2073eqtr3d 2783 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
209208oveq1d 7446 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝑈𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)))
210194, 209oveq12d 7449 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
211130, 134, 137divcld 12041 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ)
212 subcl 11505 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
21344, 211, 212sylancr 587 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
214 simp3l 1200 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
215128, 214mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
216213, 215mulcld 11279 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) ∈ ℂ)
217132, 214mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑅)) · (𝑍𝑖)) ∈ ℂ)
218211, 217mulcld 11279 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) ∈ ℂ)
219 simp3r 1201 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
220127, 219mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
221213, 220mulcld 11279 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
222124, 219mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝑈𝑖)) ∈ ℂ)
223211, 222mulcld 11279 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))) ∈ ℂ)
224216, 218, 221, 223add4d 11488 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
225213, 128mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) ∈ ℂ)
226211, 132mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) ∈ ℂ)
227213, 128, 214mulassd 11282 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))))
228211, 132, 214mulassd 11282 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))))
229227, 228oveq12d 7449 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
230225, 214, 226, 229joinlmuladdmuld 11286 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
231213, 127mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) ∈ ℂ)
232211, 124mulcld 11279 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) ∈ ℂ)
233213, 127, 219mulassd 11282 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))))
234211, 124, 219mulassd 11282 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))
235233, 234oveq12d 7449 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
236231, 219, 232, 235joinlmuladdmuld 11286 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
237230, 236oveq12d 7449 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
238213, 215, 220adddid 11283 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))))
239211, 217, 222adddid 11283 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
240238, 239oveq12d 7449 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
241224, 237, 2403eqtr4rd 2786 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
242210, 241eqtr4d 2778 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
243112, 113, 116, 119, 121, 123, 242syl222anc 1385 . . . . . . . . . . . . 13 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
244243ralrimiva 3144 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
245 oveq2 7439 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (1 − 𝑡) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
246245oveq1d 7446 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
247 oveq1 7438 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
248246, 247oveq12d 7449 . . . . . . . . . . . . . . 15 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
249248eqeq2d 2746 . . . . . . . . . . . . . 14 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
250249ralbidv 3176 . . . . . . . . . . . . 13 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
251250rspcev 3622 . . . . . . . . . . . 12 (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
252109, 244, 251syl2anc 584 . . . . . . . . . . 11 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
253252ex 412 . . . . . . . . . 10 ((𝐹𝑃) ≠ (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
25484, 253pm2.61ine 3023 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
255 r19.26-3 3110 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
256 simp2 1136 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
257 oveq2 7439 . . . . . . . . . . . . . . . . 17 ((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) → ((1 − 𝑡) · (𝑃𝑖)) = ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
258 oveq2 7439 . . . . . . . . . . . . . . . . 17 ((𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))) → (𝑡 · (𝑅𝑖)) = (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
259257, 258oveqan12d 7450 . . . . . . . . . . . . . . . 16 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
2602593adant2 1130 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
261256, 260eqeq12d 2751 . . . . . . . . . . . . . 14 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
262261ralimi 3081 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
263 ralbi 3101 . . . . . . . . . . . . 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 3177 . . . . . . . . . . 11 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
266265biimprcd 250 . . . . . . . . . 10 (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
267255, 266biimtrrid 243 . . . . . . . . 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 453 . . . . . 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, 271biimtrid 242 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27311, 272mpd 15 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))))
274 simpl1 1190 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑁 ∈ ℕ)
2751ssrab3 4092 . . . . . . . 8 𝐷 ⊆ (𝔼‘𝑁)
276275sseli 3991 . . . . . . 7 (𝑄𝐷𝑄 ∈ (𝔼‘𝑁))
277275sseli 3991 . . . . . . 7 (𝑃𝐷𝑃 ∈ (𝔼‘𝑁))
278275sseli 3991 . . . . . . 7 (𝑅𝐷𝑅 ∈ (𝔼‘𝑁))
279276, 277, 2783anim123i 1150 . . . . . 6 ((𝑄𝐷𝑃𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
2802793com12 1122 . . . . 5 ((𝑃𝐷𝑄𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
281 brbtwn 28929 . . . . . 6 ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
282281adantl 481 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
283274, 280, 282syl2an 596 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
284283adantr 480 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
285273, 284mpbird 257 . 2 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
286285ex 412 1 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wral 3059  wrex 3068  {crab 3433  cop 4637   class class class wbr 5148  {copab 5210  cfv 6563  (class class class)co 7431  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158  +∞cpnf 11290   < clt 11293  cle 11294  cmin 11490   / cdiv 11918  cn 12264  [,)cico 13386  [,]cicc 13387  ...cfz 13544  𝔼cee 28918   Btwn cbtwn 28919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-z 12612  df-uz 12877  df-ico 13390  df-icc 13391  df-fz 13545  df-ee 28921  df-btwn 28922
This theorem is referenced by:  axcontlem10  29003
  Copyright terms: Public domain W3C validator