Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-constr Structured version   Visualization version   GIF version

Definition df-constr 33713
Description: Define the set of geometrically constructible points, by recursively adding the line-line, line-circle and circle-circle intersections constructions using points in a previous iteration. (Contributed by Saveliy Skresanov, 19-Jan-2025.)
Assertion
Ref Expression
df-constr Constr = (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1}) “ ω)
Distinct variable group:   𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑟,𝑠,𝑡,𝑥

Detailed syntax breakdown of Definition df-constr
StepHypRef Expression
1 cconstr 33712 . 2 class Constr
2 vs . . . . 5 setvar 𝑠
3 cvv 3482 . . . . 5 class V
4 vx . . . . . . . . . . . . . . . 16 setvar 𝑥
54cv 1536 . . . . . . . . . . . . . . 15 class 𝑥
6 va . . . . . . . . . . . . . . . . 17 setvar 𝑎
76cv 1536 . . . . . . . . . . . . . . . 16 class 𝑎
8 vt . . . . . . . . . . . . . . . . . 18 setvar 𝑡
98cv 1536 . . . . . . . . . . . . . . . . 17 class 𝑡
10 vb . . . . . . . . . . . . . . . . . . 19 setvar 𝑏
1110cv 1536 . . . . . . . . . . . . . . . . . 18 class 𝑏
12 cmin 11516 . . . . . . . . . . . . . . . . . 18 class
1311, 7, 12co 7445 . . . . . . . . . . . . . . . . 17 class (𝑏𝑎)
14 cmul 11185 . . . . . . . . . . . . . . . . 17 class ·
159, 13, 14co 7445 . . . . . . . . . . . . . . . 16 class (𝑡 · (𝑏𝑎))
16 caddc 11183 . . . . . . . . . . . . . . . 16 class +
177, 15, 16co 7445 . . . . . . . . . . . . . . 15 class (𝑎 + (𝑡 · (𝑏𝑎)))
185, 17wceq 1537 . . . . . . . . . . . . . 14 wff 𝑥 = (𝑎 + (𝑡 · (𝑏𝑎)))
19 vc . . . . . . . . . . . . . . . . 17 setvar 𝑐
2019cv 1536 . . . . . . . . . . . . . . . 16 class 𝑐
21 vr . . . . . . . . . . . . . . . . . 18 setvar 𝑟
2221cv 1536 . . . . . . . . . . . . . . . . 17 class 𝑟
23 vd . . . . . . . . . . . . . . . . . . 19 setvar 𝑑
2423cv 1536 . . . . . . . . . . . . . . . . . 18 class 𝑑
2524, 20, 12co 7445 . . . . . . . . . . . . . . . . 17 class (𝑑𝑐)
2622, 25, 14co 7445 . . . . . . . . . . . . . . . 16 class (𝑟 · (𝑑𝑐))
2720, 26, 16co 7445 . . . . . . . . . . . . . . 15 class (𝑐 + (𝑟 · (𝑑𝑐)))
285, 27wceq 1537 . . . . . . . . . . . . . 14 wff 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐)))
29 ccj 15141 . . . . . . . . . . . . . . . . . 18 class
3013, 29cfv 6572 . . . . . . . . . . . . . . . . 17 class (∗‘(𝑏𝑎))
3130, 25, 14co 7445 . . . . . . . . . . . . . . . 16 class ((∗‘(𝑏𝑎)) · (𝑑𝑐))
32 cim 15143 . . . . . . . . . . . . . . . 16 class
3331, 32cfv 6572 . . . . . . . . . . . . . . 15 class (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐)))
34 cc0 11180 . . . . . . . . . . . . . . 15 class 0
3533, 34wne 2942 . . . . . . . . . . . . . 14 wff (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0
3618, 28, 35w3a 1087 . . . . . . . . . . . . 13 wff (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)
37 cr 11179 . . . . . . . . . . . . 13 class
3836, 21, 37wrex 3072 . . . . . . . . . . . 12 wff 𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)
3938, 8, 37wrex 3072 . . . . . . . . . . 11 wff 𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)
402cv 1536 . . . . . . . . . . 11 class 𝑠
4139, 23, 40wrex 3072 . . . . . . . . . 10 wff 𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)
4241, 19, 40wrex 3072 . . . . . . . . 9 wff 𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)
4342, 10, 40wrex 3072 . . . . . . . 8 wff 𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)
4443, 6, 40wrex 3072 . . . . . . 7 wff 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0)
455, 20, 12co 7445 . . . . . . . . . . . . . . . 16 class (𝑥𝑐)
46 cabs 15279 . . . . . . . . . . . . . . . 16 class abs
4745, 46cfv 6572 . . . . . . . . . . . . . . 15 class (abs‘(𝑥𝑐))
48 ve . . . . . . . . . . . . . . . . . 18 setvar 𝑒
4948cv 1536 . . . . . . . . . . . . . . . . 17 class 𝑒
50 vf . . . . . . . . . . . . . . . . . 18 setvar 𝑓
5150cv 1536 . . . . . . . . . . . . . . . . 17 class 𝑓
5249, 51, 12co 7445 . . . . . . . . . . . . . . . 16 class (𝑒𝑓)
5352, 46cfv 6572 . . . . . . . . . . . . . . 15 class (abs‘(𝑒𝑓))
5447, 53wceq 1537 . . . . . . . . . . . . . 14 wff (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))
5518, 54wa 395 . . . . . . . . . . . . 13 wff (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))
5655, 8, 37wrex 3072 . . . . . . . . . . . 12 wff 𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))
5756, 50, 40wrex 3072 . . . . . . . . . . 11 wff 𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))
5857, 48, 40wrex 3072 . . . . . . . . . 10 wff 𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))
5958, 19, 40wrex 3072 . . . . . . . . 9 wff 𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))
6059, 10, 40wrex 3072 . . . . . . . 8 wff 𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))
6160, 6, 40wrex 3072 . . . . . . 7 wff 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓)))
627, 24wne 2942 . . . . . . . . . . . . . 14 wff 𝑎𝑑
635, 7, 12co 7445 . . . . . . . . . . . . . . . 16 class (𝑥𝑎)
6463, 46cfv 6572 . . . . . . . . . . . . . . 15 class (abs‘(𝑥𝑎))
6511, 20, 12co 7445 . . . . . . . . . . . . . . . 16 class (𝑏𝑐)
6665, 46cfv 6572 . . . . . . . . . . . . . . 15 class (abs‘(𝑏𝑐))
6764, 66wceq 1537 . . . . . . . . . . . . . 14 wff (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐))
685, 24, 12co 7445 . . . . . . . . . . . . . . . 16 class (𝑥𝑑)
6968, 46cfv 6572 . . . . . . . . . . . . . . 15 class (abs‘(𝑥𝑑))
7069, 53wceq 1537 . . . . . . . . . . . . . 14 wff (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))
7162, 67, 70w3a 1087 . . . . . . . . . . . . 13 wff (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))
7271, 50, 40wrex 3072 . . . . . . . . . . . 12 wff 𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))
7372, 48, 40wrex 3072 . . . . . . . . . . 11 wff 𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))
7473, 23, 40wrex 3072 . . . . . . . . . 10 wff 𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))
7574, 19, 40wrex 3072 . . . . . . . . 9 wff 𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))
7675, 10, 40wrex 3072 . . . . . . . 8 wff 𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))
7776, 6, 40wrex 3072 . . . . . . 7 wff 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓)))
7844, 61, 77w3o 1086 . . . . . 6 wff (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))
79 cc 11178 . . . . . 6 class
8078, 4, 79crab 3438 . . . . 5 class {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}
812, 3, 80cmpt 5252 . . . 4 class (𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))})
82 c1 11181 . . . . 5 class 1
8334, 82cpr 4650 . . . 4 class {0, 1}
8481, 83crdg 8461 . . 3 class rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1})
85 com 7899 . . 3 class ω
8684, 85cima 5702 . 2 class (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1}) “ ω)
871, 86wceq 1537 1 wff Constr = (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑𝑐))) ∧ (ℑ‘((∗‘(𝑏𝑎)) · (𝑑𝑐))) ≠ 0) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏𝑎))) ∧ (abs‘(𝑥𝑐)) = (abs‘(𝑒𝑓))) ∨ ∃𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 (𝑎𝑑 ∧ (abs‘(𝑥𝑎)) = (abs‘(𝑏𝑐)) ∧ (abs‘(𝑥𝑑)) = (abs‘(𝑒𝑓))))}), {0, 1}) “ ω)
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator