Theorem constrfin 33736

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 6920	. . . 4 ⊢ (𝑚 = ∅ → (𝐶‘𝑚) = (𝐶‘∅))
3	2	eleq1d 2829	. . 3 ⊢ (𝑚 = ∅ → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘∅) ∈ Fin))
4		fveq2 6920	. . . 4 ⊢ (𝑚 = 𝑛 → (𝐶‘𝑚) = (𝐶‘𝑛))
5	4	eleq1d 2829	. . 3 ⊢ (𝑚 = 𝑛 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘𝑛) ∈ Fin))
6		fveq2 6920	. . . 4 ⊢ (𝑚 = suc 𝑛 → (𝐶‘𝑚) = (𝐶‘suc 𝑛))
7	6	eleq1d 2829	. . 3 ⊢ (𝑚 = suc 𝑛 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘suc 𝑛) ∈ Fin))
8		fveq2 6920	. . . 4 ⊢ (𝑚 = 𝑁 → (𝐶‘𝑚) = (𝐶‘𝑁))
9	8	eleq1d 2829	. . 3 ⊢ (𝑚 = 𝑁 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘𝑁) ∈ Fin))
10		constr0.1	. . . . 5 ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
11	10	constr0 33727	. . . 4 ⊢ (𝐶‘∅) = {0, 1}
12		prfi 9391	. . . 4 ⊢ {0, 1} ∈ Fin
13	11, 12	eqeltri 2840	. . 3 ⊢ (𝐶‘∅) ∈ Fin
14		nfv 1913	. . . . . . 7 ⊢ Ⅎ𝑥(𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin)
15		nfcv 2908	. . . . . . 7 ⊢ Ⅎ𝑥(𝐶‘suc 𝑛)
16		nfrab1 3464	. . . . . . 7 ⊢ Ⅎ𝑥{𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
17		nnon 7909	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
18	17	adantr 480	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → 𝑛 ∈ On)
19		eqid 2740	. . . . . . . . 9 ⊢ (𝐶‘𝑛) = (𝐶‘𝑛)
20	10, 18, 19	constrsuc 33728	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝑥 ∈ (𝐶‘suc 𝑛) ↔ (𝑥 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))))
21		rabid 3465	. . . . . . . 8 ⊢ (𝑥 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))} ↔ (𝑥 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
22	20, 21	bitr4di 289	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝑥 ∈ (𝐶‘suc 𝑛) ↔ 𝑥 ∈ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}))
23	14, 15, 16, 22	eqrd 4028	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
24		3unrab 32531	. . . . . 6 ⊢ (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}) = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
25	23, 24	eqtr4di 2798	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) = (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}))
26		simpr 484	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘𝑛) ∈ Fin)
27	26	adantr 480	. . . . . . . . 9 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
28	27	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
29	28	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
30		snfi 9109	. . . . . . . . . . . . 13 ⊢ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ∈ Fin
31	30	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ∈ Fin)
32	10, 17	constrsscn 33730	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) ⊆ ℂ)
33	32	ad9antr 741	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝐶‘𝑛) ⊆ ℂ)
34		simp-8r 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ (𝐶‘𝑛))
35		simp-7r 789	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ (𝐶‘𝑛))
36		simp-6r 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ (𝐶‘𝑛))
37		simp-5r 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ (𝐶‘𝑛))
38		simpllr 775	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑡 ∈ ℝ)
39		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑟 ∈ ℝ)
40		simpr1 1194	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
41		simpr2 1195	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))))
42		simpr3 1196	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
43		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))
44	33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43	constrrtll 33722	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
45	44	r19.29an 3164	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
46	45	r19.29an 3164	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
47	46	ex 412	. . . . . . . . . . . . . 14 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
48	47	ralrimiva 3152	. . . . . . . . . . . . 13 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
49		rabsssn 4690	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ⊆ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ↔ ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
50	48, 49	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ⊆ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))})
51	31, 50	ssfid 9329	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
52	29, 51	rabrexfi 32534	. . . . . . . . . 10 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
53	28, 52	rabrexfi 32534	. . . . . . . . 9 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
54	27, 53	rabrexfi 32534	. . . . . . . 8 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
55	26, 54	rabrexfi 32534	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
56	29	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
57		snfi 9109	. . . . . . . . . . . . . . 15 ⊢ {𝑎} ∈ Fin
58	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑎} ∈ Fin)
59	32	ad10antr 743	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
60		simp-9r 793	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
61		simp-8r 791	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
62		simp-7r 789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
63		simp-6r 787	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
64		simp-5r 785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
65		simplr 768	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑡 ∈ ℝ)
66		simprl 770	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
67		simprr 772	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
68		simp-4r 783	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 = 𝑏)
69	59, 60, 61, 62, 63, 64, 65, 66, 67, 68	constrrtlc2 33724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = 𝑎)
70	69	r19.29an 3164	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = 𝑎)
71	70	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
72	71	ralrimiva 3152	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
73		rabsssn 4690	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {𝑎} ↔ ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
74	72, 73	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {𝑎})
75	58, 74	ssfid 9329	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
76		prfi 9391	. . . . . . . . . . . . . . 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 775	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 ∈ ℂ)
79		1cnd 11285	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 1 ∈ ℂ)
80		ax-1ne0 11253	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≠ 0
81	80	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 1 ≠ 0)
82	32	ad10antr 743	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
83		simp-9r 793	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
84	82, 83	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ)
85	84	cjcld 15245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ ℂ)
86		simp-8r 791	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
87	82, 86	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ)
88	87	cjcld 15245	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑏) ∈ ℂ)
89	88, 85	subcld 11647	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑏) − (∗‘𝑎)) ∈ ℂ)
90	87, 84	subcld 11647	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑎) ∈ ℂ)
91		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑏)
92	91	necomd 3002	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ≠ 𝑎)
93	87, 84, 92	subne0d 11656	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑎) ≠ 0)
94	89, 90, 93	divcld 12070	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ∈ ℂ)
95	84, 94	mulcld 11310	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
96	85, 95	subcld 11647	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ ℂ)
97		simp-7r 789	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
98	82, 97	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ)
99	98	cjcld 15245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑐) ∈ ℂ)
100	96, 99	subcld 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) ∈ ℂ)
101	98, 94	mulcld 11310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
102	100, 101	subcld 11647	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ ℂ)
103		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
104		simp-5r 785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
105		simplr 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑡 ∈ ℝ)
106		simprl 770	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
107		simprr 772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
108		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) = (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))
109		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))
110		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))
111	82, 83, 86, 97, 103, 104, 105, 106, 107, 108, 109, 110, 91	constrrtlc1 33723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0 ∧ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0))
112	111	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0)
113	102, 94, 112	divcld 12070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
114	98, 100	mulcld 11310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) ∈ ℂ)
115	82, 103	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ)
116	82, 104	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ)
117	115, 116	subcld 11647	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ ℂ)
118	115	cjcld 15245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑒) ∈ ℂ)
119	116	cjcld 15245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑓) ∈ ℂ)
120	118, 119	subcld 11647	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑒) − (∗‘𝑓)) ∈ ℂ)
121	117, 120	mulcld 11310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓))) ∈ ℂ)
122	114, 121	addcld 11309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ ℂ)
123	122	negcld 11634	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → -((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ ℂ)
124	123, 94, 112	divcld 12070	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
125	78	sqcld 14194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥↑2) ∈ ℂ)
126	125	mullidd 11308	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (1 · (𝑥↑2)) = (𝑥↑2))
127	126	oveq1d 7463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = ((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))))
128	111	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0)
129	127, 128	eqtrd 2780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0)
130	78, 79, 81, 113, 124, 129	quad3d 32757	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))))
131	130	r19.29an 3164	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))))
132	131	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)))))
133	132	ralrimiva 3152	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)))))
134		rabsspr 32529	. . . . . . . . . . . . . . 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 234	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)), ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))})
136	77, 135	ssfid 9329	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
137		exmidne 2956	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏)
138	137	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏))
139	75, 136, 138	mpjaodan 959	. . . . . . . . . . . 12 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
140	56, 139	rabrexfi 32534	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
141	29, 140	rabrexfi 32534	. . . . . . . . . 10 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
142	28, 141	rabrexfi 32534	. . . . . . . . 9 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
143	27, 142	rabrexfi 32534	. . . . . . . 8 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
144	26, 143	rabrexfi 32534	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
145	55, 144	unfid 9239	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → ({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∈ Fin)
146	29	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
147	146	adantr 480	. . . . . . . . . . . 12 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
148		prfi 9391	. . . . . . . . . . . . . 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 768	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 ∈ ℂ)
151		1cnd 11285	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 1 ∈ ℂ)
152	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 1 ≠ 0)
153	32	ad9antr 741	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
154		simp-4r 783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
155	153, 154	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ)
156		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
157	153, 156	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ)
158	155, 157	subcld 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ ℂ)
159	158	cjcld 15245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑒 − 𝑓)) ∈ ℂ)
160	158, 159	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) ∈ ℂ)
161		simp-5r 785	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ (𝐶‘𝑛))
162	153, 161	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ ℂ)
163	162	cjcld 15245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑑) ∈ ℂ)
164		simp-8r 791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
165	153, 164	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ)
166	162, 165	addcld 11309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 + 𝑎) ∈ ℂ)
167	163, 166	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 + 𝑎)) ∈ ℂ)
168	160, 167	subcld 11647	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) ∈ ℂ)
169		simp-7r 789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
170	153, 169	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ)
171		simp-6r 787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
172	153, 171	sseldd 4009	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ)
173	170, 172	subcld 11647	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑐) ∈ ℂ)
174	173	cjcld 15245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑏 − 𝑐)) ∈ ℂ)
175	173, 174	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) ∈ ℂ)
176	165	cjcld 15245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ ℂ)
177	176, 166	mulcld 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 + 𝑎)) ∈ ℂ)
178	175, 177	subcld 11647	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎))) ∈ ℂ)
179	168, 178	subcld 11647	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) ∈ ℂ)
180	163, 176	subcld 11647	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ∈ ℂ)
181	162, 165	cjsubd 32755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) = ((∗‘𝑑) − (∗‘𝑎)))
182	162, 165	subcld 11647	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ∈ ℂ)
183		simpr1 1194	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑑)
184	183	necomd 3002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ≠ 𝑎)
185	162, 165, 184	subne0d 11656	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ≠ 0)
186	182, 185	cjne0d 15252	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) ≠ 0)
187	181, 186	eqnetrrd 3015	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ≠ 0)
188	179, 180, 187	divcld 12070	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
189	162, 165	mulcld 11310	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 · 𝑎) ∈ ℂ)
190	176, 189	mulcld 11310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 · 𝑎)) ∈ ℂ)
191	175, 162	mulcld 11310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑) ∈ ℂ)
192	190, 191	subcld 11647	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) ∈ ℂ)
193	163, 189	mulcld 11310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 · 𝑎)) ∈ ℂ)
194	160, 165	mulcld 11310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎) ∈ ℂ)
195	193, 194	subcld 11647	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎)) ∈ ℂ)
196	192, 195	subcld 11647	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) ∈ ℂ)
197	196, 180, 187	divcld 12070	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
198	197	negcld 11634	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
199	150	sqcld 14194	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑥↑2) ∈ ℂ)
200	199	mullidd 11308	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (1 · (𝑥↑2)) = (𝑥↑2))
201	200	oveq1d 7463	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = ((𝑥↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))))
202		simpr2 1195	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)))
203		simpr3 1196	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
204		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) = ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐)))
205		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) = ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓)))
206		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) = (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))
207		eqid 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) = -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))
208	153, 164, 169, 171, 161, 154, 156, 150, 183, 202, 203, 204, 205, 206, 207	constrrtcc 33726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑥↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0)
209	201, 208	eqtrd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0)
210	150, 151, 152, 188, 198, 209	quad3d 32757	. . . . . . . . . . . . . . . 16 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1))))
211	210	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) → ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)))))
212	211	ralrimiva 3152	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → ∀𝑥 ∈ ℂ ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)))))
213		rabsspr 32529	. . . . . . . . . . . . . 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 234	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ⊆ {((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)), ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1))})
215	149, 214	ssfid 9329	. . . . . . . . . . . 12 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
216	147, 215	rabrexfi 32534	. . . . . . . . . . 11 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
217	146, 216	rabrexfi 32534	. . . . . . . . . 10 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
218	29, 217	rabrexfi 32534	. . . . . . . . 9 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
219	28, 218	rabrexfi 32534	. . . . . . . 8 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
220	27, 219	rabrexfi 32534	. . . . . . 7 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
221	26, 220	rabrexfi 32534	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
222	145, 221	unfid 9239	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}) ∈ Fin)
223	25, 222	eqeltrd 2844	. . . 4 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) ∈ Fin)
224	223	ex 412	. . 3 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ∈ Fin → (𝐶‘suc 𝑛) ∈ Fin))
225	3, 5, 7, 9, 13, 224	finds 7936	. 2 ⊢ (𝑁 ∈ ω → (𝐶‘𝑁) ∈ Fin)
226	1, 225	syl 17	1 ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 846   ∨ w3o 1086   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  {crab 3443  Vcvv 3488   ∪ cun 3974   ⊆ wss 3976  ∅c0 4352  {csn 4648  {cpr 4650   ↦ cmpt 5249  Oncon0 6395  suc csuc 6397  ‘cfv 6573  (class class class)co 7448  ωcom 7903  reccrdg 8465  Fincfn 9003  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185   + caddc 11187   · cmul 11189   − cmin 11520  -cneg 11521   / cdiv 11947  2c2 12348  4c4 12350  ↑cexp 14112  ∗ccj 15145  ℑcim 15147  √csqrt 15282  abscabs 15283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-mulcom 11248  ax-addass 11249  ax-mulass 11250  ax-distr 11251  ax-i2m1 11252  ax-1ne0 11253  ax-1rid 11254  ax-rnegex 11255  ax-rrecex 11256  ax-cnre 11257  ax-pre-lttri 11258  ax-pre-lttrn 11259  ax-pre-ltadd 11260  ax-pre-mulgt0 11261  ax-pre-sup 11262

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-1o 8522  df-2o 8523  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-fin 9007  df-sup 9511  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330  df-sub 11522  df-neg 11523  df-div 11948  df-nn 12294  df-2 12356  df-3 12357  df-4 12358  df-n0 12554  df-z 12640  df-uz 12904  df-rp 13058  df-seq 14053  df-exp 14113  df-cj 15148  df-re 15149  df-im 15150  df-sqrt 15284  df-abs 15285

This theorem is referenced by: (None)