Metamath Proof Explorer


Definition df-constr

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)

Ref Expression
Assertion df-constr Constr = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) “ ω )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cconstr Constr
1 vs 𝑠
2 cvv V
3 vx 𝑥
4 cc
5 va 𝑎
6 1 cv 𝑠
7 vb 𝑏
8 vc 𝑐
9 vd 𝑑
10 vt 𝑡
11 cr
12 vr 𝑟
13 3 cv 𝑥
14 5 cv 𝑎
15 caddc +
16 10 cv 𝑡
17 cmul ·
18 7 cv 𝑏
19 cmin
20 18 14 19 co ( 𝑏𝑎 )
21 16 20 17 co ( 𝑡 · ( 𝑏𝑎 ) )
22 14 21 15 co ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) )
23 13 22 wceq 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) )
24 8 cv 𝑐
25 12 cv 𝑟
26 9 cv 𝑑
27 26 24 19 co ( 𝑑𝑐 )
28 25 27 17 co ( 𝑟 · ( 𝑑𝑐 ) )
29 24 28 15 co ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) )
30 13 29 wceq 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) )
31 cim
32 ccj
33 20 32 cfv ( ∗ ‘ ( 𝑏𝑎 ) )
34 33 27 17 co ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) )
35 34 31 cfv ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) )
36 cc0 0
37 35 36 wne ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0
38 23 30 37 w3a ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
39 38 12 11 wrex 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
40 39 10 11 wrex 𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
41 40 9 6 wrex 𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
42 41 8 6 wrex 𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
43 42 7 6 wrex 𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
44 43 5 6 wrex 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 )
45 ve 𝑒
46 vf 𝑓
47 cabs abs
48 13 24 19 co ( 𝑥𝑐 )
49 48 47 cfv ( abs ‘ ( 𝑥𝑐 ) )
50 45 cv 𝑒
51 46 cv 𝑓
52 50 51 19 co ( 𝑒𝑓 )
53 52 47 cfv ( abs ‘ ( 𝑒𝑓 ) )
54 49 53 wceq ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) )
55 23 54 wa ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
56 55 10 11 wrex 𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
57 56 46 6 wrex 𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
58 57 45 6 wrex 𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
59 58 8 6 wrex 𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
60 59 7 6 wrex 𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
61 60 5 6 wrex 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
62 14 26 wne 𝑎𝑑
63 13 14 19 co ( 𝑥𝑎 )
64 63 47 cfv ( abs ‘ ( 𝑥𝑎 ) )
65 18 24 19 co ( 𝑏𝑐 )
66 65 47 cfv ( abs ‘ ( 𝑏𝑐 ) )
67 64 66 wceq ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) )
68 13 26 19 co ( 𝑥𝑑 )
69 68 47 cfv ( abs ‘ ( 𝑥𝑑 ) )
70 69 53 wceq ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) )
71 62 67 70 w3a ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
72 71 46 6 wrex 𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
73 72 45 6 wrex 𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
74 73 9 6 wrex 𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
75 74 8 6 wrex 𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
76 75 7 6 wrex 𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
77 76 5 6 wrex 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) )
78 44 61 77 w3o ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) )
79 78 3 4 crab { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) }
80 1 2 79 cmpt ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } )
81 c1 1
82 36 81 cpr { 0 , 1 }
83 80 82 crdg rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } )
84 com ω
85 83 84 cima ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) “ ω )
86 0 85 wceq Constr = ( rec ( ( 𝑠 ∈ V ↦ { 𝑥 ∈ ℂ ∣ ( ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑡 ∈ ℝ ∃ 𝑟 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ 𝑥 = ( 𝑐 + ( 𝑟 · ( 𝑑𝑐 ) ) ) ∧ ( ℑ ‘ ( ( ∗ ‘ ( 𝑏𝑎 ) ) · ( 𝑑𝑐 ) ) ) ≠ 0 ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑒𝑠𝑓𝑠𝑡 ∈ ℝ ( 𝑥 = ( 𝑎 + ( 𝑡 · ( 𝑏𝑎 ) ) ) ∧ ( abs ‘ ( 𝑥𝑐 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ∨ ∃ 𝑎𝑠𝑏𝑠𝑐𝑠𝑑𝑠𝑒𝑠𝑓𝑠 ( 𝑎𝑑 ∧ ( abs ‘ ( 𝑥𝑎 ) ) = ( abs ‘ ( 𝑏𝑐 ) ) ∧ ( abs ‘ ( 𝑥𝑑 ) ) = ( abs ‘ ( 𝑒𝑓 ) ) ) ) } ) , { 0 , 1 } ) “ ω )