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 29606

Description: Lemma for axcont 29611. 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 29604	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑃 ∈ 𝐷) → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
4	3	ex 418	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑃 ∈ 𝐷 → ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
5	1, 2	axcontlem6 29604	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑄 ∈ 𝐷) → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))))
6	5	ex 418	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑄 ∈ 𝐷 → ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))))
7	1, 2	axcontlem6 29604	. . . . . . . 8 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ 𝑅 ∈ 𝐷) → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
8	7	ex 418	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → (𝑅 ∈ 𝐷 → ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
9	4, 6, 8	3anim123d 1472	. . . . . 6 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
10	9	imp 412	. . . . 5 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
11	10	adantr 486	. . . 4 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
12		3an6 1476	. . . . 5 ⊢ ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑄) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖)))) ∧ ((𝐹‘𝑅) ∈ (0[,)+∞) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
13		0elunit 13640	. . . . . . . . . . . 12 ⊢ 0 ∈ (0[,]1)
14		simplr1 1234	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑃) ∈ (0[,)+∞))
15	14	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞))
16		elrege0 13625	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) ↔ ((𝐹‘𝑃) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑃)))
17	16	simplbi 502	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℝ)
18	15, 17	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℝ)
19	18	recnd 11376	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ)
20		simprrl 793	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
21	20	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
22		simprrr 794	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅))
23		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) = (𝐹‘𝑅))
24	22, 23	breqtrrd 5139	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑃))
25	24	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ≤ (𝐹‘𝑃))
26		simplr2 1235	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑄) ∈ (0[,)+∞))
27	26	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞))
28		elrege0 13625	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) ↔ ((𝐹‘𝑄) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑄)))
29	28	simplbi 502	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℝ)
30	27, 29	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℝ)
31	18, 30	letri3d 11491	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → ((𝐹‘𝑃) = (𝐹‘𝑄) ↔ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑃))))
32	21, 25, 31	mpbir2and 726	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑄))
33		simpll 779	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) = (𝐹‘𝑅))
34		simpll2 1232	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑍 ∈ (𝔼‘𝑁))
35	34	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑍 ∈ (𝔼‘𝑁))
36	35	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑍 ∈ (𝔼‘𝑁))
37		fveecn 29537	. . . . . . . . . . . . . . 15 ⊢ ((𝑍 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
38	36, 37	sylancom 600	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
39		simpll3 1233	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → 𝑈 ∈ (𝔼‘𝑁))
40	39	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑈 ∈ (𝔼‘𝑁))
41	40	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → 𝑈 ∈ (𝔼‘𝑁))
42		fveecn 29537	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ (𝔼‘𝑁) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
43	41, 42	sylancom 600	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
44		ax-1cn 11297	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
45		simpl 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ)
46		subcl 11595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (1 − (𝐹‘𝑃)) ∈ ℂ)
47	44, 45, 46	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ)
48		simprl 783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
49	47, 48	mulcld 11368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ)
50		mulcl 11323	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
51	50	adantrl 729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
52	49, 51	addcld 11367	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ)
53	52	mullidd 11366	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))
54	52	mul02d 11547	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = 0)
55	53, 54	oveq12d 7469	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0))
56	52	addridd 11549	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) + 0) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))
57	55, 56	eqtr2d 2799	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
58	57	3adant2 1149	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ∈ ℂ ∧ ((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))))
59		oveq2 7459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑄)))
60	59	oveq1d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)))
61		oveq1 7458	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑄) · (𝑈‘𝑖)))
62	60, 61	oveq12d 7469	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑄) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))
63		oveq2 7459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (1 − (𝐹‘𝑃)) = (1 − (𝐹‘𝑅)))
64	63	oveq1d 7466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) = ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))
65		oveq1 7458	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((𝐹‘𝑃) · (𝑈‘𝑖)) = ((𝐹‘𝑅) · (𝑈‘𝑖)))
66	64, 65	oveq12d 7469	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))
67	66	oveq2d 7467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
68	67	oveq2d 7467	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
69	62, 68	eqeqan12d 2777	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑄) ∧ (𝐹‘𝑃) = (𝐹‘𝑅)) → ((((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
70	69	3ad2ant2 1152	. . . . . . . . . . . . . . 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 1407	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
73	72	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
74		oveq2 7459	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 0 → (1 − 𝑡) = (1 − 0))
75		1m0e1 12502	. . . . . . . . . . . . . . . . . 18 ⊢ (1 − 0) = 1
76	74, 75	eqtrdi 2814	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = 0 → (1 − 𝑡) = 1)
77	76	oveq1d 7466	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
78		oveq1 7458	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = 0 → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
79	77, 78	oveq12d 7469	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 0 → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
80	79	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 0 → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
81	80	ralbidv 3189	. . . . . . . . . . . . 13 ⊢ (𝑡 = 0 → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
82	81	rspcev 3580	. . . . . . . . . . . 12 ⊢ ((0 ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = ((1 · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (0 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
83	13, 73, 82	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) = (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
84	83	ex 418	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) = (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
85	26	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ (0[,)+∞))
86	85, 29	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ∈ ℝ)
87		simplr3 1236	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝐹‘𝑅) ∈ (0[,)+∞))
88	87	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ (0[,)+∞))
89		elrege0 13625	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) ↔ ((𝐹‘𝑅) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑅)))
90	89	simplbi 502	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℝ)
91	88, 90	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ∈ ℝ)
92	14	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ (0[,)+∞))
93	92, 17	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ∈ ℝ)
94		simprrr 794	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑄) ≤ (𝐹‘𝑅))
95	86, 91, 93, 94	lesub1dd 11972	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃)))
96	86, 93	resubcld 11783	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ)
97		simprrl 793	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑄))
98	86, 93	subge0d 11946	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃)) ↔ (𝐹‘𝑃) ≤ (𝐹‘𝑄)))
99	97, 98	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃)))
100	91, 93	resubcld 11783	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ)
101	93, 86, 91, 97, 94	letrd 11506	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≤ (𝐹‘𝑅))
102		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
103	102	necomd 3014	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑅) ≠ (𝐹‘𝑃))
104	93, 91, 101, 103	leneltd 11503	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (𝐹‘𝑃) < (𝐹‘𝑅))
105	93, 91	posdifd 11943	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((𝐹‘𝑃) < (𝐹‘𝑅) ↔ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃))))
106	104, 105	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))
107		divelunit 13665	. . . . . . . . . . . . . 14 ⊢ (((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 ≤ ((𝐹‘𝑄) − (𝐹‘𝑃))) ∧ (((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℝ ∧ 0 < ((𝐹‘𝑅) − (𝐹‘𝑃)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃))))
108	96, 99, 100, 106, 107	syl22anc 852	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ↔ ((𝐹‘𝑄) − (𝐹‘𝑃)) ≤ ((𝐹‘𝑅) − (𝐹‘𝑃))))
109	95, 108	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1))
110	14	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ (0[,)+∞))
111	17	recnd 11376	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑃) ∈ (0[,)+∞) → (𝐹‘𝑃) ∈ ℂ)
112	110, 111	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ∈ ℂ)
113		simpll 779	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
114	26	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ (0[,)+∞))
115	29	recnd 11376	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑄) ∈ (0[,)+∞) → (𝐹‘𝑄) ∈ ℂ)
116	114, 115	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑄) ∈ ℂ)
117	87	ad2antlr 740	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ (0[,)+∞))
118	90	recnd 11376	. . . . . . . . . . . . . . 15 ⊢ ((𝐹‘𝑅) ∈ (0[,)+∞) → (𝐹‘𝑅) ∈ ℂ)
119	117, 118	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝐹‘𝑅) ∈ ℂ)
120	34	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑍 ∈ (𝔼‘𝑁))
121	120, 37	sylan 592	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑍‘𝑖) ∈ ℂ)
122	39	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → 𝑈 ∈ (𝔼‘𝑁))
123	122, 42	sylan 592	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (𝑈‘𝑖) ∈ ℂ)
124		simp2r 1219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ∈ ℂ)
125		simp2l 1218	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) ∈ ℂ)
126	124, 125	subcld 11708	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ)
127		simp1l 1216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ∈ ℂ)
128	44, 127, 46	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑃)) ∈ ℂ)
129	126, 128	mulcld 11368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) ∈ ℂ)
130	125, 127	subcld 11708	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ)
131		subcl 11595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (1 − (𝐹‘𝑅)) ∈ ℂ)
132	44, 124, 131	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑅)) ∈ ℂ)
133	130, 132	mulcld 11368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) ∈ ℂ)
134	124, 127	subcld 11708	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ)
135		simp1r 1217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑃) ≠ (𝐹‘𝑅))
136	135	necomd 3014	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑅) ≠ (𝐹‘𝑃))
137	124, 127, 136	subne0d 11718	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) − (𝐹‘𝑃)) ≠ 0)
138	129, 133, 134, 137	divdird 12171	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
139	134	mulridd 11365	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑃)))
140	134, 125	mulcomd 11369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃))))
141	125, 124, 127	subdid 11811	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
142	140, 141	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
143	139, 142	oveq12d 7469	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
144		subdi 11788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
145	44, 144	mp3an2 1479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
146	134, 125, 145	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄))))
147		subdi 11788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
148	44, 147	mp3an2 1479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑅) − (𝐹‘𝑄)) ∈ ℂ ∧ (𝐹‘𝑃) ∈ ℂ) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
149	126, 127, 148	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))))
150	126	mulridd 11365	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) = ((𝐹‘𝑅) − (𝐹‘𝑄)))
151	124, 125, 127	subdird 11812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
152	124, 127	mulcomd 11369	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝐹‘𝑃)) = ((𝐹‘𝑃) · (𝐹‘𝑅)))
153	152	oveq1d 7466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) · (𝐹‘𝑃)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
154	151, 153	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) = (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
155	150, 154	oveq12d 7469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · 1) − (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
156	149, 155	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
157		subdi 11788	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ 1 ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
158	44, 157	mp3an2 1479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑄) − (𝐹‘𝑃)) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
159	130, 124, 158	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
160	130	mulridd 11365	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) = ((𝐹‘𝑄) − (𝐹‘𝑃)))
161	125, 127, 124	subdird 11812	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))
162	160, 161	oveq12d 7469	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · 1) − (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
163	159, 162	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) = (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
164	156, 163	oveq12d 7469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))))
165	127, 124	mulcld 11368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝐹‘𝑅)) ∈ ℂ)
166	125, 127	mulcld 11368	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑃)) ∈ ℂ)
167	165, 166	subcld 11708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) ∈ ℂ)
168		mulcl 11323	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ)
169	168	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝐹‘𝑅)) ∈ ℂ)
170	169, 165	subcld 11708	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))) ∈ ℂ)
171	126, 130, 167, 170	addsub4d 11755	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) − (((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))))
172	124, 125, 127	npncand 11732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑃)))
173	165, 166, 169	npncan3d 11744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))) = (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))))
174	172, 173	oveq12d 7469	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) + ((𝐹‘𝑄) − (𝐹‘𝑃))) − ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅))))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
175	164, 171, 174	3eqtr2d 2804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) = (((𝐹‘𝑅) − (𝐹‘𝑃)) − (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃)))))
176	143, 146, 175	3eqtr4d 2808	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))))
177	129, 133	addcld 11367	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) ∈ ℂ)
178		subcl 11595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ (𝐹‘𝑄) ∈ ℂ) → (1 − (𝐹‘𝑄)) ∈ ℂ)
179	44, 125, 178	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) ∈ ℂ)
180	177, 134, 179, 137	divmuld 12155	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄)) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑄))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))))))
181	176, 180	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅)))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (𝐹‘𝑄)))
182	126, 128, 134, 137	div23d 12170	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃))))
183	134, 130, 134, 137	divsubdird 12172	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
184	124, 125, 127	nnncan2d 11743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) = ((𝐹‘𝑅) − (𝐹‘𝑄)))
185	184	oveq1d 7466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) − ((𝐹‘𝑄) − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))))
186	134, 137	dividd 12131	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = 1)
187	186	oveq1d 7466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
188	183, 185, 187	3eqtr3d 2806	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
189	188	oveq1d 7466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))))
190	182, 189	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))))
191	130, 132, 134, 137	div23d 12170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))))
192	190, 191	oveq12d 7469	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (1 − (𝐹‘𝑃))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (1 − (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))))
193	138, 181, 192	3eqtr3d 2806	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (𝐹‘𝑄)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))))
194	193	oveq1d 7466	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)))
195	126, 127	mulcld 11368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) ∈ ℂ)
196	130, 124	mulcld 11368	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) ∈ ℂ)
197	195, 196, 134, 137	divdird 12171	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
198	154, 161	oveq12d 7469	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) = ((((𝐹‘𝑃) · (𝐹‘𝑅)) − ((𝐹‘𝑄) · (𝐹‘𝑃))) + (((𝐹‘𝑄) · (𝐹‘𝑅)) − ((𝐹‘𝑃) · (𝐹‘𝑅)))))
199	173, 198, 142	3eqtr4rd 2809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))))
200	195, 196	addcld 11367	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) ∈ ℂ)
201	200, 134, 125, 137	divmuld 12155	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄) ↔ (((𝐹‘𝑅) − (𝐹‘𝑃)) · (𝐹‘𝑄)) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)))))
202	199, 201	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) + (((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅))) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = (𝐹‘𝑄))
203	126, 127, 134, 137	div23d 12170	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃)))
204	188	oveq1d 7466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑃)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)))
205	203, 204	eqtrd 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)))
206	130, 124, 134, 137	div23d 12170	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)))
207	205, 206	oveq12d 7469	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑅) − (𝐹‘𝑄)) · (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) · (𝐹‘𝑅)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))))
208	197, 202, 207	3eqtr3d 2806	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝐹‘𝑄) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))))
209	208	oveq1d 7466	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑄) · (𝑈‘𝑖)) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)))
210	194, 209	oveq12d 7469	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))))
211	130, 134, 137	divcld 12133	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ)
212		subcl 11595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((1 ∈ ℂ ∧ (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ ℂ) → (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ)
213	44, 211, 212	sylancr 599	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) ∈ ℂ)
214		simp3l 1220	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑍‘𝑖) ∈ ℂ)
215	128, 214	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) ∈ ℂ)
216	213, 215	mulcld 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) ∈ ℂ)
217	132, 214	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) ∈ ℂ)
218	211, 217	mulcld 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) ∈ ℂ)
219		simp3r 1221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (𝑈‘𝑖) ∈ ℂ)
220	127, 219	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑃) · (𝑈‘𝑖)) ∈ ℂ)
221	213, 220	mulcld 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) ∈ ℂ)
222	124, 219	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((𝐹‘𝑅) · (𝑈‘𝑖)) ∈ ℂ)
223	211, 222	mulcld 11368	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))) ∈ ℂ)
224	216, 218, 221, 223	add4d 11578	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
225	213, 128	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) ∈ ℂ)
226	211, 132	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) ∈ ℂ)
227	213, 128, 214	mulassd 11371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))))
228	211, 132, 214	mulassd 11371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))))
229	227, 228	oveq12d 7469	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) · (𝑍‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅))) · (𝑍‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))))
230	225, 214, 226, 229	joinlmuladdmuld 11375	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))))
231	213, 127	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) ∈ ℂ)
232	211, 124	mulcld 11368	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) ∈ ℂ)
233	213, 127, 219	mulassd 11371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))))
234	211, 124, 219	mulassd 11371	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖)) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))
235	233, 234	oveq12d 7469	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) · (𝑈‘𝑖)) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅)) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
236	231, 219, 232, 235	joinlmuladdmuld 11375	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖)) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
237	230, 236	oveq12d 7469	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)))) + (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
238	213, 215, 220	adddid 11372	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))))
239	211, 217, 222	adddid 11372	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖)))))
240	238, 239	oveq12d 7469	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((1 − (𝐹‘𝑃)) · (𝑍‘𝑖))) + ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((1 − (𝐹‘𝑅)) · (𝑍‘𝑖))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · ((𝐹‘𝑅) · (𝑈‘𝑖))))))
241	224, 237, 240	3eqtr4rd 2809	. . . . . . . . . . . . . . 15 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (1 − (𝐹‘𝑃))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (1 − (𝐹‘𝑅)))) · (𝑍‘𝑖)) + ((((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (𝐹‘𝑃)) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (𝐹‘𝑅))) · (𝑈‘𝑖))))
242	210, 241	eqtr4d 2801	. . . . . . . . . . . . . 14 ⊢ ((((𝐹‘𝑃) ∈ ℂ ∧ (𝐹‘𝑃) ≠ (𝐹‘𝑅)) ∧ ((𝐹‘𝑄) ∈ ℂ ∧ (𝐹‘𝑅) ∈ ℂ) ∧ ((𝑍‘𝑖) ∈ ℂ ∧ (𝑈‘𝑖) ∈ ℂ)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
243	112, 113, 116, 119, 121, 123, 242	syl222anc 1414	. . . . . . . . . . . . 13 ⊢ ((((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) ∧ 𝑖 ∈ (1...𝑁)) → (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
244	243	ralrimiva 3158	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
245		oveq2 7459	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (1 − 𝑡) = (1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))))
246	245	oveq1d 7466	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) = ((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
247		oveq1 7458	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) = ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
248	246, 247	oveq12d 7469	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
249	248	eqeq2d 2774	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → ((((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
250	249	ralbidv 3189	. . . . . . . . . . . . 13 ⊢ (𝑡 = (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) → (∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) ↔ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
251	250	rspcev 3580	. . . . . . . . . . . 12 ⊢ (((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) ∈ (0[,]1) ∧ ∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − (((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃)))) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + ((((𝐹‘𝑄) − (𝐹‘𝑃)) / ((𝐹‘𝑅) − (𝐹‘𝑃))) · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
252	109, 244, 251	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑃) ≠ (𝐹‘𝑅) ∧ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
253	252	ex 418	. . . . . . . . . 10 ⊢ ((𝐹‘𝑃) ≠ (𝐹‘𝑅) → (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
254	84, 253	pm2.61ine 3042	. . . . . . . . 9 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
255		r19.26-3 3127	. . . . . . . . . 10 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) ↔ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
256		simp2 1155	. . . . . . . . . . . . . . 15 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))))
257		oveq2 7459	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) → ((1 − 𝑡) · (𝑃‘𝑖)) = ((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))))
258		oveq2 7459	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))) → (𝑡 · (𝑅‘𝑖)) = (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))
259	257, 258	oveqan12d 7470	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
260	259	3adant2 1149	. . . . . . . . . . . . . . 15 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))))
261	256, 260	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
262	261	ralimi 3103	. . . . . . . . . . . . 13 ⊢ (∀𝑖 ∈ (1...𝑁)((𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ (𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ (𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∀𝑖 ∈ (1...𝑁)((𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖))) ↔ (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) = (((1 − 𝑡) · (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖)))) + (𝑡 · (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))))))
263		ralbi 3121	. . . . . . . . . . . . 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 3190	. . . . . . . . . . 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 665	. . . . . . 7 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) ∧ ((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞))) → ((∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖)))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
270	269	expimpd 459	. . . . . 6 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → ((((𝐹‘𝑃) ∈ (0[,)+∞) ∧ (𝐹‘𝑄) ∈ (0[,)+∞) ∧ (𝐹‘𝑅) ∈ (0[,)+∞)) ∧ (∀𝑖 ∈ (1...𝑁)(𝑃‘𝑖) = (((1 − (𝐹‘𝑃)) · (𝑍‘𝑖)) + ((𝐹‘𝑃) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − (𝐹‘𝑄)) · (𝑍‘𝑖)) + ((𝐹‘𝑄) · (𝑈‘𝑖))) ∧ ∀𝑖 ∈ (1...𝑁)(𝑅‘𝑖) = (((1 − (𝐹‘𝑅)) · (𝑍‘𝑖)) + ((𝐹‘𝑅) · (𝑈‘𝑖))))) → ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
271	270	adantlr 728	. . . . 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 1210	. . . . 5 ⊢ (((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) → 𝑁 ∈ ℕ)
275	1	ssrab3 4010	. . . . . . . 8 ⊢ 𝐷 ⊆ (𝔼‘𝑁)
276	275	sseli 3909	. . . . . . 7 ⊢ (𝑄 ∈ 𝐷 → 𝑄 ∈ (𝔼‘𝑁))
277	275	sseli 3909	. . . . . . 7 ⊢ (𝑃 ∈ 𝐷 → 𝑃 ∈ (𝔼‘𝑁))
278	275	sseli 3909	. . . . . . 7 ⊢ (𝑅 ∈ 𝐷 → 𝑅 ∈ (𝔼‘𝑁))
279	276, 277, 278	3anim123i 1169	. . . . . 6 ⊢ ((𝑄 ∈ 𝐷 ∧ 𝑃 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
280	279	3com12 1141	. . . . 5 ⊢ ((𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷) → (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)))
281		brbtwn 29534	. . . . . 6 ⊢ ((𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
282	281	adantl 487	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑄 ∈ (𝔼‘𝑁) ∧ 𝑃 ∈ (𝔼‘𝑁) ∧ 𝑅 ∈ (𝔼‘𝑁))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
283	274, 280, 282	syl2an 608	. . . 4 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
284	283	adantr 486	. . 3 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → (𝑄 Btwn ⟨𝑃, 𝑅⟩ ↔ ∃𝑡 ∈ (0[,]1)∀𝑖 ∈ (1...𝑁)(𝑄‘𝑖) = (((1 − 𝑡) · (𝑃‘𝑖)) + (𝑡 · (𝑅‘𝑖)))))
285	273, 284	mpbird 260	. 2 ⊢ (((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) ∧ ((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅))) → 𝑄 Btwn ⟨𝑃, 𝑅⟩)
286	285	ex 418	1 ⊢ ((((𝑁 ∈ ℕ ∧ 𝑍 ∈ (𝔼‘𝑁) ∧ 𝑈 ∈ (𝔼‘𝑁)) ∧ 𝑍 ≠ 𝑈) ∧ (𝑃 ∈ 𝐷 ∧ 𝑄 ∈ 𝐷 ∧ 𝑅 ∈ 𝐷)) → (((𝐹‘𝑃) ≤ (𝐹‘𝑄) ∧ (𝐹‘𝑄) ≤ (𝐹‘𝑅)) → 𝑄 Btwn ⟨𝑃, 𝑅⟩))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 ⟨cop 4840 class class class wbr 5108 {copab 5173 ‘cfv 6566 (class class class)co 7451 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 +∞cpnf 11379 < clt 11382 ≤ cle 11383 − cmin 11580 / cdiv 12013 ℕcn 12375 [,)cico 13518 [,]cicc 13519 ...cfz 13679 𝔼cee 29522 Btwn cbtwn 29523

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-er 8755 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-z 12734 df-uz 13006 df-ico 13522 df-icc 13523 df-fz 13680 df-ee 29525 df-btwn 29526

This theorem is used by: axcontlem10 29608

W3C validator