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 29261

Description: Lemma for axcont 29266. 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 29259	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑃 ∈ 𝐷) → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
4	3	ex 417	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑃 ∈ 𝐷 → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
5	1, 2	axcontlem6 29259	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑄 ∈ 𝐷) → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))
6	5	ex 417	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑄 ∈ 𝐷 → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
7	1, 2	axcontlem6 29259	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑅 ∈ 𝐷) → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
8	7	ex 417	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑅 ∈ 𝐷 → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
9	4, 6, 8	3anim123d 1469	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
10	9	imp 411	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
11	10	adantr 485	. . . 4 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
12		3an6 1472	. . . . 5 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
13		0elunit 13495	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
14		simplr1 1232	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑃) ∈ (0[,)+∞))
15	14	ad2antlr 739	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞))
16		elrege0 13480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) ↔ ((𝐹‘𝑃) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑃)))
17	16	simplbi 501	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℝ)
18	15, 17	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℝ)
19	18	recnd 11236	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ)
20		simprrl 792	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
21	20	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
22		simprrr 793	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅))
23		simpl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) = (𝐹‘𝑅))
24	22, 23	breqtrrd 5143	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑃))
25	24	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ≤ (𝐹‘𝑃))
26		simplr2 1233	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑄) ∈ (0[,)+∞))
27	26	ad2antlr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞))
28		elrege0 13480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) ↔ ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄)))
29	28	simplbi 501	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℝ)
30	27, 29	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℝ)
31	18, 30	letri3d 11351	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹‘𝑃) = (𝐹‘𝑄) ↔ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑃))))
32	21, 25, 31	mpbir2and 725	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑄))
33		simpll 778	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑅))
34		simpll2 1230	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
35	34	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
36	35	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37		fveecn 29192	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
38	36, 37	sylancom 599	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
39		simpll3 1231	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
40	39	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
41	40	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42		fveecn 29192	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
43	41, 42	sylancom 599	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
44		ax-1cn 11157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
45		simpl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ)
46		subcl 11455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (1 − (𝐹‘𝑃)) ∈ ℂ)
47	44, 45, 46	sylancr 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ)
48		simprl 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
49	47, 48	mulcld 11228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ)
50		mulcl 11183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
51	50	adantrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
52	49, 51	addcld 11227	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ)
53	52	mullidd 11226	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))
54	52	mul02d 11407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = 0)
55	53, 54	oveq12d 7429	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0))
56	52	addridd 11409	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))
57	55, 56	eqtr2d 2805	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
58	57	3adant2 1147	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
59		oveq2 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑄)))
60	59	oveq1d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))
61		oveq1 7418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑄) · (𝑈‘𝑖)))
62	60, 61	oveq12d 7429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))
63		oveq2 7419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑅)))
64	63	oveq1d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))
65		oveq1 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑅) · (𝑈‘𝑖)))
66	64, 65	oveq12d 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))
67	66	oveq2d 7427	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
68	67	oveq2d 7427	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
69	62, 68	eqeqan12d 2783	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
70	69	3ad2ant2 1150	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
71	58, 70	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
72	19, 32, 33, 38, 43, 71	syl122anc 1404	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
73	72	ralrimiva 3163	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
74		oveq2 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75		1m0e1 12359	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 0) = 1
76	74, 75	eqtrdi 2820	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
77	76	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
78		oveq1 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
79	77, 78	oveq12d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
80	79	eqeq2d 2780	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 0 → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
81	80	ralbidv 3194	. . . . . . . . . . . . 13 ⊢ (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
82	81	rspcev 3590	. . . . . . . . . . . 12 ⊢ ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
83	13, 73, 82	sylancr 598	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
84	83	ex 417	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
85	26	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ (0[,)+∞))
86	85, 29	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ ℝ)
87		simplr3 1234	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑅) ∈ (0[,)+∞))
88	87	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ (0[,)+∞))
89		elrege0 13480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) ↔ ((𝐹‘𝑅) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑅)))
90	89	simplbi 501	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℝ)
91	88, 90	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ ℝ)
92	14	adantl 486	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ (0[,)+∞))
93	92, 17	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ ℝ)
94		simprrr 793	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅))
95	86, 91, 93, 94	lesub1dd 11829	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃)))
96	86, 93	resubcld 11641	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ)
97		simprrl 792	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
98	86, 93	subge0d 11803	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃)) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
99	97, 98	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃)))
100	91, 93	resubcld 11641	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ)
101	93, 86, 91, 97, 94	letrd 11366	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑅))
102		simpl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
103	102	necomd 3019	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ≠ (𝐹‘𝑃))
104	93, 91, 101, 103	leneltd 11363	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) < (𝐹‘𝑅))
105	93, 91	posdifd 11800	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑃) < (𝐹‘𝑅) ↔ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃))))
106	104, 105	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))
107		divelunit 13520	. . . . . . . . . . . . . 14 ⊢ (((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃))) ∧ (((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃))))
108	96, 99, 100, 106, 107	syl22anc 851	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃))))
109	95, 108	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1))
110	14	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞))
111	17	recnd 11236	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℂ)
112	110, 111	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ)
113		simpll 778	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
114	26	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞))
115	29	recnd 11236	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℂ)
116	114, 115	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℂ)
117	87	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ (0[,)+∞))
118	90	recnd 11236	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℂ)
119	117, 118	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ ℂ)
120	34	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
121	120, 37	sylan 591	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
122	39	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
123	122, 42	sylan 591	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
124		simp2r 1217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ∈ ℂ)
125		simp2l 1216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) ∈ ℂ)
126	124, 125	subcld 11568	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ)
127		simp1l 1214	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ)
128	44, 127, 46	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ)
129	126, 128	mulcld 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) ∈ ℂ)
130	125, 127	subcld 11568	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ)
131		subcl 11455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (1 − (𝐹‘𝑅)) ∈ ℂ)
132	44, 124, 131	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑅)) ∈ ℂ)
133	130, 132	mulcld 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) ∈ ℂ)
134	124, 127	subcld 11568	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ)
135		simp1r 1215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
136	135	necomd 3019	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ≠ (𝐹‘𝑃))
137	124, 127, 136	subne0d 11577	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ≠ 0)
138	129, 133, 134, 137	divdird 12028	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
139	134	mulridd 11225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑃)))
140	134, 125	mulcomd 11229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃))))
141	125, 124, 127	subdid 11669	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
142	140, 141	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
143	139, 142	oveq12d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
144		subdi 11646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
145	44, 144	mp3an2 1475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
146	134, 125, 145	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
147		subdi 11646	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
148	44, 147	mp3an2 1475	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
149	126, 127, 148	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
150	126	mulridd 11225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑄)))
151	124, 125, 127	subdird 11670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
152	124, 127	mulcomd 11229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝐹‘𝑃)) = ((𝐹‘𝑃) · (𝐹‘𝑅)))
153	152	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
154	151, 153	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
155	150, 154	oveq12d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
156	149, 155	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
157		subdi 11646	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
158	44, 157	mp3an2 1475	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
159	130, 124, 158	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
160	130	mulridd 11225	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑄) − (𝐹‘𝑃)))
161	125, 127, 124	subdird 11670	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))
162	160, 161	oveq12d 7429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
163	159, 162	eqtrd 2804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
164	156, 163	oveq12d 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))))
165	127, 124	mulcld 11228	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝐹‘𝑅)) ∈ ℂ)
166	125, 127	mulcld 11228	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑃)) ∈ ℂ)
167	165, 166	subcld 11568	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) ∈ ℂ)
168		mulcl 11183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ)
169	168	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ)
170	169, 165	subcld 11568	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))) ∈ ℂ)
171	126, 130, 167, 170	addsub4d 11615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))))
172	124, 125, 127	npncand 11592	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑃)))
173	165, 166, 169	npncan3d 11604	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
174	172, 173	oveq12d 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
175	164, 171, 174	3eqtr2d 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
176	143, 146, 175	3eqtr4d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))))
177	129, 133	addcld 11227	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) ∈ ℂ)
178		subcl 11455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − (𝐹‘𝑄)) ∈ ℂ)
179	44, 125, 178	sylancr 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) ∈ ℂ)
180	177, 134, 179, 137	divmuld 12012	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄)) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))))))
181	176, 180	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄)))
182	126, 128, 134, 137	div23d 12027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃))))
183	134, 130, 134, 137	divsubdird 12029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
184	124, 125, 127	nnncan2d 11603	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑄)))
185	184	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))
186	134, 137	dividd 11988	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = 1)
187	186	oveq1d 7426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
188	183, 185, 187	3eqtr3d 2812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
189	188	oveq1d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))))
190	182, 189	eqtrd 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))))
191	130, 132, 134, 137	div23d 12027	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))))
192	190, 191	oveq12d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))))
193	138, 181, 192	3eqtr3d 2812	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))))
194	193	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)))
195	126, 127	mulcld 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) ∈ ℂ)
196	130, 124	mulcld 11228	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) ∈ ℂ)
197	195, 196, 134, 137	divdird 12028	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
198	154, 161	oveq12d 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
199	173, 198, 142	3eqtr4rd 2815	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
200	195, 196	addcld 11227	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) ∈ ℂ)
201	200, 134, 125, 137	divmuld 12012	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)))))
202	199, 201	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄))
203	126, 127, 134, 137	div23d 12027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃)))
204	188	oveq1d 7426	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)))
205	203, 204	eqtrd 2804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)))
206	130, 124, 134, 137	div23d 12027	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)))
207	205, 206	oveq12d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))))
208	197, 202, 207	3eqtr3d 2812	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))))
209	208	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝑈‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)))
210	194, 209	oveq12d 7429	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))))
211	130, 134, 137	divcld 11990	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ)
212		subcl 11455	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ) → (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ)
213	44, 211, 212	sylancr 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ)
214		simp3l 1218	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
215	128, 214	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ)
216	213, 215	mulcld 11228	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) ∈ ℂ)
217	132, 214	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) ∈ ℂ)
218	211, 217	mulcld 11228	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) ∈ ℂ)
219		simp3r 1219	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
220	127, 219	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
221	213, 220	mulcld 11228	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ)
222	124, 219	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝑈‘𝑖)) ∈ ℂ)
223	211, 222	mulcld 11228	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))) ∈ ℂ)
224	216, 218, 221, 223	add4d 11438	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
225	213, 128	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) ∈ ℂ)
226	211, 132	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) ∈ ℂ)
227	213, 128, 214	mulassd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))))
228	211, 132, 214	mulassd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))))
229	227, 228	oveq12d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))))
230	225, 214, 226, 229	joinlmuladdmuld 11235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))))
231	213, 127	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) ∈ ℂ)
232	211, 124	mulcld 11228	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) ∈ ℂ)
233	213, 127, 219	mulassd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))))
234	211, 124, 219	mulassd 11231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))
235	233, 234	oveq12d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
236	231, 219, 232, 235	joinlmuladdmuld 11235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
237	230, 236	oveq12d 7429	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
238	213, 215, 220	adddid 11232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))))
239	211, 217, 222	adddid 11232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
240	238, 239	oveq12d 7429	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
241	224, 237, 240	3eqtr4rd 2815	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))))
242	210, 241	eqtr4d 2807	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
243	112, 113, 116, 119, 121, 123, 242	syl222anc 1411	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
244	243	ralrimiva 3163	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
245		oveq2 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (1 − 𝑡) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
246	245	oveq1d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
247		oveq1 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
248	246, 247	oveq12d 7429	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
249	248	eqeq2d 2780	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
250	249	ralbidv 3194	. . . . . . . . . . . . 13 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
251	250	rspcev 3590	. . . . . . . . . . . 12 ⊢ (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
252	109, 244, 251	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
253	252	ex 417	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) ≠ (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
254	84, 253	pm2.61ine 3047	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
255		r19.26-3 3132	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
256		simp2 1153	. . . . . . . . . . . . . . 15 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))
257		oveq2 7419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) → ((1 − 𝑡) · (𝑃‘𝑖)) = ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
258		oveq2 7419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))) → (𝑡 · (𝑅‘𝑖)) = (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
259	257, 258	oveqan12d 7430	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
260	259	3adant2 1147	. . . . . . . . . . . . . . 15 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
261	256, 260	eqeq12d 2785	. . . . . . . . . . . . . 14 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
262	261	ralimi 3108	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
263		ralbi 3126	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
264	262, 263	syl 18	. . . . . . . . . . . 12 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
265	264	rexbidv 3195	. . . . . . . . . . 11 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
266	265	biimprcd 253	. . . . . . . . . 10 ⊢ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
267	255, 266	biimtrrid 246	. . . . . . . . 9 ⊢ (∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
268	254, 267	syl 18	. . . . . . . 8 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
269	268	an32s 664	. . . . . . 7 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
270	269	expimpd 458	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
271	270	adantlr 727	. . . . 5 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
272	12, 271	biimtrid 245	. . . 4 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
273	11, 272	mpd 16	. . 3 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))))
274		simpl1 1208	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑁 ∈ ℕ)
275	1	ssrab3 4044	. . . . . . . 8 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
276	275	sseli 3941	. . . . . . 7 ⊢ (𝑄 ∈ 𝐷 → 𝑄 ∈ (𝔼‘𝑁))
277	275	sseli 3941	. . . . . . 7 ⊢ (𝑃 ∈ 𝐷 → 𝑃 ∈ (𝔼‘𝑁))
278	275	sseli 3941	. . . . . . 7 ⊢ (𝑅 ∈ 𝐷 → 𝑅 ∈ (𝔼‘𝑁))
279	276, 277, 278	3anim123i 1167	. . . . . 6 ⊢ ((𝑄 ∈ 𝐷 ∧ 𝑃 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
280	279	3com12 1139	. . . . 5 ⊢ ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
281		brbtwn 29189	. . . . . 6 ⊢ ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
282	281	adantl 486	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
283	274, 280, 282	syl2an 607	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
284	283	adantr 485	. . 3 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
285	273, 284	mpbird 260	. 2 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
286	285	ex 417	1 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 {crab 3423 ⟨cop 4600 class class class wbr 5113 {copab 5177 ‘cfv 6537 (class class class)co 7411 ℂcc 11097 ℝcr 11098 0cc0 11099 1c1 11100 + caddc 11102 · cmul 11104 +∞cpnf 11239 < clt 11242 ≤ cle 11243 − cmin 11440 / cdiv 11870 ℕcn 12232 [,)cico 13373 [,]cicc 13374 ...cfz 13534 𝔼cee 29177 Btwn cbtwn 29178

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-z 12591 df-uz 12862 df-ico 13377 df-icc 13378 df-fz 13535 df-ee 29180 df-btwn 29181

This theorem is referenced by: axcontlem10 29263

W3C validator