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

Theorem axcontlem8 25751
Description: Lemma for axcont 25756. 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 25749 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑃𝐷) → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
43ex 450 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑃𝐷 → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
51, 2axcontlem6 25749 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑄𝐷) → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
65ex 450 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑄𝐷 → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
71, 2axcontlem6 25749 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑅𝐷) → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
87ex 450 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑅𝐷 → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
94, 6, 83anim123d 1403 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ((𝑃𝐷𝑄𝐷𝑅𝐷) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
109imp 445 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
1110adantr 481 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
12 3an6 1406 . . . . 5 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
13 0elunit 12232 . . . . . . . . . . . 12 0 ∈ (0[,]1)
14 simplr1 1101 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑃) ∈ (0[,)+∞))
1514ad2antlr 762 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
16 elrege0 12220 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) ∈ (0[,)+∞) ↔ ((𝐹𝑃) ∈ ℝ ∧ 0 ≤ (𝐹𝑃)))
1716simplbi 476 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℝ)
1815, 17syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℝ)
1918recnd 10012 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
20 simprrl 803 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
2120adantr 481 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≤ (𝐹𝑄))
22 simprrr 804 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
23 simpl 473 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) = (𝐹𝑅))
2422, 23breqtrrd 4641 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑃))
2524adantr 481 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ≤ (𝐹𝑃))
26 simplr2 1102 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑄) ∈ (0[,)+∞))
2726ad2antlr 762 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
28 elrege0 12220 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑄) ∈ (0[,)+∞) ↔ ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
2928simplbi 476 . . . . . . . . . . . . . . . . 17 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℝ)
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℝ)
3118, 30letri3d 10123 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹𝑃) = (𝐹𝑄) ↔ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑃))))
3221, 25, 31mpbir2and 956 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑄))
33 simpll 789 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑅))
34 simpll2 1099 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
3534adantr 481 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
3635ad2antlr 762 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37 fveecn 25682 . . . . . . . . . . . . . . 15 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3836, 37sylancom 700 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
39 simpll3 1100 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
4039adantr 481 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
4140ad2antlr 762 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42 fveecn 25682 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
4341, 42sylancom 700 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
44 ax-1cn 9938 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
45 simpl 473 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
46 subcl 10224 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (1 − (𝐹𝑃)) ∈ ℂ)
4744, 45, 46sylancr 694 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
48 simprl 793 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
4947, 48mulcld 10004 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
50 mulcl 9964 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5150adantrl 751 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5249, 51addcld 10003 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
5352mulid2d 10002 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5452mul02d 10178 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = 0)
5553, 54oveq12d 6622 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0))
5652addid1d 10180 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5755, 56eqtr2d 2656 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
58573adant2 1078 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
59 oveq2 6612 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑄) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑄)))
6059oveq1d 6619 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑄)) · (𝑍𝑖)))
61 oveq1 6611 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑄) · (𝑈𝑖)))
6260, 61oveq12d 6622 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑄) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
63 oveq2 6612 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑃) = (𝐹𝑅) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑅)))
6463oveq1d 6619 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑅)) · (𝑍𝑖)))
65 oveq1 6611 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑅) · (𝑈𝑖)))
6664, 65oveq12d 6622 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑅) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))
6766oveq2d 6620 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑅) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
6867oveq2d 6620 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑅) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
6962, 68eqeqan12d 2637 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
70693ad2ant2 1081 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
7158, 70mpbid 222 . . . . . . . . . . . . . 14 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7219, 32, 33, 38, 43, 71syl122anc 1332 . . . . . . . . . . . . 13 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7372ralrimiva 2960 . . . . . . . . . . . 12 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
74 oveq2 6612 . . . . . . . . . . . . . . . . . 18 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75 1m0e1 11075 . . . . . . . . . . . . . . . . . 18 (1 − 0) = 1
7674, 75syl6eq 2671 . . . . . . . . . . . . . . . . 17 (𝑡 = 0 → (1 − 𝑡) = 1)
7776oveq1d 6619 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
78 oveq1 6611 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
7977, 78oveq12d 6622 . . . . . . . . . . . . . . 15 (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8079eqeq2d 2631 . . . . . . . . . . . . . 14 (𝑡 = 0 → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8180ralbidv 2980 . . . . . . . . . . . . 13 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8281rspcev 3295 . . . . . . . . . . . 12 ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8313, 73, 82sylancr 694 . . . . . . . . . . 11 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8483ex 450 . . . . . . . . . 10 ((𝐹𝑃) = (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8526adantl 482 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ (0[,)+∞))
8685, 29syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ ℝ)
87 simplr3 1103 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑅) ∈ (0[,)+∞))
8887adantl 482 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ (0[,)+∞))
89 elrege0 12220 . . . . . . . . . . . . . . . 16 ((𝐹𝑅) ∈ (0[,)+∞) ↔ ((𝐹𝑅) ∈ ℝ ∧ 0 ≤ (𝐹𝑅)))
9089simplbi 476 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℝ)
9188, 90syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ ℝ)
9214adantl 482 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ (0[,)+∞))
9392, 17syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ ℝ)
94 simprrr 804 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
9586, 91, 93, 94lesub1dd 10587 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃)))
9686, 93resubcld 10402 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ)
97 simprrl 803 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
9886, 93subge0d 10561 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (0 ≤ ((𝐹𝑄) − (𝐹𝑃)) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
9997, 98mpbird 247 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 ≤ ((𝐹𝑄) − (𝐹𝑃)))
10091, 93resubcld 10402 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ)
10193, 86, 91, 97, 94letrd 10138 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑅))
102 simpl 473 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≠ (𝐹𝑅))
103102necomd 2845 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ≠ (𝐹𝑃))
10493, 91ltlend 10126 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑃) < (𝐹𝑅) ↔ ((𝐹𝑃) ≤ (𝐹𝑅) ∧ (𝐹𝑅) ≠ (𝐹𝑃))))
105101, 103, 104mpbir2and 956 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) < (𝐹𝑅))
10693, 91posdifd 10558 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑃) < (𝐹𝑅) ↔ 0 < ((𝐹𝑅) − (𝐹𝑃))))
107105, 106mpbid 222 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 < ((𝐹𝑅) − (𝐹𝑃)))
108 divelunit 12256 . . . . . . . . . . . . . 14 (((((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑄) − (𝐹𝑃))) ∧ (((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ ∧ 0 < ((𝐹𝑅) − (𝐹𝑃)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10996, 99, 100, 107, 108syl22anc 1324 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
11095, 109mpbird 247 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1))
11114ad2antlr 762 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
11217recnd 10012 . . . . . . . . . . . . . . 15 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℂ)
113111, 112syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
114 simpll 789 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≠ (𝐹𝑅))
11526ad2antlr 762 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
11629recnd 10012 . . . . . . . . . . . . . . 15 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℂ)
117115, 116syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℂ)
11887ad2antlr 762 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ (0[,)+∞))
11990recnd 10012 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℂ)
120118, 119syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ ℂ)
12134ad2antrl 763 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
122121, 37sylan 488 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
12339ad2antrl 763 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
124123, 42sylan 488 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
125 simp2r 1086 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ∈ ℂ)
126 simp2l 1085 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) ∈ ℂ)
127125, 126subcld 10336 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ)
128 simp1l 1083 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
12944, 128, 46sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
130127, 129mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) ∈ ℂ)
131126, 128subcld 10336 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ)
132 subcl 10224 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (1 − (𝐹𝑅)) ∈ ℂ)
13344, 125, 132sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑅)) ∈ ℂ)
134131, 133mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) ∈ ℂ)
135125, 128subcld 10336 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ)
136 simp1r 1084 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ≠ (𝐹𝑅))
137136necomd 2845 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ≠ (𝐹𝑃))
138125, 128, 137subne0d 10345 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ≠ 0)
139130, 134, 135, 138divdird 10783 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))))
140135mulid1d 10001 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · 1) = ((𝐹𝑅) − (𝐹𝑃)))
141135, 126mulcomd 10005 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))))
142126, 125, 128subdid 10430 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
143141, 142eqtrd 2655 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
144140, 143oveq12d 6622 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
145 subdi 10407 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
14644, 145mp3an2 1409 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
147135, 126, 146syl2anc 692 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
148 subdi 10407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
14944, 148mp3an2 1409 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
150127, 128, 149syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
151127mulid1d 10001 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · 1) = ((𝐹𝑅) − (𝐹𝑄)))
152125, 126, 128subdird 10431 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))))
153125, 128mulcomd 10005 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝐹𝑃)) = ((𝐹𝑃) · (𝐹𝑅)))
154153oveq1d 6619 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
155152, 154eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
156151, 155oveq12d 6622 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
157150, 156eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
158 subdi 10407 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
15944, 158mp3an2 1409 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
160131, 125, 159syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
161131mulid1d 10001 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · 1) = ((𝐹𝑄) − (𝐹𝑃)))
162126, 128, 125subdird 10431 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))
163161, 162oveq12d 6622 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
164160, 163eqtrd 2655 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
165157, 164oveq12d 6622 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
166128, 125mulcld 10004 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝐹𝑅)) ∈ ℂ)
167126, 128mulcld 10004 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑃)) ∈ ℂ)
168166, 167subcld 10336 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) ∈ ℂ)
169 mulcl 9964 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
1701693ad2ant2 1081 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
171170, 166subcld 10336 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))) ∈ ℂ)
172127, 131, 168, 171addsub4d 10383 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
173125, 126, 128npncand 10360 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑃)))
174166, 167, 170npncan3d 10372 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
175173, 174oveq12d 6622 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
176165, 172, 1753eqtr2d 2661 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
177144, 147, 1763eqtr4d 2665 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))))
178130, 134addcld 10003 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) ∈ ℂ)
179 subcl 10224 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑄)) ∈ ℂ)
18044, 126, 179sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) ∈ ℂ)
181178, 135, 180, 138divmuld 10767 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))))))
182177, 181mpbird 247 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)))
183127, 129, 135, 138div23d 10782 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))))
184135, 131, 135, 138divsubdird 10784 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
185125, 126, 128nnncan2d 10371 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑄)))
186185oveq1d 6619 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))))
187135, 138dividd 10743 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = 1)
188187oveq1d 6619 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
189184, 186, 1883eqtr3d 2663 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
190189oveq1d 6619 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
191183, 190eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
192131, 133, 135, 138div23d 10782 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))))
193191, 192oveq12d 6622 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
194139, 182, 1933eqtr3d 2663 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
195194oveq1d 6619 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑄)) · (𝑍𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)))
196127, 128mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) ∈ ℂ)
197131, 125mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) ∈ ℂ)
198196, 197, 135, 138divdird 10783 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))))
199155, 162oveq12d 6622 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
200174, 199, 1433eqtr4rd 2666 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
201196, 197addcld 10003 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) ∈ ℂ)
202201, 135, 126, 138divmuld 10767 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)))))
203200, 202mpbird 247 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄))
204127, 128, 135, 138div23d 10782 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)))
205189oveq1d 6619 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
206204, 205eqtrd 2655 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
207131, 125, 135, 138div23d 10782 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)))
208206, 207oveq12d 6622 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
209198, 203, 2083eqtr3d 2663 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
210209oveq1d 6619 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝑈𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)))
211195, 210oveq12d 6622 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
212131, 135, 138divcld 10745 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ)
213 subcl 10224 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
21444, 212, 213sylancr 694 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
215 simp3l 1087 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
216129, 215mulcld 10004 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
217214, 216mulcld 10004 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) ∈ ℂ)
218133, 215mulcld 10004 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑅)) · (𝑍𝑖)) ∈ ℂ)
219212, 218mulcld 10004 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) ∈ ℂ)
220 simp3r 1088 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
221128, 220mulcld 10004 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
222214, 221mulcld 10004 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
223125, 220mulcld 10004 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝑈𝑖)) ∈ ℂ)
224212, 223mulcld 10004 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))) ∈ ℂ)
225217, 219, 222, 224add4d 10208 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
226214, 129mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) ∈ ℂ)
227212, 133mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) ∈ ℂ)
228226, 227, 215adddird 10009 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖))))
229214, 129, 215mulassd 10007 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))))
230212, 133, 215mulassd 10007 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))))
231229, 230oveq12d 6622 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
232228, 231eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
233214, 128mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) ∈ ℂ)
234212, 125mulcld 10004 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) ∈ ℂ)
235233, 234, 220adddird 10009 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖))))
236214, 128, 220mulassd 10007 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))))
237212, 125, 220mulassd 10007 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))
238236, 237oveq12d 6622 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
239235, 238eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
240232, 239oveq12d 6622 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
241214, 216, 221adddid 10008 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))))
242212, 218, 223adddid 10008 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
243241, 242oveq12d 6622 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
244225, 240, 2433eqtr4rd 2666 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
245211, 244eqtr4d 2658 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
246113, 114, 117, 120, 122, 124, 245syl222anc 1339 . . . . . . . . . . . . 13 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
247246ralrimiva 2960 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
248 oveq2 6612 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (1 − 𝑡) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
249248oveq1d 6619 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
250 oveq1 6611 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
251249, 250oveq12d 6622 . . . . . . . . . . . . . . 15 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
252251eqeq2d 2631 . . . . . . . . . . . . . 14 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
253252ralbidv 2980 . . . . . . . . . . . . 13 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
254253rspcev 3295 . . . . . . . . . . . 12 (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
255110, 247, 254syl2anc 692 . . . . . . . . . . 11 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
256255ex 450 . . . . . . . . . 10 ((𝐹𝑃) ≠ (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
25784, 256pm2.61ine 2873 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
258 r19.26-3 3059 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
259 simp2 1060 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
260 oveq2 6612 . . . . . . . . . . . . . . . . 17 ((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) → ((1 − 𝑡) · (𝑃𝑖)) = ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
261 oveq2 6612 . . . . . . . . . . . . . . . . 17 ((𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))) → (𝑡 · (𝑅𝑖)) = (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
262260, 261oveqan12d 6623 . . . . . . . . . . . . . . . 16 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
2632623adant2 1078 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
264259, 263eqeq12d 2636 . . . . . . . . . . . . . 14 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
265264ralimi 2947 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
266 ralbi 3061 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
267265, 266syl 17 . . . . . . . . . . . 12 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
268267rexbidv 3045 . . . . . . . . . . 11 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
269268biimprcd 240 . . . . . . . . . 10 (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
270258, 269syl5bir 233 . . . . . . . . 9 (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
271257, 270syl 17 . . . . . . . 8 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
272271an32s 845 . . . . . . 7 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
273272expimpd 628 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
274273adantlr 750 . . . . 5 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27512, 274syl5bi 232 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27611, 275mpd 15 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))))
277 simpl1 1062 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑁 ∈ ℕ)
278 ssrab2 3666 . . . . . . . . 9 {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ⊆ (𝔼‘𝑁)
2791, 278eqsstri 3614 . . . . . . . 8 𝐷 ⊆ (𝔼‘𝑁)
280279sseli 3579 . . . . . . 7 (𝑄𝐷𝑄 ∈ (𝔼‘𝑁))
281279sseli 3579 . . . . . . 7 (𝑃𝐷𝑃 ∈ (𝔼‘𝑁))
282279sseli 3579 . . . . . . 7 (𝑅𝐷𝑅 ∈ (𝔼‘𝑁))
283280, 281, 2823anim123i 1245 . . . . . 6 ((𝑄𝐷𝑃𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
2842833com12 1266 . . . . 5 ((𝑃𝐷𝑄𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
285 brbtwn 25679 . . . . . 6 ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
286285adantl 482 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
287277, 284, 286syl2an 494 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
288287adantr 481 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
289276, 288mpbird 247 . 2 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
290289ex 450 1 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  cop 4154   class class class wbr 4613  {copab 4672  cfv 5847  (class class class)co 6604  cc 9878  cr 9879  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885  +∞cpnf 10015   < clt 10018  cle 10019  cmin 10210   / cdiv 10628  cn 10964  [,)cico 12119  [,]cicc 12120  ...cfz 12268  𝔼cee 25668   Btwn cbtwn 25669
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-z 11322  df-uz 11632  df-ico 12123  df-icc 12124  df-fz 12269  df-ee 25671  df-btwn 25672
This theorem is referenced by:  axcontlem10  25753
  Copyright terms: Public domain W3C validator