constrcccllem

Description: Constructible numbers are closed under circle-circle intersections. (Contributed by Thierry Arnoux, 2-Nov-2025)

	Ref	Expression
Hypotheses	constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
	constrcccllem.a	$⊢ φ \to A \in Constr$
	constrcccllem.b	$⊢ φ \to B \in Constr$
	constrcccllem.c	$⊢ φ \to G \in Constr$
	constrcccllem.d	$⊢ φ \to D \in Constr$
	constrcccllem.e	$⊢ φ \to E \in Constr$
	constrcccllem.f	$⊢ φ \to F \in Constr$
	constrcccllem.x	$⊢ φ \to X \in ℂ$
	constrcccllem.1	$⊢ φ \to A \neq D$
	constrcccllem.2	$⊢ φ \to \|X - A\| = \|B - G\|$
	constrcccllem.3	$⊢ φ \to \|X - D\| = \|E - F\|$
Assertion	constrcccllem	$⊢ φ \to X \in Constr$

Proof

Step	Hyp	Ref	Expression
1		constr0.1	$⊢ C = rec ((s \in V ⟼ \{x \in ℂ \| (\exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists t \in ℝ \exists r \in ℝ (x = a + t (b - a) \land x = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in s \exists b \in s \exists c \in s \exists e \in s \exists f \in s \exists t \in ℝ (x = a + t (b - a) \land \|x - c\| = \|e - f\|) \lor \exists a \in s \exists b \in s \exists c \in s \exists d \in s \exists e \in s \exists f \in s (a \neq d \land \|x - a\| = \|b - c\| \land \|x - d\| = \|e - f\|))\}), \{0, 1\})$
2		constrcccllem.a	$⊢ φ \to A \in Constr$
3		constrcccllem.b	$⊢ φ \to B \in Constr$
4		constrcccllem.c	$⊢ φ \to G \in Constr$
5		constrcccllem.d	$⊢ φ \to D \in Constr$
6		constrcccllem.e	$⊢ φ \to E \in Constr$
7		constrcccllem.f	$⊢ φ \to F \in Constr$
8		constrcccllem.x	$⊢ φ \to X \in ℂ$
9		constrcccllem.1	$⊢ φ \to A \neq D$
10		constrcccllem.2	$⊢ φ \to \|X - A\| = \|B - G\|$
11		constrcccllem.3	$⊢ φ \to \|X - D\| = \|E - F\|$
12		peano2b	$⊢ n \in ω \leftrightarrow suc n \in ω$
13	12	biimpi	$⊢ n \in ω \to suc n \in ω$
14	13	ad2antlr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to suc n \in ω$
15		fveq2	$⊢ m = suc n \to C (m) = C (suc n)$
16	15	eleq2d	$⊢ m = suc n \to (X \in C (m) \leftrightarrow X \in C (suc n))$
17	16	adantl	$⊢ (((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \land m = suc n) \to (X \in C (m) \leftrightarrow X \in C (suc n))$
18	8	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to X \in ℂ$
19		neeq1	$⊢ a = A \to (a \neq d \leftrightarrow A \neq d)$
20		oveq2	$⊢ a = A \to X - a = X - A$
21	20	fveq2d	$⊢ a = A \to \|X - a\| = \|X - A\|$
22	21	eqeq1d	$⊢ a = A \to (\|X - a\| = \|b - c\| \leftrightarrow \|X - A\| = \|b - c\|)$
23	19 22	3anbi12d	$⊢ a = A \to ((a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow (A \neq d \land \|X - A\| = \|b - c\| \land \|X - d\| = \|e - f\|))$
24	23	rexbidv	$⊢ a = A \to (\exists f \in C (n) (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow \exists f \in C (n) (A \neq d \land \|X - A\| = \|b - c\| \land \|X - d\| = \|e - f\|))$
25	24	2rexbidv	$⊢ a = A \to (\exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (A \neq d \land \|X - A\| = \|b - c\| \land \|X - d\| = \|e - f\|))$
26		oveq1	$⊢ b = B \to b - c = B - c$
27	26	fveq2d	$⊢ b = B \to \|b - c\| = \|B - c\|$
28	27	eqeq2d	$⊢ b = B \to (\|X - A\| = \|b - c\| \leftrightarrow \|X - A\| = \|B - c\|)$
29	28	3anbi2d	$⊢ b = B \to ((A \neq d \land \|X - A\| = \|b - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow (A \neq d \land \|X - A\| = \|B - c\| \land \|X - d\| = \|e - f\|))$
30	29	rexbidv	$⊢ b = B \to (\exists f \in C (n) (A \neq d \land \|X - A\| = \|b - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow \exists f \in C (n) (A \neq d \land \|X - A\| = \|B - c\| \land \|X - d\| = \|e - f\|))$
31	30	2rexbidv	$⊢ b = B \to (\exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (A \neq d \land \|X - A\| = \|b - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (A \neq d \land \|X - A\| = \|B - c\| \land \|X - d\| = \|e - f\|))$
32		oveq2	$⊢ c = G \to B - c = B - G$
33	32	fveq2d	$⊢ c = G \to \|B - c\| = \|B - G\|$
34	33	eqeq2d	$⊢ c = G \to (\|X - A\| = \|B - c\| \leftrightarrow \|X - A\| = \|B - G\|)$
35	34	3anbi2d	$⊢ c = G \to ((A \neq d \land \|X - A\| = \|B - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow (A \neq d \land \|X - A\| = \|B - G\| \land \|X - d\| = \|e - f\|))$
36	35	rexbidv	$⊢ c = G \to (\exists f \in C (n) (A \neq d \land \|X - A\| = \|B - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow \exists f \in C (n) (A \neq d \land \|X - A\| = \|B - G\| \land \|X - d\| = \|e - f\|))$
37	36	2rexbidv	$⊢ c = G \to (\exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (A \neq d \land \|X - A\| = \|B - c\| \land \|X - d\| = \|e - f\|) \leftrightarrow \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (A \neq d \land \|X - A\| = \|B - G\| \land \|X - d\| = \|e - f\|))$
38	2	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to A \in Constr$
39		simpr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)$
40	39	unssad	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \{A, B, G\} \subseteq C (n)$
41	38 40	tpssad	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to A \in C (n)$
42	3	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to B \in Constr$
43	42 40	tpssbd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to B \in C (n)$
44	4	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to G \in Constr$
45	44 40	tpsscd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to G \in C (n)$
46		neeq2	$⊢ d = D \to (A \neq d \leftrightarrow A \neq D)$
47		oveq2	$⊢ d = D \to X - d = X - D$
48	47	fveq2d	$⊢ d = D \to \|X - d\| = \|X - D\|$
49	48	eqeq1d	$⊢ d = D \to (\|X - d\| = \|e - f\| \leftrightarrow \|X - D\| = \|e - f\|)$
50	46 49	3anbi13d	$⊢ d = D \to ((A \neq d \land \|X - A\| = \|B - G\| \land \|X - d\| = \|e - f\|) \leftrightarrow (A \neq D \land \|X - A\| = \|B - G\| \land \|X - D\| = \|e - f\|))$
51		oveq1	$⊢ e = E \to e - f = E - f$
52	51	fveq2d	$⊢ e = E \to \|e - f\| = \|E - f\|$
53	52	eqeq2d	$⊢ e = E \to (\|X - D\| = \|e - f\| \leftrightarrow \|X - D\| = \|E - f\|)$
54	53	3anbi3d	$⊢ e = E \to ((A \neq D \land \|X - A\| = \|B - G\| \land \|X - D\| = \|e - f\|) \leftrightarrow (A \neq D \land \|X - A\| = \|B - G\| \land \|X - D\| = \|E - f\|))$
55		oveq2	$⊢ f = F \to E - f = E - F$
56	55	fveq2d	$⊢ f = F \to \|E - f\| = \|E - F\|$
57	56	eqeq2d	$⊢ f = F \to (\|X - D\| = \|E - f\| \leftrightarrow \|X - D\| = \|E - F\|)$
58	57	3anbi3d	$⊢ f = F \to ((A \neq D \land \|X - A\| = \|B - G\| \land \|X - D\| = \|E - f\|) \leftrightarrow (A \neq D \land \|X - A\| = \|B - G\| \land \|X - D\| = \|E - F\|))$
59	5	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to D \in Constr$
60	39	unssbd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \{D, E, F\} \subseteq C (n)$
61	59 60	tpssad	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to D \in C (n)$
62	6	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to E \in Constr$
63	62 60	tpssbd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to E \in C (n)$
64	7	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to F \in Constr$
65	64 60	tpsscd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to F \in C (n)$
66	9	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to A \neq D$
67	10	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \|X - A\| = \|B - G\|$
68	11	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \|X - D\| = \|E - F\|$
69	66 67 68	3jca	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to (A \neq D \land \|X - A\| = \|B - G\| \land \|X - D\| = \|E - F\|)$
70	50 54 58 61 63 65 69	3rspcedvdw	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (A \neq d \land \|X - A\| = \|B - G\| \land \|X - d\| = \|e - f\|)$
71	25 31 37 41 43 45 70	3rspcedvdw	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|)$
72	71	3mix3d	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (X = a + t (b - a) \land X = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|))$
73		nnon	$⊢ n \in ω \to n \in On$
74	73	ad2antlr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to n \in On$
75		eqid	$⊢ C (n) = C (n)$
76	1 74 75	constrsuc	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to (X \in C (suc n) \leftrightarrow (X \in ℂ \land (\exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (X = a + t (b - a) \land X = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|) \lor \exists a \in C (n) \exists b \in C (n) \exists c \in C (n) \exists d \in C (n) \exists e \in C (n) \exists f \in C (n) (a \neq d \land \|X - a\| = \|b - c\| \land \|X - d\| = \|e - f\|))))$
77	18 72 76	mpbir2and	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to X \in C (suc n)$
78	14 17 77	rspcedvd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to \exists m \in ω X \in C (m)$
79	1	isconstr	$⊢ X \in Constr \leftrightarrow \exists m \in ω X \in C (m)$
80	78 79	sylibr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)) \to X \in Constr$
81	2 3 4	tpssd	$⊢ φ \to \{A, B, G\} \subseteq Constr$
82	5 6 7	tpssd	$⊢ φ \to \{D, E, F\} \subseteq Constr$
83	81 82	unssd	$⊢ φ \to \{A, B, G\} \cup \{D, E, F\} \subseteq Constr$
84		tpfi	$⊢ \{A, B, G\} \in Fin$
85	84	a1i	$⊢ φ \to \{A, B, G\} \in Fin$
86		tpfi	$⊢ \{D, E, F\} \in Fin$
87	86	a1i	$⊢ φ \to \{D, E, F\} \in Fin$
88	85 87	unfid	$⊢ φ \to \{A, B, G\} \cup \{D, E, F\} \in Fin$
89	1 83 88	constrfiss	$⊢ φ \to \exists n \in ω \{A, B, G\} \cup \{D, E, F\} \subseteq C (n)$
90	80 89	r19.29a	$⊢ φ \to X \in Constr$

Metamath Proof Explorer

Theorem constrcccllem

Proof