Theorem constrfin 33787

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 6906	. . . 4 ⊢ (𝑚 = ∅ → (𝐶‘𝑚) = (𝐶‘∅))
3	2	eleq1d 2826	. . 3 ⊢ (𝑚 = ∅ → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘∅) ∈ Fin))
4		fveq2 6906	. . . 4 ⊢ (𝑚 = 𝑛 → (𝐶‘𝑚) = (𝐶‘𝑛))
5	4	eleq1d 2826	. . 3 ⊢ (𝑚 = 𝑛 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘𝑛) ∈ Fin))
6		fveq2 6906	. . . 4 ⊢ (𝑚 = suc 𝑛 → (𝐶‘𝑚) = (𝐶‘suc 𝑛))
7	6	eleq1d 2826	. . 3 ⊢ (𝑚 = suc 𝑛 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘suc 𝑛) ∈ Fin))
8		fveq2 6906	. . . 4 ⊢ (𝑚 = 𝑁 → (𝐶‘𝑚) = (𝐶‘𝑁))
9	8	eleq1d 2826	. . 3 ⊢ (𝑚 = 𝑁 → ((𝐶‘𝑚) ∈ Fin ↔ (𝐶‘𝑁) ∈ Fin))
10		constr0.1	. . . . 5 ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
11	10	constr0 33778	. . . 4 ⊢ (𝐶‘∅) = {0, 1}
12		prfi 9363	. . . 4 ⊢ {0, 1} ∈ Fin
13	11, 12	eqeltri 2837	. . 3 ⊢ (𝐶‘∅) ∈ Fin
14		nfv 1914	. . . . . . 7 ⊢ Ⅎ𝑥(𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin)
15		nfcv 2905	. . . . . . 7 ⊢ Ⅎ𝑥(𝐶‘suc 𝑛)
16		nfrab1 3457	. . . . . . 7 ⊢ Ⅎ𝑥{𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
17		nnon 7893	. . . . . . . . . 10 ⊢ (𝑛 ∈ ω → 𝑛 ∈ On)
18	17	adantr 480	. . . . . . . . 9 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → 𝑛 ∈ On)
19		eqid 2737	. . . . . . . . 9 ⊢ (𝐶‘𝑛) = (𝐶‘𝑛)
20	10, 18, 19	constrsuc 33779	. . . . . . . 8 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝑥 ∈ (𝐶‘suc 𝑛) ↔ (𝑥 ∈ ℂ ∧ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))))
21		rabid 3458	. . . . . . . 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 4003	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
24		3unrab 32522	. . . . . 6 ⊢ (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}) = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
25	23, 24	eqtr4di 2795	. . . . 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 9083	. . . . . . . . . . . . 13 ⊢ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ∈ Fin
31	30	a1i 11	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ∈ Fin)
32	10, 17	constrsscn 33781	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ω → (𝐶‘𝑛) ⊆ ℂ)
33	32	ad9antr 742	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (𝐶‘𝑛) ⊆ ℂ)
34		simp-8r 792	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑎 ∈ (𝐶‘𝑛))
35		simp-7r 790	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑏 ∈ (𝐶‘𝑛))
36		simp-6r 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑐 ∈ (𝐶‘𝑛))
37		simp-5r 786	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑑 ∈ (𝐶‘𝑛))
38		simpllr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑡 ∈ ℝ)
39		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑟 ∈ ℝ)
40		simpr1 1195	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
41		simpr2 1196	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))))
42		simpr3 1197	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)
43		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))) = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))
44	33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43	constrrtll 33772	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ 𝑟 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
45	44	r19.29an 3158	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
46	45	r19.29an 3158	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎))))
47	46	ex 412	. . . . . . . . . . . . . 14 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
48	47	ralrimiva 3146	. . . . . . . . . . . . 13 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
49		rabsssn 4668	. . . . . . . . . . . . 13 ⊢ ({𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ⊆ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))} ↔ ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) → 𝑥 = (𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))))
50	48, 49	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ⊆ {(𝑎 + (((((𝑎 − 𝑐) · ((∗‘𝑑) − (∗‘𝑐))) − (((∗‘𝑎) − (∗‘𝑐)) · (𝑑 − 𝑐))) / ((((∗‘𝑏) − (∗‘𝑎)) · (𝑑 − 𝑐)) − ((𝑏 − 𝑎) · ((∗‘𝑑) − (∗‘𝑐))))) · (𝑏 − 𝑎)))})
51	31, 50	ssfid 9301	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
52	29, 51	rabrexfi 32525	. . . . . . . . . 10 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
53	28, 52	rabrexfi 32525	. . . . . . . . 9 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
54	27, 53	rabrexfi 32525	. . . . . . . 8 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
55	26, 54	rabrexfi 32525	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∈ Fin)
56	29	adantr 480	. . . . . . . . . . . 12 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
57		snfi 9083	. . . . . . . . . . . . . . 15 ⊢ {𝑎} ∈ Fin
58	57	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑎} ∈ Fin)
59	32	ad10antr 744	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
60		simp-9r 794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
61		simp-8r 792	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
62		simp-7r 790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
63		simp-6r 788	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
64		simp-5r 786	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
65		simplr 769	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑡 ∈ ℝ)
66		simprl 771	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
67		simprr 773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
68		simp-4r 784	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 = 𝑏)
69	59, 60, 61, 62, 63, 64, 65, 66, 67, 68	constrrtlc2 33774	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = 𝑎)
70	69	r19.29an 3158	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) ∧ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = 𝑎)
71	70	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) ∧ 𝑥 ∈ ℂ) → (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
72	71	ralrimiva 3146	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
73		rabsssn 4668	. . . . . . . . . . . . . . 15 ⊢ ({𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {𝑎} ↔ ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → 𝑥 = 𝑎))
74	72, 73	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ⊆ {𝑎})
75	58, 74	ssfid 9301	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 = 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
76		prfi 9363	. . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 ∈ ℂ)
79		1cnd 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 1 ∈ ℂ)
80		ax-1ne0 11224	. . . . . . . . . . . . . . . . . . . 20 ⊢ 1 ≠ 0
81	80	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 1 ≠ 0)
82	32	ad10antr 744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
83		simp-9r 794	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
84	82, 83	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ)
85	84	cjcld 15235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ ℂ)
86		simp-8r 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
87	82, 86	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ)
88	87	cjcld 15235	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑏) ∈ ℂ)
89	88, 85	subcld 11620	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑏) − (∗‘𝑎)) ∈ ℂ)
90	87, 84	subcld 11620	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑎) ∈ ℂ)
91		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑏)
92	91	necomd 2996	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ≠ 𝑎)
93	87, 84, 92	subne0d 11629	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑎) ≠ 0)
94	89, 90, 93	divcld 12043	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ∈ ℂ)
95	84, 94	mulcld 11281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
96	85, 95	subcld 11620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ ℂ)
97		simp-7r 790	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
98	82, 97	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ)
99	98	cjcld 15235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑐) ∈ ℂ)
100	96, 99	subcld 11620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) ∈ ℂ)
101	98, 94	mulcld 11281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
102	100, 101	subcld 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) ∈ ℂ)
103		simp-6r 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
104		simp-5r 786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
105		simplr 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑡 ∈ ℝ)
106		simprl 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
107		simprr 773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))
108		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) = (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))
109		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))
110		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) = (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))
111	82, 83, 86, 97, 103, 104, 105, 106, 107, 108, 109, 110, 91	constrrtlc1 33773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0 ∧ (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0))
112	111	simprd 495	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)) ≠ 0)
113	102, 94, 112	divcld 12043	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
114	98, 100	mulcld 11281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) ∈ ℂ)
115	82, 103	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ)
116	82, 104	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ)
117	115, 116	subcld 11620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ ℂ)
118	115	cjcld 15235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑒) ∈ ℂ)
119	116	cjcld 15235	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑓) ∈ ℂ)
120	118, 119	subcld 11620	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑒) − (∗‘𝑓)) ∈ ℂ)
121	117, 120	mulcld 11281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓))) ∈ ℂ)
122	114, 121	addcld 11280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ ℂ)
123	122	negcld 11607	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → -((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) ∈ ℂ)
124	123, 94, 112	divcld 12043	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) ∈ ℂ)
125	78	sqcld 14184	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥↑2) ∈ ℂ)
126	125	mullidd 11279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (1 · (𝑥↑2)) = (𝑥↑2))
127	126	oveq1d 7446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = ((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))))
128	111	simpld 494	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((𝑥↑2) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0)
129	127, 128	eqtrd 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) · 𝑥) + (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))))) = 0)
130	78, 79, 81, 113, 124, 129	quad3d 32754	. . . . . . . . . . . . . . . . . 18 ⊢ (((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑥 ∈ ℂ) ∧ 𝑡 ∈ ℝ) ∧ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1))))
131	130	r19.29an 3158	. . . . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . . . . 15 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → ∀𝑥 ∈ ℂ (∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) + (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎))) − (√‘(((((((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐)) − (𝑐 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))↑2) − (4 · (1 · (-((𝑐 · (((∗‘𝑎) − (𝑎 · (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))) − (∗‘𝑐))) + ((𝑒 − 𝑓) · ((∗‘𝑒) − (∗‘𝑓)))) / (((∗‘𝑏) − (∗‘𝑎)) / (𝑏 − 𝑎)))))))) / (2 · 1)))))
134		rabsspr 32520	. . . . . . . . . . . . . . 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 9301	. . . . . . . . . . . . 13 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑎 ≠ 𝑏) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
137		exmidne 2950	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏)
138	137	a1i 11	. . . . . . . . . . . . 13 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → (𝑎 = 𝑏 ∨ 𝑎 ≠ 𝑏))
139	75, 136, 138	mpjaodan 961	. . . . . . . . . . . 12 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
140	56, 139	rabrexfi 32525	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
141	29, 140	rabrexfi 32525	. . . . . . . . . 10 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
142	28, 141	rabrexfi 32525	. . . . . . . . 9 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
143	27, 142	rabrexfi 32525	. . . . . . . 8 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
144	26, 143	rabrexfi 32525	. . . . . . 7 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
145	55, 144	unfid 9212	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → ({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∈ Fin)
146	29	adantr 480	. . . . . . . . . . 11 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
147	146	adantr 480	. . . . . . . . . . . 12 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → (𝐶‘𝑛) ∈ Fin)
148		prfi 9363	. . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑥 ∈ ℂ)
151		1cnd 11256	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 1 ∈ ℂ)
152	80	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 1 ≠ 0)
153	32	ad9antr 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝐶‘𝑛) ⊆ ℂ)
154		simp-4r 784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ (𝐶‘𝑛))
155	153, 154	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑒 ∈ ℂ)
156		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ (𝐶‘𝑛))
157	153, 156	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑓 ∈ ℂ)
158	155, 157	subcld 11620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑒 − 𝑓) ∈ ℂ)
159	158	cjcld 15235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑒 − 𝑓)) ∈ ℂ)
160	158, 159	mulcld 11281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) ∈ ℂ)
161		simp-5r 786	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ (𝐶‘𝑛))
162	153, 161	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ∈ ℂ)
163	162	cjcld 15235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑑) ∈ ℂ)
164		simp-8r 792	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ (𝐶‘𝑛))
165	153, 164	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ∈ ℂ)
166	162, 165	addcld 11280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 + 𝑎) ∈ ℂ)
167	163, 166	mulcld 11281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 + 𝑎)) ∈ ℂ)
168	160, 167	subcld 11620	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) ∈ ℂ)
169		simp-7r 790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ (𝐶‘𝑛))
170	153, 169	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑏 ∈ ℂ)
171		simp-6r 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ (𝐶‘𝑛))
172	153, 171	sseldd 3984	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑐 ∈ ℂ)
173	170, 172	subcld 11620	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑏 − 𝑐) ∈ ℂ)
174	173	cjcld 15235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑏 − 𝑐)) ∈ ℂ)
175	173, 174	mulcld 11281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) ∈ ℂ)
176	165	cjcld 15235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘𝑎) ∈ ℂ)
177	176, 166	mulcld 11281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 + 𝑎)) ∈ ℂ)
178	175, 177	subcld 11620	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎))) ∈ ℂ)
179	168, 178	subcld 11620	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) ∈ ℂ)
180	163, 176	subcld 11620	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ∈ ℂ)
181	162, 165	cjsubd 32752	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) = ((∗‘𝑑) − (∗‘𝑎)))
182	162, 165	subcld 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ∈ ℂ)
183		simpr1 1195	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑎 ≠ 𝑑)
184	183	necomd 2996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → 𝑑 ≠ 𝑎)
185	162, 165, 184	subne0d 11629	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 − 𝑎) ≠ 0)
186	182, 185	cjne0d 15242	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (∗‘(𝑑 − 𝑎)) ≠ 0)
187	181, 186	eqnetrrd 3009	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) − (∗‘𝑎)) ≠ 0)
188	179, 180, 187	divcld 12043	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
189	162, 165	mulcld 11281	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑑 · 𝑎) ∈ ℂ)
190	176, 189	mulcld 11281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑎) · (𝑑 · 𝑎)) ∈ ℂ)
191	175, 162	mulcld 11281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑) ∈ ℂ)
192	190, 191	subcld 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) ∈ ℂ)
193	163, 189	mulcld 11281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((∗‘𝑑) · (𝑑 · 𝑎)) ∈ ℂ)
194	160, 165	mulcld 11281	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎) ∈ ℂ)
195	193, 194	subcld 11620	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎)) ∈ ℂ)
196	192, 195	subcld 11620	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) ∈ ℂ)
197	196, 180, 187	divcld 12043	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
198	197	negcld 11607	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) ∈ ℂ)
199	150	sqcld 14184	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (𝑥↑2) ∈ ℂ)
200	199	mullidd 11279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (1 · (𝑥↑2)) = (𝑥↑2))
201	200	oveq1d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = ((𝑥↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))))
202		simpr2 1196	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)))
203		simpr3 1197	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))
204		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) = ((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐)))
205		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) = ((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓)))
206		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) = (((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))
207		eqid 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))) = -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))
208	153, 164, 169, 171, 161, 154, 156, 150, 183, 202, 203, 204, 205, 206, 207	constrrtcc 33776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((𝑥↑2) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0)
209	201, 208	eqtrd 2777	. . . . . . . . . . . . . . . . 17 ⊢ ((((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) ∧ 𝑥 ∈ ℂ) ∧ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) → ((1 · (𝑥↑2)) + (((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) · 𝑥) + -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎))))) = 0)
210	150, 151, 152, 188, 198, 209	quad3d 32754	. . . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . . . 14 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → ∀𝑥 ∈ ℂ ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) → (𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) + (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)) ∨ 𝑥 = ((-(((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎))) − (√‘(((((((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) − ((∗‘𝑑) · (𝑑 + 𝑎))) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) − ((∗‘𝑎) · (𝑑 + 𝑎)))) / ((∗‘𝑑) − (∗‘𝑎)))↑2) − (4 · (1 · -(((((∗‘𝑎) · (𝑑 · 𝑎)) − (((𝑏 − 𝑐) · (∗‘(𝑏 − 𝑐))) · 𝑑)) − (((∗‘𝑑) · (𝑑 · 𝑎)) − (((𝑒 − 𝑓) · (∗‘(𝑒 − 𝑓))) · 𝑎))) / ((∗‘𝑑) − (∗‘𝑎)))))))) / (2 · 1)))))
213		rabsspr 32520	. . . . . . . . . . . . . 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 9301	. . . . . . . . . . . 12 ⊢ ((((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) ∧ 𝑓 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
216	147, 215	rabrexfi 32525	. . . . . . . . . . 11 ⊢ (((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) ∧ 𝑒 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
217	146, 216	rabrexfi 32525	. . . . . . . . . 10 ⊢ ((((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) ∧ 𝑑 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
218	29, 217	rabrexfi 32525	. . . . . . . . 9 ⊢ (((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) ∧ 𝑐 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
219	28, 218	rabrexfi 32525	. . . . . . . 8 ⊢ ((((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) ∧ 𝑏 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
220	27, 219	rabrexfi 32525	. . . . . . 7 ⊢ (((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) ∧ 𝑎 ∈ (𝐶‘𝑛)) → {𝑥 ∈ ℂ ∣ ∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
221	26, 220	rabrexfi 32525	. . . . . 6 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))} ∈ Fin)
222	145, 221	unfid 9212	. . . . 5 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (({𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)} ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))}) ∪ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ (𝐶‘𝑛)∃𝑏 ∈ (𝐶‘𝑛)∃𝑐 ∈ (𝐶‘𝑛)∃𝑑 ∈ (𝐶‘𝑛)∃𝑒 ∈ (𝐶‘𝑛)∃𝑓 ∈ (𝐶‘𝑛)(𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))}) ∈ Fin)
223	25, 222	eqeltrd 2841	. . . 4 ⊢ ((𝑛 ∈ ω ∧ (𝐶‘𝑛) ∈ Fin) → (𝐶‘suc 𝑛) ∈ Fin)
224	223	ex 412	. . 3 ⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ∈ Fin → (𝐶‘suc 𝑛) ∈ Fin))
225	3, 5, 7, 9, 13, 224	finds 7918	. 2 ⊢ (𝑁 ∈ ω → (𝐶‘𝑁) ∈ Fin)
226	1, 225	syl 17	1 ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3436  Vcvv 3480   ∪ cun 3949   ⊆ wss 3951  ∅c0 4333  {csn 4626  {cpr 4628   ↦ cmpt 5225  Oncon0 6384  suc csuc 6386  ‘cfv 6561  (class class class)co 7431  ωcom 7887  reccrdg 8449  Fincfn 8985  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   − cmin 11492  -cneg 11493   / cdiv 11920  2c2 12321  4c4 12323  ↑cexp 14102  ∗ccj 15135  ℑcim 15137  √csqrt 15272  abscabs 15273

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

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

This theorem is referenced by:  constrextdg2lem  33789