axcontlem8 - Metamath Proof Explorer

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

Theorem axcontlem8 28986

Description: Lemma for axcont 28991. 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**
Step	Hyp	Ref	Expression
1		axcontlem8.1	. . . . . . . . 9 ⊢ 𝐷 = {𝑝 ∈ (𝔼‘𝑁) ∣ (𝑈 Btwn ⟨𝑍, 𝑝⟩ ∨ 𝑝 Btwn ⟨𝑍, 𝑈⟩)}
2		axcontlem8.2	. . . . . . . . 9 ⊢ 𝐹 = {⟨𝑥, 𝑡⟩ ∣ (𝑥 ∈ 𝐷 ∧ (𝑡 ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑥‘𝑖) = (((1 − 𝑡) · (𝑍‘𝑖)) + (𝑡 · (𝑈‘𝑖)))))}
3	1, 2	axcontlem6 28984	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑃 ∈ 𝐷) → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
4	3	ex 412	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑃 ∈ 𝐷 → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
5	1, 2	axcontlem6 28984	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑄 ∈ 𝐷) → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))
6	5	ex 412	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑄 ∈ 𝐷 → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
7	1, 2	axcontlem6 28984	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑅 ∈ 𝐷) → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
8	7	ex 412	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑅 ∈ 𝐷 → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
9	4, 6, 8	3anim123d 1445	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
10	9	imp 406	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
11	10	adantr 480	. . . 4 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
12		3an6 1448	. . . . 5 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
13		0elunit 13509	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
14		simplr1 1216	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑃) ∈ (0[,)+∞))
15	14	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞))
16		elrege0 13494	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) ↔ ((𝐹‘𝑃) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑃)))
17	16	simplbi 497	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℝ)
18	15, 17	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℝ)
19	18	recnd 11289	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ)
20		simprrl 781	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
21	20	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
22		simprrr 782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅))
23		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) = (𝐹‘𝑅))
24	22, 23	breqtrrd 5171	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑃))
25	24	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ≤ (𝐹‘𝑃))
26		simplr2 1217	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑄) ∈ (0[,)+∞))
27	26	ad2antlr 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞))
28		elrege0 13494	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) ↔ ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄)))
29	28	simplbi 497	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℝ)
30	27, 29	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℝ)
31	18, 30	letri3d 11403	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹‘𝑃) = (𝐹‘𝑄) ↔ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑃))))
32	21, 25, 31	mpbir2and 713	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑄))
33		simpll 767	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑅))
34		simpll2 1214	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
35	34	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
36	35	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37		fveecn 28917	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
38	36, 37	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
39		simpll3 1215	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
40	39	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
41	40	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42		fveecn 28917	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
43	41, 42	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
44		ax-1cn 11213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
45		simpl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ)
46		subcl 11507	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (1 − (𝐹‘𝑃)) ∈ ℂ)
47	44, 45, 46	sylancr 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ)
48		simprl 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
49	47, 48	mulcld 11281	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ)
50		mulcl 11239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
51	50	adantrl 716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
52	49, 51	addcld 11280	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ)
53	52	mullidd 11279	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))
54	52	mul02d 11459	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = 0)
55	53, 54	oveq12d 7449	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0))
56	52	addridd 11461	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))
57	55, 56	eqtr2d 2778	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
58	57	3adant2 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
59		oveq2 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑄)))
60	59	oveq1d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))
61		oveq1 7438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑄) · (𝑈‘𝑖)))
62	60, 61	oveq12d 7449	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))
63		oveq2 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑅)))
64	63	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))
65		oveq1 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑅) · (𝑈‘𝑖)))
66	64, 65	oveq12d 7449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))
67	66	oveq2d 7447	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
68	67	oveq2d 7447	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
69	62, 68	eqeqan12d 2751	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
70	69	3ad2ant2 1135	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
71	58, 70	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
72	19, 32, 33, 38, 43, 71	syl122anc 1381	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
73	72	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
74		oveq2 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75		1m0e1 12387	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 0) = 1
76	74, 75	eqtrdi 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
77	76	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
78		oveq1 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
79	77, 78	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
80	79	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 0 → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
81	80	ralbidv 3178	. . . . . . . . . . . . 13 ⊢ (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
82	81	rspcev 3622	. . . . . . . . . . . 12 ⊢ ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
83	13, 73, 82	sylancr 587	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
84	83	ex 412	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
85	26	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ (0[,)+∞))
86	85, 29	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ ℝ)
87		simplr3 1218	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑅) ∈ (0[,)+∞))
88	87	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ (0[,)+∞))
89		elrege0 13494	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) ↔ ((𝐹‘𝑅) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑅)))
90	89	simplbi 497	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℝ)
91	88, 90	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ ℝ)
92	14	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ (0[,)+∞))
93	92, 17	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ ℝ)
94		simprrr 782	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅))
95	86, 91, 93, 94	lesub1dd 11879	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃)))
96	86, 93	resubcld 11691	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ)
97		simprrl 781	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
98	86, 93	subge0d 11853	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃)) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
99	97, 98	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃)))
100	91, 93	resubcld 11691	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ)
101	93, 86, 91, 97, 94	letrd 11418	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑅))
102		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
103	102	necomd 2996	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ≠ (𝐹‘𝑃))
104	93, 91, 101, 103	leneltd 11415	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) < (𝐹‘𝑅))
105	93, 91	posdifd 11850	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑃) < (𝐹‘𝑅) ↔ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃))))
106	104, 105	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))
107		divelunit 13534	. . . . . . . . . . . . . 14 ⊢ (((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃))) ∧ (((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃))))
108	96, 99, 100, 106, 107	syl22anc 839	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃))))
109	95, 108	mpbird 257	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1))
110	14	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞))
111	17	recnd 11289	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℂ)
112	110, 111	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ)
113		simpll 767	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
114	26	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞))
115	29	recnd 11289	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℂ)
116	114, 115	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℂ)
117	87	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ (0[,)+∞))
118	90	recnd 11289	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℂ)
119	117, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ ℂ)
120	34	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
121	120, 37	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
122	39	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
123	122, 42	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
124		simp2r 1201	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ∈ ℂ)
125		simp2l 1200	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) ∈ ℂ)
126	124, 125	subcld 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ)
127		simp1l 1198	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ)
128	44, 127, 46	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ)
129	126, 128	mulcld 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) ∈ ℂ)
130	125, 127	subcld 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ)
131		subcl 11507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (1 − (𝐹‘𝑅)) ∈ ℂ)
132	44, 124, 131	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑅)) ∈ ℂ)
133	130, 132	mulcld 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) ∈ ℂ)
134	124, 127	subcld 11620	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ)
135		simp1r 1199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
136	135	necomd 2996	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ≠ (𝐹‘𝑃))
137	124, 127, 136	subne0d 11629	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ≠ 0)
138	129, 133, 134, 137	divdird 12081	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
139	134	mulridd 11278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑃)))
140	134, 125	mulcomd 11282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃))))
141	125, 124, 127	subdid 11719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
142	140, 141	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
143	139, 142	oveq12d 7449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
144		subdi 11696	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
145	44, 144	mp3an2 1451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
146	134, 125, 145	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
147		subdi 11696	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
148	44, 147	mp3an2 1451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
149	126, 127, 148	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
150	126	mulridd 11278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑄)))
151	124, 125, 127	subdird 11720	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
152	124, 127	mulcomd 11282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝐹‘𝑃)) = ((𝐹‘𝑃) · (𝐹‘𝑅)))
153	152	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
154	151, 153	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
155	150, 154	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
156	149, 155	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
157		subdi 11696	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
158	44, 157	mp3an2 1451	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
159	130, 124, 158	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
160	130	mulridd 11278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑄) − (𝐹‘𝑃)))
161	125, 127, 124	subdird 11720	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))
162	160, 161	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
163	159, 162	eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
164	156, 163	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))))
165	127, 124	mulcld 11281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝐹‘𝑅)) ∈ ℂ)
166	125, 127	mulcld 11281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑃)) ∈ ℂ)
167	165, 166	subcld 11620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) ∈ ℂ)
168		mulcl 11239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ)
169	168	3ad2ant2 1135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ)
170	169, 165	subcld 11620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))) ∈ ℂ)
171	126, 130, 167, 170	addsub4d 11667	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))))
172	124, 125, 127	npncand 11644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑃)))
173	165, 166, 169	npncan3d 11656	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
174	172, 173	oveq12d 7449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
175	164, 171, 174	3eqtr2d 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
176	143, 146, 175	3eqtr4d 2787	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))))
177	129, 133	addcld 11280	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) ∈ ℂ)
178		subcl 11507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − (𝐹‘𝑄)) ∈ ℂ)
179	44, 125, 178	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) ∈ ℂ)
180	177, 134, 179, 137	divmuld 12065	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄)) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))))))
181	176, 180	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄)))
182	126, 128, 134, 137	div23d 12080	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃))))
183	134, 130, 134, 137	divsubdird 12082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
184	124, 125, 127	nnncan2d 11655	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑄)))
185	184	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))
186	134, 137	dividd 12041	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = 1)
187	186	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
188	183, 185, 187	3eqtr3d 2785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
189	188	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))))
190	182, 189	eqtrd 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))))
191	130, 132, 134, 137	div23d 12080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))))
192	190, 191	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))))
193	138, 181, 192	3eqtr3d 2785	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))))
194	193	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)))
195	126, 127	mulcld 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) ∈ ℂ)
196	130, 124	mulcld 11281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) ∈ ℂ)
197	195, 196, 134, 137	divdird 12081	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
198	154, 161	oveq12d 7449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
199	173, 198, 142	3eqtr4rd 2788	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
200	195, 196	addcld 11280	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) ∈ ℂ)
201	200, 134, 125, 137	divmuld 12065	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)))))
202	199, 201	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄))
203	126, 127, 134, 137	div23d 12080	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃)))
204	188	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)))
205	203, 204	eqtrd 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)))
206	130, 124, 134, 137	div23d 12080	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)))
207	205, 206	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))))
208	197, 202, 207	3eqtr3d 2785	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))))
209	208	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝑈‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)))
210	194, 209	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))))
211	130, 134, 137	divcld 12043	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ)
212		subcl 11507	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ) → (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ)
213	44, 211, 212	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ)
214		simp3l 1202	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
215	128, 214	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ)
216	213, 215	mulcld 11281	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) ∈ ℂ)
217	132, 214	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) ∈ ℂ)
218	211, 217	mulcld 11281	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) ∈ ℂ)
219		simp3r 1203	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
220	127, 219	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
221	213, 220	mulcld 11281	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ)
222	124, 219	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝑈‘𝑖)) ∈ ℂ)
223	211, 222	mulcld 11281	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))) ∈ ℂ)
224	216, 218, 221, 223	add4d 11490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
225	213, 128	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) ∈ ℂ)
226	211, 132	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) ∈ ℂ)
227	213, 128, 214	mulassd 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))))
228	211, 132, 214	mulassd 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))))
229	227, 228	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))))
230	225, 214, 226, 229	joinlmuladdmuld 11288	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))))
231	213, 127	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) ∈ ℂ)
232	211, 124	mulcld 11281	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) ∈ ℂ)
233	213, 127, 219	mulassd 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))))
234	211, 124, 219	mulassd 11284	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))
235	233, 234	oveq12d 7449	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
236	231, 219, 232, 235	joinlmuladdmuld 11288	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
237	230, 236	oveq12d 7449	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
238	213, 215, 220	adddid 11285	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))))
239	211, 217, 222	adddid 11285	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
240	238, 239	oveq12d 7449	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
241	224, 237, 240	3eqtr4rd 2788	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))))
242	210, 241	eqtr4d 2780	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
243	112, 113, 116, 119, 121, 123, 242	syl222anc 1388	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
244	243	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
245		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (1 − 𝑡) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
246	245	oveq1d 7446	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
247		oveq1 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
248	246, 247	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
249	248	eqeq2d 2748	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
250	249	ralbidv 3178	. . . . . . . . . . . . 13 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
251	250	rspcev 3622	. . . . . . . . . . . 12 ⊢ (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
252	109, 244, 251	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
253	252	ex 412	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) ≠ (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
254	84, 253	pm2.61ine 3025	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
255		r19.26-3 3112	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
256		simp2 1138	. . . . . . . . . . . . . . 15 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))
257		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) → ((1 − 𝑡) · (𝑃‘𝑖)) = ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
258		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))) → (𝑡 · (𝑅‘𝑖)) = (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
259	257, 258	oveqan12d 7450	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
260	259	3adant2 1132	. . . . . . . . . . . . . . 15 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
261	256, 260	eqeq12d 2753	. . . . . . . . . . . . . 14 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
262	261	ralimi 3083	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
263		ralbi 3103	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
264	262, 263	syl 17	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
265	264	rexbidv 3179	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
266	265	biimprcd 250	. . . . . . . . . 10 ⊢ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
267	255, 266	biimtrrid 243	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
268	254, 267	syl 17	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
269	268	an32s 652	. . . . . . 7 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
270	269	expimpd 453	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
271	270	adantlr 715	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
272	12, 271	biimtrid 242	. . . 4 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
273	11, 272	mpd 15	. . 3 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))
274		simpl1 1192	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑁 ∈ ℕ)
275	1	ssrab3 4082	. . . . . . . 8 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
276	275	sseli 3979	. . . . . . 7 ⊢ (𝑄 ∈ 𝐷 → 𝑄 ∈ (𝔼‘𝑁))
277	275	sseli 3979	. . . . . . 7 ⊢ (𝑃 ∈ 𝐷 → 𝑃 ∈ (𝔼‘𝑁))
278	275	sseli 3979	. . . . . . 7 ⊢ (𝑅 ∈ 𝐷 → 𝑅 ∈ (𝔼‘𝑁))
279	276, 277, 278	3anim123i 1152	. . . . . 6 ⊢ ((𝑄 ∈ 𝐷 ∧ 𝑃 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
280	279	3com12 1124	. . . . 5 ⊢ ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
281		brbtwn 28914	. . . . . 6 ⊢ ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
282	281	adantl 481	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
283	274, 280, 282	syl2an 596	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
284	283	adantr 480	. . 3 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
285	273, 284	mpbird 257	. 2 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
286	285	ex 412	1 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3436 ⟨cop 4632 class class class wbr 5143 {copab 5205 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 +∞cpnf 11292 < clt 11295 ≤ cle 11296 − cmin 11492 / cdiv 11920 ℕcn 12266 [,)cico 13389 [,]cicc 13390 ...cfz 13547 𝔼cee 28903 Btwn cbtwn 28904

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-map 8868 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-z 12614 df-uz 12879 df-ico 13393 df-icc 13394 df-fz 13548 df-ee 28906 df-btwn 28907

This theorem is referenced by: axcontlem10 28988

W3C validator