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 s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1 ω

Detailed syntax breakdown

Step Hyp Ref Expression
0 cconstr class Constr
1 vs setvar s
2 cvv class V
3 vx setvar x
4 cc class
5 va setvar a
6 1 cv setvar s
7 vb setvar b
8 vc setvar c
9 vd setvar d
10 vt setvar t
11 cr class
12 vr setvar r
13 3 cv setvar x
14 5 cv setvar a
15 caddc class +
16 10 cv setvar t
17 cmul class ×
18 7 cv setvar b
19 cmin class
20 18 14 19 co class b a
21 16 20 17 co class t b a
22 14 21 15 co class a + t b a
23 13 22 wceq wff x = a + t b a
24 8 cv setvar c
25 12 cv setvar r
26 9 cv setvar d
27 26 24 19 co class d c
28 25 27 17 co class r d c
29 24 28 15 co class c + r d c
30 13 29 wceq wff x = c + r d c
31 cim class
32 ccj class *
33 20 32 cfv class b a
34 33 27 17 co class b a d c
35 34 31 cfv class b a d c
36 cc0 class 0
37 35 36 wne wff b a d c 0
38 23 30 37 w3a wff x = a + t b a x = c + r d c b a d c 0
39 38 12 11 wrex wff r x = a + t b a x = c + r d c b a d c 0
40 39 10 11 wrex wff t r x = a + t b a x = c + r d c b a d c 0
41 40 9 6 wrex wff d s t r x = a + t b a x = c + r d c b a d c 0
42 41 8 6 wrex wff c s d s t r x = a + t b a x = c + r d c b a d c 0
43 42 7 6 wrex wff b s c s d s t r x = a + t b a x = c + r d c b a d c 0
44 43 5 6 wrex wff a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0
45 ve setvar e
46 vf setvar f
47 cabs class abs
48 13 24 19 co class x c
49 48 47 cfv class x c
50 45 cv setvar e
51 46 cv setvar f
52 50 51 19 co class e f
53 52 47 cfv class e f
54 49 53 wceq wff x c = e f
55 23 54 wa wff x = a + t b a x c = e f
56 55 10 11 wrex wff t x = a + t b a x c = e f
57 56 46 6 wrex wff f s t x = a + t b a x c = e f
58 57 45 6 wrex wff e s f s t x = a + t b a x c = e f
59 58 8 6 wrex wff c s e s f s t x = a + t b a x c = e f
60 59 7 6 wrex wff b s c s e s f s t x = a + t b a x c = e f
61 60 5 6 wrex wff a s b s c s e s f s t x = a + t b a x c = e f
62 14 26 wne wff a d
63 13 14 19 co class x a
64 63 47 cfv class x a
65 18 24 19 co class b c
66 65 47 cfv class b c
67 64 66 wceq wff x a = b c
68 13 26 19 co class x d
69 68 47 cfv class x d
70 69 53 wceq wff x d = e f
71 62 67 70 w3a wff a d x a = b c x d = e f
72 71 46 6 wrex wff f s a d x a = b c x d = e f
73 72 45 6 wrex wff e s f s a d x a = b c x d = e f
74 73 9 6 wrex wff d s e s f s a d x a = b c x d = e f
75 74 8 6 wrex wff c s d s e s f s a d x a = b c x d = e f
76 75 7 6 wrex wff b s c s d s e s f s a d x a = b c x d = e f
77 76 5 6 wrex wff a s b s c s d s e s f s a d x a = b c x d = e f
78 44 61 77 w3o wff a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f
79 78 3 4 crab class x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f
80 1 2 79 cmpt class s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f
81 c1 class 1
82 36 81 cpr class 0 1
83 80 82 crdg class rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1
84 com class ω
85 83 84 cima class rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1 ω
86 0 85 wceq wff Constr = rec s V x | a s b s c s d s t r x = a + t b a x = c + r d c b a d c 0 a s b s c s e s f s t x = a + t b a x c = e f a s b s c s d s e s f s a d x a = b c x d = e f 0 1 ω