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

Theorem axcontlem8 26142
Description: Lemma for axcont 26147. 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 26140 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑃𝐷) → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
43ex 401 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑃𝐷 → ((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
51, 2axcontlem6 26140 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑄𝐷) → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))))
65ex 401 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑄𝐷 → ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))))
71, 2axcontlem6 26140 . . . . . . . 8 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ 𝑅𝐷) → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
87ex 401 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → (𝑅𝐷 → ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
94, 6, 83anim123d 1567 . . . . . 6 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → ((𝑃𝐷𝑄𝐷𝑅𝐷) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
109imp 395 . . . . 5 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
1110adantr 472 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
12 3an6 1570 . . . . 5 ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
13 0elunit 12495 . . . . . . . . . . . 12 0 ∈ (0[,]1)
14 simplr1 1275 . . . . . . . . . . . . . . . . 17 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑃) ∈ (0[,)+∞))
1514ad2antlr 718 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
16 elrege0 12482 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) ∈ (0[,)+∞) ↔ ((𝐹𝑃) ∈ ℝ ∧ 0 ≤ (𝐹𝑃)))
1716simplbi 491 . . . . . . . . . . . . . . . 16 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℝ)
1815, 17syl 17 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℝ)
1918recnd 10322 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
20 simprrl 799 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
2120adantr 472 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≤ (𝐹𝑄))
22 simprrr 800 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
23 simpl 474 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) = (𝐹𝑅))
2422, 23breqtrrd 4837 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑃))
2524adantr 472 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ≤ (𝐹𝑃))
26 simplr2 1277 . . . . . . . . . . . . . . . . . 18 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑄) ∈ (0[,)+∞))
2726ad2antlr 718 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
28 elrege0 12482 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑄) ∈ (0[,)+∞) ↔ ((𝐹𝑄) ∈ ℝ ∧ 0 ≤ (𝐹𝑄)))
2928simplbi 491 . . . . . . . . . . . . . . . . 17 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℝ)
3027, 29syl 17 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℝ)
3118, 30letri3d 10433 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹𝑃) = (𝐹𝑄) ↔ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑃))))
3221, 25, 31mpbir2and 704 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑄))
33 simpll 783 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) = (𝐹𝑅))
34 simpll2 1271 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
3534adantr 472 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
3635ad2antlr 718 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37 fveecn 26073 . . . . . . . . . . . . . . 15 ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
3836, 37sylancom 582 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
39 simpll3 1273 . . . . . . . . . . . . . . . . 17 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
4039adantr 472 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
4140ad2antlr 718 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42 fveecn 26073 . . . . . . . . . . . . . . 15 ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
4341, 42sylancom 582 . . . . . . . . . . . . . 14 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
44 ax-1cn 10247 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℂ
45 simpl 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
46 subcl 10534 . . . . . . . . . . . . . . . . . . . . . 22 ((1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (1 − (𝐹𝑃)) ∈ ℂ)
4744, 45, 46sylancr 581 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
48 simprl 787 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
4947, 48mulcld 10314 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
50 mulcl 10273 . . . . . . . . . . . . . . . . . . . . 21 (((𝐹𝑃) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5150adantrl 707 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
5249, 51addcld 10313 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
5352mulid2d 10312 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5452mul02d 10488 . . . . . . . . . . . . . . . . . 18 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = 0)
5553, 54oveq12d 6860 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0))
5652addid1d 10490 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) + 0) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))
5755, 56eqtr2d 2800 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ∈ ℂ ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
58573adant2 1161 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))))
59 oveq2 6850 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑄) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑄)))
6059oveq1d 6857 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑄)) · (𝑍𝑖)))
61 oveq1 6849 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑄) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑄) · (𝑈𝑖)))
6260, 61oveq12d 6860 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑄) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
63 oveq2 6850 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑃) = (𝐹𝑅) → (1 − (𝐹𝑃)) = (1 − (𝐹𝑅)))
6463oveq1d 6857 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) = ((1 − (𝐹𝑅)) · (𝑍𝑖)))
65 oveq1 6849 . . . . . . . . . . . . . . . . . . . 20 ((𝐹𝑃) = (𝐹𝑅) → ((𝐹𝑃) · (𝑈𝑖)) = ((𝐹𝑅) · (𝑈𝑖)))
6664, 65oveq12d 6860 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑃) = (𝐹𝑅) → (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))
6766oveq2d 6858 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑃) = (𝐹𝑅) → (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
6867oveq2d 6858 . . . . . . . . . . . . . . . . 17 ((𝐹𝑃) = (𝐹𝑅) → ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
6962, 68eqeqan12d 2781 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
70693ad2ant2 1164 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
7158, 70mpbid 223 . . . . . . . . . . . . . 14 (((𝐹𝑃) ∈ ℂ ∧ ((𝐹𝑃) = (𝐹𝑄) ∧ (𝐹𝑃) = (𝐹𝑅)) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7219, 32, 33, 38, 43, 71syl122anc 1498 . . . . . . . . . . . . 13 ((((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
7372ralrimiva 3113 . . . . . . . . . . . 12 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
74 oveq2 6850 . . . . . . . . . . . . . . . . . 18 (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75 1m0e1 11400 . . . . . . . . . . . . . . . . . 18 (1 − 0) = 1
7674, 75syl6eq 2815 . . . . . . . . . . . . . . . . 17 (𝑡 = 0 → (1 − 𝑡) = 1)
7776oveq1d 6857 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
78 oveq1 6849 . . . . . . . . . . . . . . . 16 (𝑡 = 0 → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
7977, 78oveq12d 6860 . . . . . . . . . . . . . . 15 (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8079eqeq2d 2775 . . . . . . . . . . . . . 14 (𝑡 = 0 → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8180ralbidv 3133 . . . . . . . . . . . . 13 (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8281rspcev 3461 . . . . . . . . . . . 12 ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = ((1 · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (0 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8313, 73, 82sylancr 581 . . . . . . . . . . 11 (((𝐹𝑃) = (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
8483ex 401 . . . . . . . . . 10 ((𝐹𝑃) = (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
8526adantl 473 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ (0[,)+∞))
8685, 29syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ∈ ℝ)
87 simplr3 1279 . . . . . . . . . . . . . . . 16 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝐹𝑅) ∈ (0[,)+∞))
8887adantl 473 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ (0[,)+∞))
89 elrege0 12482 . . . . . . . . . . . . . . . 16 ((𝐹𝑅) ∈ (0[,)+∞) ↔ ((𝐹𝑅) ∈ ℝ ∧ 0 ≤ (𝐹𝑅)))
9089simplbi 491 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℝ)
9188, 90syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ∈ ℝ)
9214adantl 473 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ (0[,)+∞))
9392, 17syl 17 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ∈ ℝ)
94 simprrr 800 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑄) ≤ (𝐹𝑅))
9586, 91, 93, 94lesub1dd 10897 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃)))
9686, 93resubcld 10712 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ)
97 simprrl 799 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑄))
9886, 93subge0d 10871 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (0 ≤ ((𝐹𝑄) − (𝐹𝑃)) ↔ (𝐹𝑃) ≤ (𝐹𝑄)))
9997, 98mpbird 248 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 ≤ ((𝐹𝑄) − (𝐹𝑃)))
10091, 93resubcld 10712 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ)
10193, 86, 91, 97, 94letrd 10448 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≤ (𝐹𝑅))
102 simpl 474 . . . . . . . . . . . . . . . . 17 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) ≠ (𝐹𝑅))
103102necomd 2992 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑅) ≠ (𝐹𝑃))
10493, 91ltlend 10436 . . . . . . . . . . . . . . . 16 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑃) < (𝐹𝑅) ↔ ((𝐹𝑃) ≤ (𝐹𝑅) ∧ (𝐹𝑅) ≠ (𝐹𝑃))))
105101, 103, 104mpbir2and 704 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (𝐹𝑃) < (𝐹𝑅))
10693, 91posdifd 10868 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((𝐹𝑃) < (𝐹𝑅) ↔ 0 < ((𝐹𝑅) − (𝐹𝑃))))
107105, 106mpbid 223 . . . . . . . . . . . . . 14 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 0 < ((𝐹𝑅) − (𝐹𝑃)))
108 divelunit 12521 . . . . . . . . . . . . . 14 (((((𝐹𝑄) − (𝐹𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹𝑄) − (𝐹𝑃))) ∧ (((𝐹𝑅) − (𝐹𝑃)) ∈ ℝ ∧ 0 < ((𝐹𝑅) − (𝐹𝑃)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
10996, 99, 100, 107, 108syl22anc 867 . . . . . . . . . . . . 13 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ↔ ((𝐹𝑄) − (𝐹𝑃)) ≤ ((𝐹𝑅) − (𝐹𝑃))))
11095, 109mpbird 248 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1))
11114ad2antlr 718 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ (0[,)+∞))
11217recnd 10322 . . . . . . . . . . . . . . 15 ((𝐹𝑃) ∈ (0[,)+∞) → (𝐹𝑃) ∈ ℂ)
113111, 112syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ∈ ℂ)
114 simpll 783 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑃) ≠ (𝐹𝑅))
11526ad2antlr 718 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ (0[,)+∞))
11629recnd 10322 . . . . . . . . . . . . . . 15 ((𝐹𝑄) ∈ (0[,)+∞) → (𝐹𝑄) ∈ ℂ)
117115, 116syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑄) ∈ ℂ)
11887ad2antlr 718 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ (0[,)+∞))
11990recnd 10322 . . . . . . . . . . . . . . 15 ((𝐹𝑅) ∈ (0[,)+∞) → (𝐹𝑅) ∈ ℂ)
120118, 119syl 17 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹𝑅) ∈ ℂ)
12134ad2antrl 719 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
122121, 37sylan 575 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍𝑖) ∈ ℂ)
12339ad2antrl 719 . . . . . . . . . . . . . . 15 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
124123, 42sylan 575 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈𝑖) ∈ ℂ)
125 simp2r 1257 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ∈ ℂ)
126 simp2l 1256 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) ∈ ℂ)
127125, 126subcld 10646 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ)
128 simp1l 1254 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ∈ ℂ)
12944, 128, 46sylancr 581 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑃)) ∈ ℂ)
130127, 129mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) ∈ ℂ)
131126, 128subcld 10646 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ)
132 subcl 10534 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (1 − (𝐹𝑅)) ∈ ℂ)
13344, 125, 132sylancr 581 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑅)) ∈ ℂ)
134131, 133mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) ∈ ℂ)
135125, 128subcld 10646 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ)
136 simp1r 1255 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑃) ≠ (𝐹𝑅))
137136necomd 2992 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑅) ≠ (𝐹𝑃))
138125, 128, 137subne0d 10655 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) − (𝐹𝑃)) ≠ 0)
139130, 134, 135, 138divdird 11093 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))))
140135mulid1d 10311 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · 1) = ((𝐹𝑅) − (𝐹𝑃)))
141135, 126mulcomd 10315 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))))
142126, 125, 128subdid 10740 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
143141, 142eqtrd 2799 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
144140, 143oveq12d 6860 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
145 subdi 10717 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
14644, 145mp3an2 1573 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑅) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
147135, 126, 146syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑃)) · 1) − (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄))))
148 subdi 10717 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
14944, 148mp3an2 1573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑅) − (𝐹𝑄)) ∈ ℂ ∧ (𝐹𝑃) ∈ ℂ) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
150127, 128, 149syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))))
151127mulid1d 10311 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · 1) = ((𝐹𝑅) − (𝐹𝑄)))
152125, 126, 128subdird 10741 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))))
153125, 128mulcomd 10315 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝐹𝑃)) = ((𝐹𝑃) · (𝐹𝑅)))
154153oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) · (𝐹𝑃)) − ((𝐹𝑄) · (𝐹𝑃))) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
155152, 154eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) = (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
156151, 155oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · 1) − (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
157150, 156eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
158 subdi 10717 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
15944, 158mp3an2 1573 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑄) − (𝐹𝑃)) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
160131, 125, 159syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
161131mulid1d 10311 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · 1) = ((𝐹𝑄) − (𝐹𝑃)))
162126, 128, 125subdird 10741 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))
163161, 162oveq12d 6860 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · 1) − (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
164160, 163eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) = (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
165157, 164oveq12d 6860 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
166128, 125mulcld 10314 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝐹𝑅)) ∈ ℂ)
167126, 128mulcld 10314 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑃)) ∈ ℂ)
168166, 167subcld 10646 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) ∈ ℂ)
169 mulcl 10273 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
1701693ad2ant2 1164 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝐹𝑅)) ∈ ℂ)
171170, 166subcld 10646 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))) ∈ ℂ)
172127, 131, 168, 171addsub4d 10693 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = ((((𝐹𝑅) − (𝐹𝑄)) − (((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))) + (((𝐹𝑄) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))))
173125, 126, 128npncand 10670 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑃)))
174166, 167, 170npncan3d 10682 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))) = (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))))
175173, 174oveq12d 6860 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) + ((𝐹𝑄) − (𝐹𝑃))) − ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅))))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
176165, 172, 1753eqtr2d 2805 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) = (((𝐹𝑅) − (𝐹𝑃)) − (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃)))))
177144, 147, 1763eqtr4d 2809 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))))
178130, 134addcld 10313 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) ∈ ℂ)
179 subcl 10534 . . . . . . . . . . . . . . . . . . . . 21 ((1 ∈ ℂ ∧ (𝐹𝑄) ∈ ℂ) → (1 − (𝐹𝑄)) ∈ ℂ)
18044, 126, 179sylancr 581 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) ∈ ℂ)
181178, 135, 180, 138divmuld 11077 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (1 − (𝐹𝑄))) = ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))))))
182177, 181mpbird 248 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) + (((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅)))) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (𝐹𝑄)))
183127, 129, 135, 138div23d 11092 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))))
184135, 131, 135, 138divsubdird 11094 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
185125, 126, 128nnncan2d 10681 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) = ((𝐹𝑅) − (𝐹𝑄)))
186185oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) − ((𝐹𝑄) − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))))
187135, 138dividd 11053 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = 1)
188187oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
189184, 186, 1883eqtr3d 2807 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
190189oveq1d 6857 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
191183, 190eqtrd 2799 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))))
192131, 133, 135, 138div23d 11092 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))))
193191, 192oveq12d 6860 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (1 − (𝐹𝑃))) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (1 − (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
194139, 182, 1933eqtr3d 2807 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (𝐹𝑄)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))))
195194oveq1d 6857 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑄)) · (𝑍𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)))
196127, 128mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) ∈ ℂ)
197131, 125mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) ∈ ℂ)
198196, 197, 135, 138divdird 11093 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))))
199155, 162oveq12d 6860 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) = ((((𝐹𝑃) · (𝐹𝑅)) − ((𝐹𝑄) · (𝐹𝑃))) + (((𝐹𝑄) · (𝐹𝑅)) − ((𝐹𝑃) · (𝐹𝑅)))))
200174, 199, 1433eqtr4rd 2810 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))))
201196, 197addcld 10313 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) ∈ ℂ)
202201, 135, 126, 138divmuld 11077 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄) ↔ (((𝐹𝑅) − (𝐹𝑃)) · (𝐹𝑄)) = ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)))))
203200, 202mpbird 248 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) + (((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅))) / ((𝐹𝑅) − (𝐹𝑃))) = (𝐹𝑄))
204127, 128, 135, 138div23d 11092 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)))
205189oveq1d 6857 . . . . . . . . . . . . . . . . . . . 20 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑃)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
206204, 205eqtrd 2799 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)))
207131, 125, 135, 138div23d 11092 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)))
208206, 207oveq12d 6860 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑅) − (𝐹𝑄)) · (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) · (𝐹𝑅)) / ((𝐹𝑅) − (𝐹𝑃)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
209198, 203, 2083eqtr3d 2807 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝐹𝑄) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))))
210209oveq1d 6857 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑄) · (𝑈𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)))
211195, 210oveq12d 6860 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
212131, 135, 138divcld 11055 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ)
213 subcl 10534 . . . . . . . . . . . . . . . . . . 19 ((1 ∈ ℂ ∧ (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ ℂ) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
21444, 212, 213sylancr 581 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) ∈ ℂ)
215 simp3l 1258 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑍𝑖) ∈ ℂ)
216129, 215mulcld 10314 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑃)) · (𝑍𝑖)) ∈ ℂ)
217214, 216mulcld 10314 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) ∈ ℂ)
218133, 215mulcld 10314 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (𝐹𝑅)) · (𝑍𝑖)) ∈ ℂ)
219212, 218mulcld 10314 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) ∈ ℂ)
220 simp3r 1259 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (𝑈𝑖) ∈ ℂ)
221128, 220mulcld 10314 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑃) · (𝑈𝑖)) ∈ ℂ)
222214, 221mulcld 10314 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) ∈ ℂ)
223125, 220mulcld 10314 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((𝐹𝑅) · (𝑈𝑖)) ∈ ℂ)
224212, 223mulcld 10314 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))) ∈ ℂ)
225217, 219, 222, 224add4d 10518 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
226214, 129mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) ∈ ℂ)
227212, 133mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) ∈ ℂ)
228226, 227, 215adddird 10319 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖))))
229214, 129, 215mulassd 10317 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))))
230212, 133, 215mulassd 10317 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))))
231229, 230oveq12d 6860 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) · (𝑍𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅))) · (𝑍𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
232228, 231eqtrd 2799 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))))
233214, 128mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) ∈ ℂ)
234212, 125mulcld 10314 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) ∈ ℂ)
235233, 234, 220adddird 10319 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖))))
236214, 128, 220mulassd 10317 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))))
237212, 125, 220mulassd 10317 . . . . . . . . . . . . . . . . . . 19 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖)) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))
238236, 237oveq12d 6860 . . . . . . . . . . . . . . . . . 18 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) · (𝑈𝑖)) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅)) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
239235, 238eqtrd 2799 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖)) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
240232, 239oveq12d 6860 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖)))) + (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
241214, 216, 221adddid 10318 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))))
242212, 218, 223adddid 10318 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖)))))
243241, 242oveq12d 6860 . . . . . . . . . . . . . . . 16 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((1 − (𝐹𝑃)) · (𝑍𝑖))) + ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · ((𝐹𝑃) · (𝑈𝑖)))) + (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((1 − (𝐹𝑅)) · (𝑍𝑖))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · ((𝐹𝑅) · (𝑈𝑖))))))
244225, 240, 2433eqtr4rd 2810 . . . . . . . . . . . . . . 15 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (1 − (𝐹𝑃))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (1 − (𝐹𝑅)))) · (𝑍𝑖)) + ((((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (𝐹𝑃)) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (𝐹𝑅))) · (𝑈𝑖))))
245211, 244eqtr4d 2802 . . . . . . . . . . . . . 14 ((((𝐹𝑃) ∈ ℂ ∧ (𝐹𝑃) ≠ (𝐹𝑅)) ∧ ((𝐹𝑄) ∈ ℂ ∧ (𝐹𝑅) ∈ ℂ) ∧ ((𝑍𝑖) ∈ ℂ ∧ (𝑈𝑖) ∈ ℂ)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
246113, 114, 117, 120, 122, 124, 245syl222anc 1505 . . . . . . . . . . . . 13 ((((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
247246ralrimiva 3113 . . . . . . . . . . . 12 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
248 oveq2 6850 . . . . . . . . . . . . . . . . 17 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (1 − 𝑡) = (1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))))
249248oveq1d 6857 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) = ((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
250 oveq1 6849 . . . . . . . . . . . . . . . 16 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) = ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
251249, 250oveq12d 6860 . . . . . . . . . . . . . . 15 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
252251eqeq2d 2775 . . . . . . . . . . . . . 14 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → ((((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
253252ralbidv 3133 . . . . . . . . . . . . 13 (𝑡 = (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
254253rspcev 3461 . . . . . . . . . . . 12 (((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − (((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃)))) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + ((((𝐹𝑄) − (𝐹𝑃)) / ((𝐹𝑅) − (𝐹𝑃))) · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
255110, 247, 254syl2anc 579 . . . . . . . . . . 11 (((𝐹𝑃) ≠ (𝐹𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
256255ex 401 . . . . . . . . . 10 ((𝐹𝑃) ≠ (𝐹𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
25784, 256pm2.61ine 3020 . . . . . . . . 9 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
258 r19.26-3 3213 . . . . . . . . . 10 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
259 simp2 1167 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))))
260 oveq2 6850 . . . . . . . . . . . . . . . . 17 ((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) → ((1 − 𝑡) · (𝑃𝑖)) = ((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))))
261 oveq2 6850 . . . . . . . . . . . . . . . . 17 ((𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))) → (𝑡 · (𝑅𝑖)) = (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))
262260, 261oveqan12d 6861 . . . . . . . . . . . . . . . 16 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
2632623adant2 1161 . . . . . . . . . . . . . . 15 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))))
264259, 263eqeq12d 2780 . . . . . . . . . . . . . 14 (((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
265264ralimi 3099 . . . . . . . . . . . . 13 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
266 ralbi 3215 . . . . . . . . . . . . 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 3199 . . . . . . . . . . 11 (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))))))
269268biimprcd 241 . . . . . . . . . 10 (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) = (((1 − 𝑡) · (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) + (𝑡 · (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ (𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ (𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
270258, 269syl5bir 234 . . . . . . . . 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 642 . . . . . . 7 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) ∧ ((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
273272expimpd 445 . . . . . 6 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
274273adantlr 706 . . . . 5 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ (𝐹𝑄) ∈ (0[,)+∞) ∧ (𝐹𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27512, 274syl5bi 233 . . . 4 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ((((𝐹𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃𝑖) = (((1 − (𝐹𝑃)) · (𝑍𝑖)) + ((𝐹𝑃) · (𝑈𝑖)))) ∧ ((𝐹𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − (𝐹𝑄)) · (𝑍𝑖)) + ((𝐹𝑄) · (𝑈𝑖)))) ∧ ((𝐹𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅𝑖) = (((1 − (𝐹𝑅)) · (𝑍𝑖)) + ((𝐹𝑅) · (𝑈𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
27611, 275mpd 15 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖))))
277 simpl1 1242 . . . . 5 (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) → 𝑁 ∈ ℕ)
278 ssrab2 3847 . . . . . . . . 9 {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)} ⊆ (𝔼‘𝑁)
2791, 278eqsstri 3795 . . . . . . . 8 𝐷 ⊆ (𝔼‘𝑁)
280279sseli 3757 . . . . . . 7 (𝑄𝐷𝑄 ∈ (𝔼‘𝑁))
281279sseli 3757 . . . . . . 7 (𝑃𝐷𝑃 ∈ (𝔼‘𝑁))
282279sseli 3757 . . . . . . 7 (𝑅𝐷𝑅 ∈ (𝔼‘𝑁))
283280, 281, 2823anim123i 1190 . . . . . 6 ((𝑄𝐷𝑃𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
2842833com12 1153 . . . . 5 ((𝑃𝐷𝑄𝐷𝑅𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
285 brbtwn 26070 . . . . . 6 ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
286285adantl 473 . . . . 5 ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
287277, 284, 286syl2an 589 . . . 4 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
288287adantr 472 . . 3 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄𝑖) = (((1 − 𝑡) · (𝑃𝑖)) + (𝑡 · (𝑅𝑖)))))
289276, 288mpbird 248 . 2 (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) ∧ ((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
290289ex 401 1 ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍𝑈) ∧ (𝑃𝐷𝑄𝐷𝑅𝐷)) → (((𝐹𝑃) ≤ (𝐹𝑄) ∧ (𝐹𝑄) ≤ (𝐹𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  wral 3055  wrex 3056  {crab 3059  cop 4340   class class class wbr 4809  {copab 4871  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  +∞cpnf 10325   < clt 10328  cle 10329  cmin 10520   / cdiv 10938  cn 11274  [,)cico 12379  [,]cicc 12380  ...cfz 12533  𝔼cee 26059   Btwn cbtwn 26060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-map 8062  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-z 11625  df-uz 11887  df-ico 12383  df-icc 12384  df-fz 12534  df-ee 26062  df-btwn 26063
This theorem is referenced by:  axcontlem10  26144
  Copyright terms: Public domain W3C validator