Theorem constrfin 34311

Description: Each step of the construction of constructible numbers is finite. (Contributed by Thierry Arnoux, 6-Jul-2025.)

Hypotheses

Ref	Expression
constr0.1	⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
constrfin.1	⊢ (𝜑 → 𝑁 ∈ ω)

Assertion

Ref	Expression
constrfin	⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin)

Distinct variable groups:   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑠,𝑡,𝑥   𝐶,𝑟,𝑎,𝑏,𝑐,𝑑,𝑠,𝑡,𝑥

Allowed substitution hints:   𝜑(𝑥, 𝑡, 𝑒, 𝑓, 𝑠, 𝑟, 𝑎, 𝑏, 𝑐, 𝑑)   𝑁(𝑥, 𝑡, 𝑒, 𝑓, 𝑠, 𝑟, 𝑎, 𝑏, 𝑐, 𝑑)

Proof of Theorem constrfin

Dummy variables 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		constrfin.1	. 2 ⊢ (𝜑 → 𝑁 ∈ ω)
2		fveq2 6873	. . . 4 ⊢ (𝑚 = ∅ → (𝐶‘𝑚) = (𝐶‘∅))
3	2	eleq1d 2845	. . 3 ⊢ (𝑚 = ∅ → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘∅) ∈ Fin))
4		fveq2 6873	. . . 4 ⊢ (𝑚 = 𝑛 → (𝐶‘𝑚) = (𝐶‘𝑛))
5	4	eleq1d 2845	. . 3 ⊢ (𝑚 = 𝑛 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘𝑛) ∈ Fin))
6		fveq2 6873	. . . 4 ⊢ (𝑚 = suc 𝑛 → (𝐶‘𝑚) = (𝐶‘suc 𝑛))
7	6	eleq1d 2845	. . 3 ⊢ (𝑚 = suc 𝑛 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘suc 𝑛) ∈ Fin))
8		fveq2 6873	. . . 4 ⊢ (𝑚 = 𝑁 → (𝐶‘𝑚) = (𝐶‘𝑁))
9	8	eleq1d 2845	. . 3 ⊢ (𝑚 = 𝑁 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘𝑁) ∈ Fin))
10		constr0.1	. . . . 5 ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
11	10	constr0 34302	. . . 4 ⊢ (𝐶‘∅) = {0, 1}
12		prfi 9293	. . . 4 ⊢ {0, 1} ∈ Fin
13	11, 12	eqeltri 2856	. . 3 ⊢ (𝐶‘∅) ∈ Fin
14		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑥(𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin)
15		nfcv 2922	. . . . . . 7 ⊢ Ⅎ𝑥(𝐶‘suc 𝑛)
16		nfrab1 3431	. . . . . . 7 ⊢ Ⅎ𝑥{𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
17		nnon 7866	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
18	17	adantr 486	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → 𝑛 ∈ On)
19		eqid 2760	. . . . . . . . 9 ⊢ (𝐶‘𝑛) = (𝐶‘𝑛)
20	10, 18, 19	constrsuc 34303	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝑥 ∈ (𝐶‘suc 𝑛) ↔ (𝑥 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))))
21		rabid 3432	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))} ↔ (𝑥 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
22	20, 21	bitr4di 292	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝑥 ∈ (𝐶‘suc 𝑛) ↔ 𝑥 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}))
23	14, 15, 16, 22	eqrd 3949	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
24		3unrab 33032	. . . . . 6 ⊢ (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}) = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
25	23, 24	eqtr4di 2813	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) = (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}))
26		simpr 490	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘𝑛) ∈ Fin)
27	26	adantr 486	. . . . . . . . 9 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
28	27	adantr 486	. . . . . . . . . 10 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
29	28	adantr 486	. . . . . . . . . . 11 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
30		snfi 9049	. . . . . . . . . . . . 13 ⊢ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ∈ Fin
31	30	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ∈ Fin)
32	10, 17	constrsscn 34305	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) ⊆ ℂ)
33	32	ad9antr 755	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝐶‘𝑛) ⊆ ℂ)
34		simp-8r 804	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ (𝐶‘𝑛))
35		simp-7r 802	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ (𝐶‘𝑛))
36		simp-6r 800	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ (𝐶‘𝑛))
37		simp-5r 798	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ (𝐶‘𝑛))
38		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑡 ∈ ℝ)
39		simplr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑟 ∈ ℝ)
40		simpr1 1213	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
41		simpr2 1214	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))))
42		simpr3 1215	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
43		eqid 2760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))
44	33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43	constrrtll 34296	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
45	44	r19.29an 3166	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
46	45	r19.29an 3166	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
47	46	ex 418	. . . . . . . . . . . . . 14 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
48	47	ralrimiva 3154	. . . . . . . . . . . . 13 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
49		rabsssn 4628	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ⊆ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ↔ ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
50	48, 49	sylibr 237	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ⊆ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))})
51	31, 50	ssfid 9238	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
52	29, 51	rabrexfi 33035	. . . . . . . . . 10 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
53	28, 52	rabrexfi 33035	. . . . . . . . 9 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
54	27, 53	rabrexfi 33035	. . . . . . . 8 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
55	26, 54	rabrexfi 33035	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
56	29	adantr 486	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
57		snfi 9049	. . . . . . . . . . . . . . 15 ⊢ {𝑎} ∈ Fin
58	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑎} ∈ Fin)
59	32	ad10antr 757	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
60		simp-9r 806	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
61		simp-8r 804	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
62		simp-7r 802	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
63		simp-6r 800	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
64		simp-5r 798	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
65		simplr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑡 ∈ ℝ)
66		simprl 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
67		simprr 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
68		simp-4r 796	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 = 𝑏)
69	59, 60, 61, 62, 63, 64, 65, 66, 67, 68	constrrtlc2 34298	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = 𝑎)
70	69	r19.29an 3166	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = 𝑎)
71	70	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
72	71	ralrimiva 3154	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
73		rabsssn 4628	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {𝑎} ↔ ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
74	72, 73	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {𝑎})
75	58, 74	ssfid 9238	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
76		prfi 9293	. . . . . . . . . . . . . . 15 ⊢ {((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)), ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))} ∈ Fin
77	76	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → {((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)), ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))} ∈ Fin)
78		simpllr 788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 ∈ ℂ)
79		1cnd 11273	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 1 ∈ ℂ)
80		ax-1ne0 11240	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≠ 0
81	80	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 1 ≠ 0)
82	32	ad10antr 757	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
83		simp-9r 806	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
84	82, 83	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ)
85	84	cjcld 15330	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ ℂ)
86		simp-8r 804	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
87	82, 86	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ)
88	87	cjcld 15330	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑏) ∈ ℂ)
89	88, 85	subcld 11640	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑏) − (∗‘𝑎)) ∈ ℂ)
90	87, 84	subcld 11640	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑎) ∈ ℂ)
91		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑏)
92	91	necomd 3010	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ≠ 𝑎)
93	87, 84, 92	subne0d 11650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑎) ≠ 0)
94	89, 90, 93	divcld 12062	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ∈ ℂ)
95	84, 94	mulcld 11300	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
96	85, 95	subcld 11640	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ ℂ)
97		simp-7r 802	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
98	82, 97	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ)
99	98	cjcld 15330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑐) ∈ ℂ)
100	96, 99	subcld 11640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) ∈ ℂ)
101	98, 94	mulcld 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
102	100, 101	subcld 11640	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ ℂ)
103		simp-6r 800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
104		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
105		simplr 781	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑡 ∈ ℝ)
106		simprl 783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
107		simprr 785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
108		eqid 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) = (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))
109		eqid 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))
110		eqid 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))
111	82, 83, 86, 97, 103, 104, 105, 106, 107, 108, 109, 110, 91	constrrtlc1 34297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0 ∧ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0))
112	111	simprd 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0)
113	102, 94, 112	divcld 12062	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
114	98, 100	mulcld 11300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) ∈ ℂ)
115	82, 103	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ)
116	82, 104	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ)
117	115, 116	subcld 11640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ ℂ)
118	115	cjcld 15330	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑒) ∈ ℂ)
119	116	cjcld 15330	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑓) ∈ ℂ)
120	118, 119	subcld 11640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑒) − (∗‘𝑓)) ∈ ℂ)
121	117, 120	mulcld 11300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓))) ∈ ℂ)
122	114, 121	addcld 11299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ ℂ)
123	122	negcld 11627	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → -((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ ℂ)
124	123, 94, 112	divcld 12062	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
125	78	sqcld 14255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥↑2) ∈ ℂ)
126	125	mullidd 11298	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (1 · (𝑥↑2)) = (𝑥↑2))
127	126	oveq1d 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = ((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))))
128	111	simpld 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0)
129	127, 128	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0)
130	78, 79, 81, 113, 124, 129	quad3d 33274	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))))
131	130	r19.29an 3166	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))))
132	131	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)))))
133	132	ralrimiva 3154	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)))))
134		rabsspr 33030	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)), ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))} ↔ ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)))))
135	133, 134	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)), ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))})
136	77, 135	ssfid 9238	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
137		exmidne 2965	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏)
138	137	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏))
139	75, 136, 138	mpjaodan 973	. . . . . . . . . . . 12 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
140	56, 139	rabrexfi 33035	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
141	29, 140	rabrexfi 33035	. . . . . . . . . 10 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
142	28, 141	rabrexfi 33035	. . . . . . . . 9 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
143	27, 142	rabrexfi 33035	. . . . . . . 8 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
144	26, 143	rabrexfi 33035	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
145	55, 144	unfid 9165	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → ({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∈ Fin)
146	29	adantr 486	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
147	146	adantr 486	. . . . . . . . . . . 12 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
148		prfi 9293	. . . . . . . . . . . . . 14 ⊢ {((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)), ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1))} ∈ Fin
149	148	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)), ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1))} ∈ Fin)
150		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 ∈ ℂ)
151		1cnd 11273	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 1 ∈ ℂ)
152	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 1 ≠ 0)
153	32	ad9antr 755	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
154		simp-4r 796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
155	153, 154	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ)
156		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
157	153, 156	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ)
158	155, 157	subcld 11640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ ℂ)
159	158	cjcld 15330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑒 − 𝑓)) ∈ ℂ)
160	158, 159	mulcld 11300	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) ∈ ℂ)
161		simp-5r 798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ (𝐶‘𝑛))
162	153, 161	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ ℂ)
163	162	cjcld 15330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑑) ∈ ℂ)
164		simp-8r 804	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
165	153, 164	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ)
166	162, 165	addcld 11299	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 + 𝑎) ∈ ℂ)
167	163, 166	mulcld 11300	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 + 𝑎)) ∈ ℂ)
168	160, 167	subcld 11640	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) ∈ ℂ)
169		simp-7r 802	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
170	153, 169	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ)
171		simp-6r 800	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
172	153, 171	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ)
173	170, 172	subcld 11640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑐) ∈ ℂ)
174	173	cjcld 15330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑏 − 𝑐)) ∈ ℂ)
175	173, 174	mulcld 11300	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) ∈ ℂ)
176	165	cjcld 15330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ ℂ)
177	176, 166	mulcld 11300	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 + 𝑎)) ∈ ℂ)
178	175, 177	subcld 11640	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎))) ∈ ℂ)
179	168, 178	subcld 11640	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) ∈ ℂ)
180	163, 176	subcld 11640	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ∈ ℂ)
181	162, 165	cjsubd 33267	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) = ((∗‘𝑑) − (∗‘𝑎)))
182	162, 165	subcld 11640	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ∈ ℂ)
183		simpr1 1213	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑑)
184	183	necomd 3010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ≠ 𝑎)
185	162, 165, 184	subne0d 11650	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ≠ 0)
186	182, 185	cjne0d 15337	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) ≠ 0)
187	181, 186	eqnetrrd 3023	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ≠ 0)
188	179, 180, 187	divcld 12062	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
189	162, 165	mulcld 11300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 · 𝑎) ∈ ℂ)
190	176, 189	mulcld 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 · 𝑎)) ∈ ℂ)
191	175, 162	mulcld 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑) ∈ ℂ)
192	190, 191	subcld 11640	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) ∈ ℂ)
193	163, 189	mulcld 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 · 𝑎)) ∈ ℂ)
194	160, 165	mulcld 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎) ∈ ℂ)
195	193, 194	subcld 11640	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎)) ∈ ℂ)
196	192, 195	subcld 11640	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) ∈ ℂ)
197	196, 180, 187	divcld 12062	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
198	197	negcld 11627	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
199	150	sqcld 14255	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑥↑2) ∈ ℂ)
200	199	mullidd 11298	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (1 · (𝑥↑2)) = (𝑥↑2))
201	200	oveq1d 7423	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = ((𝑥↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))))
202		simpr2 1214	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)))
203		simpr3 1215	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
204		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) = ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐)))
205		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) = ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓)))
206		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) = (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))
207		eqid 2760	. . . . . . . . . . . . . . . . . . 19 ⊢ -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) = -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))
208	153, 164, 169, 171, 161, 154, 156, 150, 183, 202, 203, 204, 205, 206, 207	constrrtcc 34300	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑥↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0)
209	201, 208	eqtrd 2795	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0)
210	150, 151, 152, 188, 198, 209	quad3d 33274	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1))))
211	210	ex 418	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) → ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)))))
212	211	ralrimiva 3154	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → ∀𝑥 ∈ ℂ ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)))))
213		rabsspr 33030	. . . . . . . . . . . . . 14 ⊢ ({𝑥 ∈ ℂ ∣ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ⊆ {((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)), ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1))} ↔ ∀𝑥 ∈ ℂ ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)))))
214	212, 213	sylibr 237	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ⊆ {((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)), ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1))})
215	149, 214	ssfid 9238	. . . . . . . . . . . 12 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
216	147, 215	rabrexfi 33035	. . . . . . . . . . 11 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
217	146, 216	rabrexfi 33035	. . . . . . . . . 10 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
218	29, 217	rabrexfi 33035	. . . . . . . . 9 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
219	28, 218	rabrexfi 33035	. . . . . . . 8 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
220	27, 219	rabrexfi 33035	. . . . . . 7 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
221	26, 220	rabrexfi 33035	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
222	145, 221	unfid 9165	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}) ∈ Fin)
223	25, 222	eqeltrd 2860	. . . 4 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) ∈ Fin)
224	223	ex 418	. . 3 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ∈ Fin → (𝐶‘suc 𝑛) ∈ Fin))
225	3, 5, 7, 9, 13, 224	finds 7891	. 2 ⊢ (𝑁 ∈ ω → (𝐶‘𝑁) ∈ Fin)
226	1, 225	syl 18	1 ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2955  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ∪ cun 3896   ⊆ wss 3898  ∅c0 4278  {csn 4583  {cpr 4585   ↦ cmpt 5185  Oncon0 6351  suc csuc 6353  ‘cfv 6527  (class class class)co 7408  ωcom 7860  reccrdg 8395  Fincfn 8951  ℂcc 11169  ℝcr 11170  0cc0 11171  1c1 11172   + caddc 11174   · cmul 11176   − cmin 11512  -cneg 11513   / cdiv 11942  2c2 12366  4c4 12368  ↑cexp 14172  ∗ccj 15230  ℑcim 15232  √csqrt 15367  abscabs 15368

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-cnex 11227  ax-resscn 11228  ax-1cn 11229  ax-icn 11230  ax-addcl 11231  ax-addrcl 11232  ax-mulcl 11233  ax-mulrcl 11234  ax-mulcom 11235  ax-addass 11236  ax-mulass 11237  ax-distr 11238  ax-i2m1 11239  ax-1ne0 11240  ax-1rid 11241  ax-rnegex 11242  ax-rrecex 11243  ax-cnre 11244  ax-pre-lttri 11245  ax-pre-lttrn 11246  ax-pre-ltadd 11247  ax-pre-mulgt0 11248  ax-pre-sup 11249

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7861  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8454  df-2o 8455  df-er 8695  df-en 8952  df-dom 8953  df-sdom 8954  df-fin 8955  df-sup 9412  df-pnf 11316  df-mnf 11317  df-xr 11318  df-ltxr 11319  df-le 11320  df-sub 11514  df-neg 11515  df-div 11943  df-nn 12305  df-2 12374  df-3 12375  df-4 12376  df-n0 12576  df-z 12663  df-uz 12935  df-rp 13090  df-seq 14113  df-exp 14173  df-cj 15233  df-re 15234  df-im 15235  df-sqrt 15369  df-abs 15370

This theorem is used by:  constrextdg2lem  34313