constrext2chn - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > constrext2chn		Structured version Visualization version GIF version

Theorem constrext2chn 33722

Description: If a constructible number generates some subfield 𝐿 of ℂ, then the degree of the extension of 𝐿 over ℚ is a power of two. (Contributed by Thierry Arnoux, 26-Oct-2025.)

**Hypotheses**
Ref	Expression
constrext2chn.q	⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
constrext2chn.l	⊢ 𝐿 = (ℂ_fld ↾_s 𝑆)
constrext2chn.s	⊢ 𝑆 = (ℂ_fld fldGen (ℚ ∪ {𝐴}))
constrext2chn.a	⊢ (𝜑 → 𝐴 ∈ Constr)

**Assertion**
Ref	Expression
constrext2chn	⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛))

Distinct variable groups: 𝐴,𝑛 𝑛,𝐿 𝑄,𝑛 𝑆,𝑛 𝜑,𝑛

Proof of Theorem constrext2chn Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑖 𝑗 𝑘 𝑙 𝑚 𝑜 𝑝 𝑞 𝑟 𝑠 𝑡 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 = 𝑡 → (𝑜 · (𝑗 − 𝑖)) = (𝑡 · (𝑗 − 𝑖)))
2	1	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑜 = 𝑡 → (𝑖 + (𝑜 · (𝑗 − 𝑖))) = (𝑖 + (𝑡 · (𝑗 − 𝑖))))
3	2	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑜 = 𝑡 → (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ↔ 𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖)))))
4	3	3anbi1d 1441	. . . . . . . . . . . . 13 ⊢ (𝑜 = 𝑡 → ((𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0)))
5		oveq1 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑟 → (𝑝 · (𝑙 − 𝑘)) = (𝑟 · (𝑙 − 𝑘)))
6	5	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑟 → (𝑘 + (𝑝 · (𝑙 − 𝑘))) = (𝑘 + (𝑟 · (𝑙 − 𝑘))))
7	6	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑟 → (𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ↔ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘)))))
8	7	3anbi2d 1442	. . . . . . . . . . . . 13 ⊢ (𝑝 = 𝑟 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0)))
9	4, 8	cbvrex2vw 3228	. . . . . . . . . . . 12 ⊢ (∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0))
10	9	2rexbii 3116	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0))
11		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑐 → 𝑘 = 𝑐)
12		oveq2 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑐 → (𝑙 − 𝑘) = (𝑙 − 𝑐))
13	12	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑐 → (𝑟 · (𝑙 − 𝑘)) = (𝑟 · (𝑙 − 𝑐)))
14	11, 13	oveq12d 7430	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → (𝑘 + (𝑟 · (𝑙 − 𝑘))) = (𝑐 + (𝑟 · (𝑙 − 𝑐))))
15	14	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → (𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ↔ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐)))))
16	12	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑐 → ((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘)) = ((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐)))
17	16	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) = (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))))
18	17	neeq1d 2990	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → ((ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0 ↔ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0))
19	15, 18	3anbi23d 1440	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑐 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0)))
20	19	2rexbidv 3209	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑐 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0)))
21		oveq1 7419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑙 = 𝑑 → (𝑙 − 𝑐) = (𝑑 − 𝑐))
22	21	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑑 → (𝑟 · (𝑙 − 𝑐)) = (𝑟 · (𝑑 − 𝑐)))
23	22	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑑 → (𝑐 + (𝑟 · (𝑙 − 𝑐))) = (𝑐 + (𝑟 · (𝑑 − 𝑐))))
24	23	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑑 → (𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ↔ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐)))))
25	21	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑑 → ((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐)) = ((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐)))
26	25	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑑 → (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) = (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))))
27	26	neeq1d 2990	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑑 → ((ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
28	24, 27	3anbi23d 1440	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑑 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0)))
29	28	2rexbidv 3209	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑑 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑙 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0)))
30	20, 29	cbvrex2vw 3228	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑟 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
31	10, 30	bitri 275	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
32	31	2rexbii 3116	. . . . . . . . 9 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ↔ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0))
33		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = 𝑓 → (𝑚 − 𝑞) = (𝑚 − 𝑓))
34	33	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑓 → (abs‘(𝑚 − 𝑞)) = (abs‘(𝑚 − 𝑓)))
35	34	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑓 → ((abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞)) ↔ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))))
36	35	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑓 → ((𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓)))))
37	3	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (𝑜 = 𝑡 → ((𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓)))))
38	36, 37	cbvrex2vw 3228	. . . . . . . . . . . 12 ⊢ (∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))))
39	38	2rexbii 3116	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))))
40		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑐 → (𝑦 − 𝑘) = (𝑦 − 𝑐))
41	40	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → (abs‘(𝑦 − 𝑘)) = (abs‘(𝑦 − 𝑐)))
42	41	eqeq1d 2736	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → ((abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓)) ↔ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓))))
43	42	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑐 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓)))))
44	43	2rexbidv 3209	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑐 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓)))))
45		oveq1 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑒 → (𝑚 − 𝑓) = (𝑒 − 𝑓))
46	45	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑒 → (abs‘(𝑚 − 𝑓)) = (abs‘(𝑒 − 𝑓)))
47	46	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑒 → ((abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓)) ↔ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
48	47	anbi2d 630	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑒 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓))) ↔ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
49	48	2rexbidv 3209	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑒 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑚 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
50	44, 49	cbvrex2vw 3228	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
51	39, 50	bitri 275	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
52	51	2rexbii 3116	. . . . . . . . 9 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
53		oveq1 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑒 → (𝑚 − 𝑞) = (𝑒 − 𝑞))
54	53	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑒 → (abs‘(𝑚 − 𝑞)) = (abs‘(𝑒 − 𝑞)))
55	54	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑒 → ((abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞)) ↔ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞))))
56	55	3anbi3d 1443	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑒 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞)))))
57		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 = 𝑓 → (𝑒 − 𝑞) = (𝑒 − 𝑓))
58	57	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑞 = 𝑓 → (abs‘(𝑒 − 𝑞)) = (abs‘(𝑒 − 𝑓)))
59	58	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑞 = 𝑓 → ((abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞)) ↔ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))))
60	59	3anbi3d 1443	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑓 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑞))) ↔ (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)))))
61	56, 60	cbvrex2vw 3228	. . . . . . . . . . . 12 ⊢ (∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))))
62	61	2rexbii 3116	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))))
63		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑐 → (𝑗 − 𝑘) = (𝑗 − 𝑐))
64	63	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑐 → (abs‘(𝑗 − 𝑘)) = (abs‘(𝑗 − 𝑐)))
65	64	eqeq2d 2745	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑐 → ((abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ↔ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐))))
66	65	3anbi2d 1442	. . . . . . . . . . . . 13 ⊢ (𝑘 = 𝑐 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)))))
67	66	2rexbidv 3209	. . . . . . . . . . . 12 ⊢ (𝑘 = 𝑐 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)))))
68		neeq2 2994	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑑 → (𝑖 ≠ 𝑙 ↔ 𝑖 ≠ 𝑑))
69		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 = 𝑑 → (𝑦 − 𝑙) = (𝑦 − 𝑑))
70	69	fveq2d 6889	. . . . . . . . . . . . . . 15 ⊢ (𝑙 = 𝑑 → (abs‘(𝑦 − 𝑙)) = (abs‘(𝑦 − 𝑑)))
71	70	eqeq1d 2736	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑑 → ((abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓)) ↔ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
72	68, 71	3anbi13d 1439	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑑 → ((𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
73	72	2rexbidv 3209	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑑 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
74	67, 73	cbvrex2vw 3228	. . . . . . . . . . 11 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
75	62, 74	bitri 275	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
76	75	2rexbii 3116	. . . . . . . . 9 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))) ↔ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
77	32, 52, 76	3orbi123i 1156	. . . . . . . 8 ⊢ ((∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞)))) ↔ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
78		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑎 → 𝑖 = 𝑎)
79		oveq2 7420	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑎 → (𝑗 − 𝑖) = (𝑗 − 𝑎))
80	79	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑎 → (𝑡 · (𝑗 − 𝑖)) = (𝑡 · (𝑗 − 𝑎)))
81	78, 80	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑎 → (𝑖 + (𝑡 · (𝑗 − 𝑖))) = (𝑎 + (𝑡 · (𝑗 − 𝑎))))
82	81	eqeq2d 2745	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑎 → (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ↔ 𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎)))))
83	79	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑎 → (∗‘(𝑗 − 𝑖)) = (∗‘(𝑗 − 𝑎)))
84	83	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑎 → ((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐)) = ((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐)))
85	84	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑎 → (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) = (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))))
86	85	neeq1d 2990	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑎 → ((ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
87	82, 86	3anbi13d 1439	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑎 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
88	87	2rexbidv 3209	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑎 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
89	88	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
90		oveq1 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑏 → (𝑗 − 𝑎) = (𝑏 − 𝑎))
91	90	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑏 → (𝑡 · (𝑗 − 𝑎)) = (𝑡 · (𝑏 − 𝑎)))
92	91	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑏 → (𝑎 + (𝑡 · (𝑗 − 𝑎))) = (𝑎 + (𝑡 · (𝑏 − 𝑎))))
93	92	eqeq2d 2745	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑏 → (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ↔ 𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))))
94	90	fveq2d 6889	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑏 → (∗‘(𝑗 − 𝑎)) = (∗‘(𝑏 − 𝑎)))
95	94	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑏 → ((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐)) = ((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐)))
96	95	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑏 → (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) = (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))))
97	96	neeq1d 2990	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑏 → ((ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
98	93, 97	3anbi13d 1439	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑏 → ((𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
99	98	2rexbidv 3209	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑏 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
100	99	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑗 = 𝑏 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
101	89, 100	cbvrex2vw 3228	. . . . . . . . 9 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
102	82	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑎 → ((𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
103	102	2rexbidv 3209	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑎 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
104	103	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
105	93	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑏 → ((𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
106	105	2rexbidv 3209	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑏 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
107	106	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑗 = 𝑏 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑗 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
108	104, 107	cbvrex2vw 3228	. . . . . . . . 9 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
109		neeq1 2993	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑎 → (𝑖 ≠ 𝑑 ↔ 𝑎 ≠ 𝑑))
110		oveq2 7420	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑎 → (𝑦 − 𝑖) = (𝑦 − 𝑎))
111	110	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑎 → (abs‘(𝑦 − 𝑖)) = (abs‘(𝑦 − 𝑎)))
112	111	eqeq1d 2736	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑎 → ((abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ↔ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐))))
113	109, 112	3anbi12d 1438	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑎 → ((𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
114	113	2rexbidv 3209	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑎 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
115	114	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑖 = 𝑎 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
116		oveq1 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑏 → (𝑗 − 𝑐) = (𝑏 − 𝑐))
117	116	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝑏 → (abs‘(𝑗 − 𝑐)) = (abs‘(𝑏 − 𝑐)))
118	117	eqeq2d 2745	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝑏 → ((abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ↔ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐))))
119	118	3anbi2d 1442	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑏 → ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
120	119	2rexbidv 3209	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑏 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
121	120	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑗 = 𝑏 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
122	115, 121	cbvrex2vw 3228	. . . . . . . . 9 ⊢ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
123	101, 108, 122	3orbi123i 1156	. . . . . . . 8 ⊢ ((∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑖 + (𝑡 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑖 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
124	77, 123	bitri 275	. . . . . . 7 ⊢ ((∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞)))) ↔ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
125	124	rabbii 3425	. . . . . 6 ⊢ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))} = {𝑦 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
126		eqeq1 2738	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ↔ 𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎)))))
127		eqeq1 2738	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ↔ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐)))))
128		biidd 262	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0 ↔ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))
129	126, 127, 128	3anbi123d 1437	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
130	129	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
131	130	2rexbidv 3209	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
132	131	2rexbidv 3209	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
133		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝑐) = (𝑥 − 𝑐))
134	133	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (abs‘(𝑦 − 𝑐)) = (abs‘(𝑥 − 𝑐)))
135	134	eqeq1d 2736	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓)) ↔ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))
136	126, 135	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
137	136	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
138	137	2rexbidv 3209	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
139	138	2rexbidv 3209	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
140		biidd 262	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑎 ≠ 𝑑 ↔ 𝑎 ≠ 𝑑))
141		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝑎) = (𝑥 − 𝑎))
142	141	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (abs‘(𝑦 − 𝑎)) = (abs‘(𝑥 − 𝑎)))
143	142	eqeq1d 2736	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ↔ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐))))
144		oveq1 7419	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑥 → (𝑦 − 𝑑) = (𝑥 − 𝑑))
145	144	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑥 → (abs‘(𝑦 − 𝑑)) = (abs‘(𝑥 − 𝑑)))
146	145	eqeq1d 2736	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → ((abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)) ↔ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))
147	140, 143, 146	3anbi123d 1437	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → ((𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
148	147	2rexbidv 3209	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
149	148	2rexbidv 3209	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
150	149	2rexbidv 3209	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
151	132, 139, 150	3orbi123d 1436	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
152	151	cbvrabv 3430	. . . . . 6 ⊢ {𝑦 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑦 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑦 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑦 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑦 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑦 − 𝑑)) = (abs‘(𝑒 − 𝑓))))} = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
153	125, 152	eqtri 2757	. . . . 5 ⊢ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))} = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}
154	153	mpteq2i 5227	. . . 4 ⊢ (𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}) = (𝑧 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
155		elequ2 2122	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (𝑎 ∈ 𝑧 ↔ 𝑎 ∈ 𝑠))
156		elequ2 2122	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → (𝑏 ∈ 𝑧 ↔ 𝑏 ∈ 𝑠))
157		elequ2 2122	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑠 → (𝑐 ∈ 𝑧 ↔ 𝑐 ∈ 𝑠))
158		rexeq 3305	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑠 → (∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
159	157, 158	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑠 → ((𝑐 ∈ 𝑧 ∧ ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) ↔ (𝑐 ∈ 𝑠 ∧ ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))))
160	159	rexbidv2 3162	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
161	156, 160	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → ((𝑏 ∈ 𝑧 ∧ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) ↔ (𝑏 ∈ 𝑠 ∧ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))))
162	161	rexbidv2 3162	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
163	155, 162	anbi12d 632	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → ((𝑎 ∈ 𝑧 ∧ ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)) ↔ (𝑎 ∈ 𝑠 ∧ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0))))
164	163	rexbidv2 3162	. . . . . . 7 ⊢ (𝑧 = 𝑠 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ↔ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0)))
165		elequ2 2122	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑠 → (𝑒 ∈ 𝑧 ↔ 𝑒 ∈ 𝑠))
166		rexeq 3305	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑠 → (∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
167	165, 166	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑠 → ((𝑒 ∈ 𝑧 ∧ ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑒 ∈ 𝑠 ∧ ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
168	167	rexbidv2 3162	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑠 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
169	157, 168	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑠 → ((𝑐 ∈ 𝑧 ∧ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑐 ∈ 𝑠 ∧ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
170	169	rexbidv2 3162	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → (∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
171	156, 170	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → ((𝑏 ∈ 𝑧 ∧ ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑏 ∈ 𝑠 ∧ ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
172	171	rexbidv2 3162	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
173	155, 172	anbi12d 632	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → ((𝑎 ∈ 𝑧 ∧ ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑎 ∈ 𝑠 ∧ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))))))
174	173	rexbidv2 3162	. . . . . . 7 ⊢ (𝑧 = 𝑠 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓)))))
175		elequ2 2122	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑠 → (𝑑 ∈ 𝑧 ↔ 𝑑 ∈ 𝑠))
176		rexeq 3305	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = 𝑠 → (∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
177	165, 176	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = 𝑠 → ((𝑒 ∈ 𝑧 ∧ ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑒 ∈ 𝑠 ∧ ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
178	177	rexbidv2 3162	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑠 → (∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
179	175, 178	anbi12d 632	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑠 → ((𝑑 ∈ 𝑧 ∧ ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑑 ∈ 𝑠 ∧ ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
180	179	rexbidv2 3162	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑠 → (∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
181	157, 180	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑠 → ((𝑐 ∈ 𝑧 ∧ ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑐 ∈ 𝑠 ∧ ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
182	181	rexbidv2 3162	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑠 → (∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
183	156, 182	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑧 = 𝑠 → ((𝑏 ∈ 𝑧 ∧ ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑏 ∈ 𝑠 ∧ ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
184	183	rexbidv2 3162	. . . . . . . . 9 ⊢ (𝑧 = 𝑠 → (∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
185	155, 184	anbi12d 632	. . . . . . . 8 ⊢ (𝑧 = 𝑠 → ((𝑎 ∈ 𝑧 ∧ ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (𝑎 ∈ 𝑠 ∧ ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
186	185	rexbidv2 3162	. . . . . . 7 ⊢ (𝑧 = 𝑠 → (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))) ↔ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))))
187	164, 174, 186	3orbi123d 1436	. . . . . 6 ⊢ (𝑧 = 𝑠 → ((∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓)))) ↔ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))
188	187	rabbidv 3427	. . . . 5 ⊢ (𝑧 = 𝑠 → {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))} = {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
189	188	cbvmptv 5235	. . . 4 ⊢ (𝑧 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑧 ∃𝑏 ∈ 𝑧 ∃𝑐 ∈ 𝑧 ∃𝑑 ∈ 𝑧 ∃𝑒 ∈ 𝑧 ∃𝑓 ∈ 𝑧 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}) = (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
190	154, 189	eqtri 2757	. . 3 ⊢ (𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}) = (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))})
191		rdgeq1 8432	. . 3 ⊢ ((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}) = (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}) → rec((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}), {0, 1}) = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}))
192	190, 191	ax-mp 5	. 2 ⊢ rec((𝑧 ∈ V ↦ {𝑦 ∈ ℂ ∣ (∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑜 ∈ ℝ ∃𝑝 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ 𝑦 = (𝑘 + (𝑝 · (𝑙 − 𝑘))) ∧ (ℑ‘((∗‘(𝑗 − 𝑖)) · (𝑙 − 𝑘))) ≠ 0) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 ∃𝑜 ∈ ℝ (𝑦 = (𝑖 + (𝑜 · (𝑗 − 𝑖))) ∧ (abs‘(𝑦 − 𝑘)) = (abs‘(𝑚 − 𝑞))) ∨ ∃𝑖 ∈ 𝑧 ∃𝑗 ∈ 𝑧 ∃𝑘 ∈ 𝑧 ∃𝑙 ∈ 𝑧 ∃𝑚 ∈ 𝑧 ∃𝑞 ∈ 𝑧 (𝑖 ≠ 𝑙 ∧ (abs‘(𝑦 − 𝑖)) = (abs‘(𝑗 − 𝑘)) ∧ (abs‘(𝑦 − 𝑙)) = (abs‘(𝑚 − 𝑞))))}), {0, 1}) = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1})
193		eqid 2734	. 2 ⊢ (ℂ_fld ↾_s 𝑒) = (ℂ_fld ↾_s 𝑒)
194		eqid 2734	. 2 ⊢ (ℂ_fld ↾_s 𝑓) = (ℂ_fld ↾_s 𝑓)
195		oveq2 7420	. . . . . 6 ⊢ (ℎ = 𝑒 → (ℂ_fld ↾_s ℎ) = (ℂ_fld ↾_s 𝑒))
196	195	adantl 481	. . . . 5 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (ℂ_fld ↾_s ℎ) = (ℂ_fld ↾_s 𝑒))
197		oveq2 7420	. . . . . 6 ⊢ (𝑔 = 𝑓 → (ℂ_fld ↾_s 𝑔) = (ℂ_fld ↾_s 𝑓))
198	197	adantr 480	. . . . 5 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (ℂ_fld ↾_s 𝑔) = (ℂ_fld ↾_s 𝑓))
199	196, 198	breq12d 5136	. . . 4 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → ((ℂ_fld ↾_s ℎ)/_FldExt(ℂ_fld ↾_s 𝑔) ↔ (ℂ_fld ↾_s 𝑒)/_FldExt(ℂ_fld ↾_s 𝑓)))
200	196, 198	oveq12d 7430	. . . . 5 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → ((ℂ_fld ↾_s ℎ)[:](ℂ_fld ↾_s 𝑔)) = ((ℂ_fld ↾_s 𝑒)[:](ℂ_fld ↾_s 𝑓)))
201	200	eqeq1d 2736	. . . 4 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (((ℂ_fld ↾_s ℎ)[:](ℂ_fld ↾_s 𝑔)) = 2 ↔ ((ℂ_fld ↾_s 𝑒)[:](ℂ_fld ↾_s 𝑓)) = 2))
202	199, 201	anbi12d 632	. . 3 ⊢ ((𝑔 = 𝑓 ∧ ℎ = 𝑒) → (((ℂ_fld ↾_s ℎ)/_FldExt(ℂ_fld ↾_s 𝑔) ∧ ((ℂ_fld ↾_s ℎ)[:](ℂ_fld ↾_s 𝑔)) = 2) ↔ ((ℂ_fld ↾_s 𝑒)/_FldExt(ℂ_fld ↾_s 𝑓) ∧ ((ℂ_fld ↾_s 𝑒)[:](ℂ_fld ↾_s 𝑓)) = 2)))
203	202	cbvopabv 5196	. 2 ⊢ {⟨𝑔, ℎ⟩ ∣ ((ℂ_fld ↾_s ℎ)/_FldExt(ℂ_fld ↾_s 𝑔) ∧ ((ℂ_fld ↾_s ℎ)[:](ℂ_fld ↾_s 𝑔)) = 2)} = {⟨𝑓, 𝑒⟩ ∣ ((ℂ_fld ↾_s 𝑒)/_FldExt(ℂ_fld ↾_s 𝑓) ∧ ((ℂ_fld ↾_s 𝑒)[:](ℂ_fld ↾_s 𝑓)) = 2)}
204		peano1 7891	. . 3 ⊢ ∅ ∈ ω
205	204	a1i 11	. 2 ⊢ (𝜑 → ∅ ∈ ω)
206		constrext2chn.q	. 2 ⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
207		constrext2chn.l	. . 3 ⊢ 𝐿 = (ℂ_fld ↾_s 𝑆)
208		constrext2chn.s	. . . 4 ⊢ 𝑆 = (ℂ_fld fldGen (ℚ ∪ {𝐴}))
209	208	oveq2i 7423	. . 3 ⊢ (ℂ_fld ↾_s 𝑆) = (ℂ_fld ↾_s (ℂ_fld fldGen (ℚ ∪ {𝐴})))
210	207, 209	eqtri 2757	. 2 ⊢ 𝐿 = (ℂ_fld ↾_s (ℂ_fld fldGen (ℚ ∪ {𝐴})))
211		constrext2chn.a	. 2 ⊢ (𝜑 → 𝐴 ∈ Constr)
212	192, 193, 194, 203, 205, 206, 210, 211	constrext2chnlem 33721	1 ⊢ (𝜑 → ∃𝑛 ∈ ℕ₀ (𝐿[:]𝑄) = (2↑𝑛))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∨ w3o 1085 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2931 ∃wrex 3059 {crab 3419 Vcvv 3463 ∪ cun 3929 ∅c0 4313 {csn 4606 {cpr 4608 class class class wbr 5123 {copab 5185 ↦ cmpt 5205 ‘cfv 6540 (class class class)co 7412 ωcom 7868 reccrdg 8430 ℂcc 11134 ℝcr 11135 0cc0 11136 1c1 11137 + caddc 11139 · cmul 11141 − cmin 11473 2c2 12302 ℕ₀cn0 12508 ℚcq 12971 ↑cexp 14083 ∗ccj 15116 ℑcim 15118 abscabs 15254 ↾_s cress 17251 ℂ_fldccnfld 21325 fldGen cfldgen 33243 /_FldExtcfldext 33615 [:]cextdg 33618 Constrcconstr 33700

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7736 ax-reg 9613 ax-inf2 9662 ax-ac2 10484 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213 ax-pre-sup 11214 ax-addf 11215 ax-mulf 11216

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6493 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7678 df-ofr 7679 df-rpss 7724 df-om 7869 df-1st 7995 df-2nd 7996 df-supp 8167 df-tpos 8232 df-frecs 8287 df-wrecs 8318 df-recs 8392 df-rdg 8431 df-1o 8487 df-2o 8488 df-oadd 8491 df-er 8726 df-ec 8728 df-qs 8732 df-map 8849 df-pm 8850 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9383 df-sup 9463 df-inf 9464 df-oi 9531 df-r1 9785 df-rank 9786 df-dju 9922 df-card 9960 df-acn 9963 df-ac 10137 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11475 df-neg 11476 df-div 11902 df-nn 12248 df-2 12310 df-3 12311 df-4 12312 df-5 12313 df-6 12314 df-7 12315 df-8 12316 df-9 12317 df-n0 12509 df-xnn0 12582 df-z 12596 df-dec 12716 df-uz 12860 df-q 12972 df-rp 13016 df-xneg 13135 df-xmul 13137 df-ico 13374 df-fz 13529 df-fzo 13676 df-fl 13813 df-mod 13891 df-seq 14024 df-exp 14084 df-hash 14351 df-word 14534 df-lsw 14582 df-concat 14590 df-s1 14615 df-substr 14660 df-pfx 14690 df-cj 15119 df-re 15120 df-im 15121 df-sqrt 15255 df-abs 15256 df-dvds 16272 df-gcd 16513 df-prm 16690 df-pc 16856 df-struct 17165 df-sets 17182 df-slot 17200 df-ndx 17212 df-base 17229 df-ress 17252 df-plusg 17285 df-mulr 17286 df-starv 17287 df-sca 17288 df-vsca 17289 df-ip 17290 df-tset 17291 df-ple 17292 df-ocomp 17293 df-ds 17294 df-unif 17295 df-hom 17296 df-cco 17297 df-0g 17456 df-gsum 17457 df-prds 17462 df-pws 17464 df-imas 17523 df-qus 17524 df-mre 17599 df-mrc 17600 df-mri 17601 df-acs 17602 df-proset 18309 df-drs 18310 df-poset 18328 df-ipo 18541 df-mgm 18621 df-sgrp 18700 df-mnd 18716 df-mhm 18764 df-submnd 18765 df-grp 18922 df-minusg 18923 df-sbg 18924 df-mulg 19054 df-subg 19109 df-nsg 19110 df-eqg 19111 df-ghm 19199 df-gim 19245 df-cntz 19303 df-oppg 19332 df-lsm 19621 df-cmn 19767 df-abl 19768 df-mgp 20105 df-rng 20117 df-ur 20146 df-srg 20151 df-ring 20199 df-cring 20200 df-oppr 20301 df-dvdsr 20324 df-unit 20325 df-irred 20326 df-invr 20355 df-dvr 20368 df-rhm 20439 df-nzr 20480 df-subrng 20513 df-subrg 20537 df-rlreg 20661 df-domn 20662 df-idom 20663 df-drng 20698 df-field 20699 df-sdrg 20755 df-lmod 20827 df-lss 20897 df-lsp 20937 df-lmhm 20988 df-lmim 20989 df-lmic 20990 df-lbs 21041 df-lvec 21069 df-sra 21139 df-rgmod 21140 df-lidl 21179 df-rsp 21180 df-2idl 21221 df-lpidl 21293 df-lpir 21294 df-pid 21308 df-cnfld 21326 df-dsmm 21705 df-frlm 21720 df-uvc 21756 df-lindf 21779 df-linds 21780 df-assa 21826 df-asp 21827 df-ascl 21828 df-psr 21882 df-mvr 21883 df-mpl 21884 df-opsr 21886 df-evls 22045 df-evl 22046 df-psr1 22128 df-vr1 22129 df-ply1 22130 df-coe1 22131 df-evls1 22266 df-evl1 22267 df-mdeg 26029 df-deg1 26030 df-mon1 26105 df-uc1p 26106 df-q1p 26107 df-r1p 26108 df-ig1p 26109 df-chn 32925 df-fldgen 33244 df-mxidl 33414 df-dim 33576 df-fldext 33619 df-extdg 33620 df-irng 33662 df-minply 33671 df-constr 33701

This theorem is referenced by: constrcon 33723

W3C validator