constrlccllem

Description: Constructible numbers are closed under line-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\})$
	constrlccllem.a	$⊢ φ \to A \in Constr$
	constrlccllem.b	$⊢ φ \to B \in Constr$
	constrlccllem.c	$⊢ φ \to G \in Constr$
	constrlccllem.e	$⊢ φ \to E \in Constr$
	constrlccllem.f	$⊢ φ \to F \in Constr$
	constrlccllem.t	$⊢ φ \to T \in ℝ$
	constrlccllem.x	$⊢ φ \to X \in ℂ$
	constrlccllem.1	$⊢ φ \to X = A + T (B - A)$
	constrlccllem.2	$⊢ φ \to \|X - G\| = \|E - F\|$
Assertion	constrlccllem	$⊢ φ \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		constrlccllem.a	$⊢ φ \to A \in Constr$
3		constrlccllem.b	$⊢ φ \to B \in Constr$
4		constrlccllem.c	$⊢ φ \to G \in Constr$
5		constrlccllem.e	$⊢ φ \to E \in Constr$
6		constrlccllem.f	$⊢ φ \to F \in Constr$
7		constrlccllem.t	$⊢ φ \to T \in ℝ$
8		constrlccllem.x	$⊢ φ \to X \in ℂ$
9		constrlccllem.1	$⊢ φ \to X = A + T (B - A)$
10		constrlccllem.2	$⊢ φ \to \|X - G\| = \|E - F\|$
11		peano2b	$⊢ n \in ω \leftrightarrow suc n \in ω$
12	11	biimpi	$⊢ n \in ω \to suc n \in ω$
13	12	ad2antlr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to suc n \in ω$
14		fveq2	$⊢ m = suc n \to C (m) = C (suc n)$
15	14	eleq2d	$⊢ m = suc n \to (X \in C (m) \leftrightarrow X \in C (suc n))$
16	15	adantl	$⊢ (((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \land m = suc n) \to (X \in C (m) \leftrightarrow X \in C (suc n))$
17	8	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to X \in ℂ$
18		id	$⊢ a = A \to a = A$
19		oveq2	$⊢ a = A \to b - a = b - A$
20	19	oveq2d	$⊢ a = A \to t (b - a) = t (b - A)$
21	18 20	oveq12d	$⊢ a = A \to a + t (b - a) = A + t (b - A)$
22	21	eqeq2d	$⊢ a = A \to (X = a + t (b - a) \leftrightarrow X = A + t (b - A))$
23	22	anbi1d	$⊢ a = A \to ((X = a + t (b - a) \land \|X - c\| = \|e - f\|) \leftrightarrow (X = A + t (b - A) \land \|X - c\| = \|e - f\|))$
24	23	rexbidv	$⊢ a = A \to (\exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|) \leftrightarrow \exists t \in ℝ (X = A + t (b - A) \land \|X - c\| = \|e - f\|))$
25	24	2rexbidv	$⊢ a = A \to (\exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = a + t (b - a) \land \|X - c\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = A + t (b - A) \land \|X - c\| = \|e - f\|))$
26		oveq1	$⊢ b = B \to b - A = B - A$
27	26	oveq2d	$⊢ b = B \to t (b - A) = t (B - A)$
28	27	oveq2d	$⊢ b = B \to A + t (b - A) = A + t (B - A)$
29	28	eqeq2d	$⊢ b = B \to (X = A + t (b - A) \leftrightarrow X = A + t (B - A))$
30	29	anbi1d	$⊢ b = B \to ((X = A + t (b - A) \land \|X - c\| = \|e - f\|) \leftrightarrow (X = A + t (B - A) \land \|X - c\| = \|e - f\|))$
31	30	rexbidv	$⊢ b = B \to (\exists t \in ℝ (X = A + t (b - A) \land \|X - c\| = \|e - f\|) \leftrightarrow \exists t \in ℝ (X = A + t (B - A) \land \|X - c\| = \|e - f\|))$
32	31	2rexbidv	$⊢ b = B \to (\exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = A + t (b - A) \land \|X - c\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = A + t (B - A) \land \|X - c\| = \|e - f\|))$
33		oveq2	$⊢ c = G \to X - c = X - G$
34	33	fveq2d	$⊢ c = G \to \|X - c\| = \|X - G\|$
35	34	eqeq1d	$⊢ c = G \to (\|X - c\| = \|e - f\| \leftrightarrow \|X - G\| = \|e - f\|)$
36	35	anbi2d	$⊢ c = G \to ((X = A + t (B - A) \land \|X - c\| = \|e - f\|) \leftrightarrow (X = A + t (B - A) \land \|X - G\| = \|e - f\|))$
37	36	rexbidv	$⊢ c = G \to (\exists t \in ℝ (X = A + t (B - A) \land \|X - c\| = \|e - f\|) \leftrightarrow \exists t \in ℝ (X = A + t (B - A) \land \|X - G\| = \|e - f\|))$
38	37	2rexbidv	$⊢ c = G \to (\exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = A + t (B - A) \land \|X - c\| = \|e - f\|) \leftrightarrow \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = A + t (B - A) \land \|X - G\| = \|e - f\|))$
39	2	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to A \in Constr$
40		simpr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to \{A, B, G\} \cup \{E, F\} \subseteq C (n)$
41	40	unssad	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to \{A, B, G\} \subseteq C (n)$
42	39 41	tpssad	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to A \in C (n)$
43	3	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to B \in Constr$
44	43 41	tpssbd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to B \in C (n)$
45	4	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to G \in Constr$
46	45 41	tpsscd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to G \in C (n)$
47		oveq1	$⊢ e = E \to e - f = E - f$
48	47	fveq2d	$⊢ e = E \to \|e - f\| = \|E - f\|$
49	48	eqeq2d	$⊢ e = E \to (\|X - G\| = \|e - f\| \leftrightarrow \|X - G\| = \|E - f\|)$
50	49	anbi2d	$⊢ e = E \to ((X = A + t (B - A) \land \|X - G\| = \|e - f\|) \leftrightarrow (X = A + t (B - A) \land \|X - G\| = \|E - f\|))$
51		oveq2	$⊢ f = F \to E - f = E - F$
52	51	fveq2d	$⊢ f = F \to \|E - f\| = \|E - F\|$
53	52	eqeq2d	$⊢ f = F \to (\|X - G\| = \|E - f\| \leftrightarrow \|X - G\| = \|E - F\|)$
54	53	anbi2d	$⊢ f = F \to ((X = A + t (B - A) \land \|X - G\| = \|E - f\|) \leftrightarrow (X = A + t (B - A) \land \|X - G\| = \|E - F\|))$
55		oveq1	$⊢ t = T \to t (B - A) = T (B - A)$
56	55	oveq2d	$⊢ t = T \to A + t (B - A) = A + T (B - A)$
57	56	eqeq2d	$⊢ t = T \to (X = A + t (B - A) \leftrightarrow X = A + T (B - A))$
58	57	anbi1d	$⊢ t = T \to ((X = A + t (B - A) \land \|X - G\| = \|E - F\|) \leftrightarrow (X = A + T (B - A) \land \|X - G\| = \|E - F\|))$
59	5	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to E \in Constr$
60	40	unssbd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to \{E, F\} \subseteq C (n)$
61	59 60	prssad	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to E \in C (n)$
62	6	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to F \in Constr$
63	62 60	prssbd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to F \in C (n)$
64	7	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to T \in ℝ$
65	9	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to X = A + T (B - A)$
66	10	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to \|X - G\| = \|E - F\|$
67	65 66	jca	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to (X = A + T (B - A) \land \|X - G\| = \|E - F\|)$
68	50 54 58 61 63 64 67	3rspcedvdw	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to \exists e \in C (n) \exists f \in C (n) \exists t \in ℝ (X = A + t (B - A) \land \|X - G\| = \|e - f\|)$
69	25 32 38 42 44 46 68	3rspcedvdw	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to \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\|)$
70	69	3mix2d	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{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\|))$
71		nnon	$⊢ n \in ω \to n \in On$
72	71	ad2antlr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to n \in On$
73		eqid	$⊢ C (n) = C (n)$
74	1 72 73	constrsuc	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{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\|))))$
75	17 70 74	mpbir2and	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to X \in C (suc n)$
76	13 16 75	rspcedvd	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to \exists m \in ω X \in C (m)$
77	1	isconstr	$⊢ X \in Constr \leftrightarrow \exists m \in ω X \in C (m)$
78	76 77	sylibr	$⊢ ((φ \land n \in ω) \land \{A, B, G\} \cup \{E, F\} \subseteq C (n)) \to X \in Constr$
79	2 3 4	tpssd	$⊢ φ \to \{A, B, G\} \subseteq Constr$
80	5 6	prssd	$⊢ φ \to \{E, F\} \subseteq Constr$
81	79 80	unssd	$⊢ φ \to \{A, B, G\} \cup \{E, F\} \subseteq Constr$
82		tpfi	$⊢ \{A, B, G\} \in Fin$
83	82	a1i	$⊢ φ \to \{A, B, G\} \in Fin$
84		prfi	$⊢ \{E, F\} \in Fin$
85	84	a1i	$⊢ φ \to \{E, F\} \in Fin$
86	83 85	unfid	$⊢ φ \to \{A, B, G\} \cup \{E, F\} \in Fin$
87	1 81 86	constrfiss	$⊢ φ \to \exists n \in ω \{A, B, G\} \cup \{E, F\} \subseteq C (n)$
88	78 87	r19.29a	$⊢ φ \to X \in Constr$

Metamath Proof Explorer

Theorem constrlccllem

Proof