constrllcllem

Description: Constructible numbers are closed under line-line 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\})$
	constrllcllem.a	$⊢ φ \to A \in Constr$
	constrllcllem.b	$⊢ φ \to B \in Constr$
	constrllcllem.c	$⊢ φ \to G \in Constr$
	constrllcllem.e	$⊢ φ \to D \in Constr$
	constrllcllem.t	$⊢ φ \to T \in ℝ$
	constrllcllem.r	$⊢ φ \to R \in ℝ$
	constrllcllem.x	$⊢ φ \to X \in ℂ$
	constrllcllem.1	$⊢ φ \to X = A + T (B - A)$
	constrllcllem.2	$⊢ φ \to X = G + R (D - G)$
	constrllcllem.3	$⊢ φ \to ℑ (\overline{B - A} (D - G)) \neq 0$
Assertion	constrllcllem	$⊢ φ \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		constrllcllem.a	$⊢ φ \to A \in Constr$
3		constrllcllem.b	$⊢ φ \to B \in Constr$
4		constrllcllem.c	$⊢ φ \to G \in Constr$
5		constrllcllem.e	$⊢ φ \to D \in Constr$
6		constrllcllem.t	$⊢ φ \to T \in ℝ$
7		constrllcllem.r	$⊢ φ \to R \in ℝ$
8		constrllcllem.x	$⊢ φ \to X \in ℂ$
9		constrllcllem.1	$⊢ φ \to X = A + T (B - A)$
10		constrllcllem.2	$⊢ φ \to X = G + R (D - G)$
11		constrllcllem.3	$⊢ φ \to ℑ (\overline{B - A} (D - G)) \neq 0$
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\} \cup \{G, D\} \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\} \cup \{G, D\} \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\} \cup \{G, D\} \subseteq C (n)) \to X \in ℂ$
19		id	$⊢ a = A \to a = A$
20		oveq2	$⊢ a = A \to b - a = b - A$
21	20	oveq2d	$⊢ a = A \to t (b - a) = t (b - A)$
22	19 21	oveq12d	$⊢ a = A \to a + t (b - a) = A + t (b - A)$
23	22	eqeq2d	$⊢ a = A \to (X = a + t (b - a) \leftrightarrow X = A + t (b - A))$
24	20	fveq2d	$⊢ a = A \to \overline{b - a} = \overline{b - A}$
25	24	oveq1d	$⊢ a = A \to \overline{b - a} (d - c) = \overline{b - A} (d - c)$
26	25	fveq2d	$⊢ a = A \to ℑ (\overline{b - a} (d - c)) = ℑ (\overline{b - A} (d - c))$
27	26	neeq1d	$⊢ a = A \to (ℑ (\overline{b - a} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{b - A} (d - c)) \neq 0)$
28	23 27	3anbi13d	$⊢ a = A \to ((X = a + t (b - a) \land X = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow (X = A + t (b - A) \land X = c + r (d - c) \land ℑ (\overline{b - A} (d - c)) \neq 0))$
29	28	rexbidv	$⊢ a = A \to (\exists r \in ℝ (X = a + t (b - a) \land X = c + r (d - c) \land ℑ (\overline{b - a} (d - c)) \neq 0) \leftrightarrow \exists r \in ℝ (X = A + t (b - A) \land X = c + r (d - c) \land ℑ (\overline{b - A} (d - c)) \neq 0))$
30	29	2rexbidv	$⊢ a = A \to (\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) \leftrightarrow \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))$
31		oveq1	$⊢ b = B \to b - A = B - A$
32	31	oveq2d	$⊢ b = B \to t (b - A) = t (B - A)$
33	32	oveq2d	$⊢ b = B \to A + t (b - A) = A + t (B - A)$
34	33	eqeq2d	$⊢ b = B \to (X = A + t (b - A) \leftrightarrow X = A + t (B - A))$
35	31	fveq2d	$⊢ b = B \to \overline{b - A} = \overline{B - A}$
36	35	oveq1d	$⊢ b = B \to \overline{b - A} (d - c) = \overline{B - A} (d - c)$
37	36	fveq2d	$⊢ b = B \to ℑ (\overline{b - A} (d - c)) = ℑ (\overline{B - A} (d - c))$
38	37	neeq1d	$⊢ b = B \to (ℑ (\overline{b - A} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{B - A} (d - c)) \neq 0)$
39	34 38	3anbi13d	$⊢ b = B \to ((X = A + t (b - A) \land X = c + r (d - c) \land ℑ (\overline{b - A} (d - c)) \neq 0) \leftrightarrow (X = A + t (B - A) \land X = c + r (d - c) \land ℑ (\overline{B - A} (d - c)) \neq 0))$
40	39	rexbidv	$⊢ b = B \to (\exists r \in ℝ (X = A + t (b - A) \land X = c + r (d - c) \land ℑ (\overline{b - A} (d - c)) \neq 0) \leftrightarrow \exists r \in ℝ (X = A + t (B - A) \land X = c + r (d - c) \land ℑ (\overline{B - A} (d - c)) \neq 0))$
41	40	2rexbidv	$⊢ b = B \to (\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) \leftrightarrow \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))$
42		id	$⊢ c = G \to c = G$
43		oveq2	$⊢ c = G \to d - c = d - G$
44	43	oveq2d	$⊢ c = G \to r (d - c) = r (d - G)$
45	42 44	oveq12d	$⊢ c = G \to c + r (d - c) = G + r (d - G)$
46	45	eqeq2d	$⊢ c = G \to (X = c + r (d - c) \leftrightarrow X = G + r (d - G))$
47	43	oveq2d	$⊢ c = G \to \overline{B - A} (d - c) = \overline{B - A} (d - G)$
48	47	fveq2d	$⊢ c = G \to ℑ (\overline{B - A} (d - c)) = ℑ (\overline{B - A} (d - G))$
49	48	neeq1d	$⊢ c = G \to (ℑ (\overline{B - A} (d - c)) \neq 0 \leftrightarrow ℑ (\overline{B - A} (d - G)) \neq 0)$
50	46 49	3anbi23d	$⊢ c = G \to ((X = A + t (B - A) \land X = c + r (d - c) \land ℑ (\overline{B - A} (d - c)) \neq 0) \leftrightarrow (X = A + t (B - A) \land X = G + r (d - G) \land ℑ (\overline{B - A} (d - G)) \neq 0))$
51	50	rexbidv	$⊢ c = G \to (\exists r \in ℝ (X = A + t (B - A) \land X = c + r (d - c) \land ℑ (\overline{B - A} (d - c)) \neq 0) \leftrightarrow \exists r \in ℝ (X = A + t (B - A) \land X = G + r (d - G) \land ℑ (\overline{B - A} (d - G)) \neq 0))$
52	51	2rexbidv	$⊢ c = G \to (\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) \leftrightarrow \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (X = A + t (B - A) \land X = G + r (d - G) \land ℑ (\overline{B - A} (d - G)) \neq 0))$
53	2	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to A \in Constr$
54		simpr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to \{A, B\} \cup \{G, D\} \subseteq C (n)$
55	54	unssad	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to \{A, B\} \subseteq C (n)$
56	53 55	prssad	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to A \in C (n)$
57	3	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to B \in Constr$
58	57 55	prssbd	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to B \in C (n)$
59	4	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to G \in Constr$
60	54	unssbd	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to \{G, D\} \subseteq C (n)$
61	59 60	prssad	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to G \in C (n)$
62		oveq1	$⊢ d = D \to d - G = D - G$
63	62	oveq2d	$⊢ d = D \to r (d - G) = r (D - G)$
64	63	oveq2d	$⊢ d = D \to G + r (d - G) = G + r (D - G)$
65	64	eqeq2d	$⊢ d = D \to (X = G + r (d - G) \leftrightarrow X = G + r (D - G))$
66	62	oveq2d	$⊢ d = D \to \overline{B - A} (d - G) = \overline{B - A} (D - G)$
67	66	fveq2d	$⊢ d = D \to ℑ (\overline{B - A} (d - G)) = ℑ (\overline{B - A} (D - G))$
68	67	neeq1d	$⊢ d = D \to (ℑ (\overline{B - A} (d - G)) \neq 0 \leftrightarrow ℑ (\overline{B - A} (D - G)) \neq 0)$
69	65 68	3anbi23d	$⊢ d = D \to ((X = A + t (B - A) \land X = G + r (d - G) \land ℑ (\overline{B - A} (d - G)) \neq 0) \leftrightarrow (X = A + t (B - A) \land X = G + r (D - G) \land ℑ (\overline{B - A} (D - G)) \neq 0))$
70		oveq1	$⊢ t = T \to t (B - A) = T (B - A)$
71	70	oveq2d	$⊢ t = T \to A + t (B - A) = A + T (B - A)$
72	71	eqeq2d	$⊢ t = T \to (X = A + t (B - A) \leftrightarrow X = A + T (B - A))$
73	72	3anbi1d	$⊢ t = T \to ((X = A + t (B - A) \land X = G + r (D - G) \land ℑ (\overline{B - A} (D - G)) \neq 0) \leftrightarrow (X = A + T (B - A) \land X = G + r (D - G) \land ℑ (\overline{B - A} (D - G)) \neq 0))$
74		oveq1	$⊢ r = R \to r (D - G) = R (D - G)$
75	74	oveq2d	$⊢ r = R \to G + r (D - G) = G + R (D - G)$
76	75	eqeq2d	$⊢ r = R \to (X = G + r (D - G) \leftrightarrow X = G + R (D - G))$
77	76	3anbi2d	$⊢ r = R \to ((X = A + T (B - A) \land X = G + r (D - G) \land ℑ (\overline{B - A} (D - G)) \neq 0) \leftrightarrow (X = A + T (B - A) \land X = G + R (D - G) \land ℑ (\overline{B - A} (D - G)) \neq 0))$
78	5	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to D \in Constr$
79	78 60	prssbd	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to D \in C (n)$
80	6	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to T \in ℝ$
81	7	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to R \in ℝ$
82	9	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to X = A + T (B - A)$
83	10	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to X = G + R (D - G)$
84	11	ad2antrr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to ℑ (\overline{B - A} (D - G)) \neq 0$
85	82 83 84	3jca	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to (X = A + T (B - A) \land X = G + R (D - G) \land ℑ (\overline{B - A} (D - G)) \neq 0)$
86	69 73 77 79 80 81 85	3rspcedvdw	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to \exists d \in C (n) \exists t \in ℝ \exists r \in ℝ (X = A + t (B - A) \land X = G + r (d - G) \land ℑ (\overline{B - A} (d - G)) \neq 0)$
87	30 41 52 56 58 61 86	3rspcedvdw	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \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)$
88	87	3mix1d	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \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\|))$
89		nnon	$⊢ n \in ω \to n \in On$
90	89	ad2antlr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to n \in On$
91		eqid	$⊢ C (n) = C (n)$
92	1 90 91	constrsuc	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \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\|))))$
93	18 88 92	mpbir2and	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to X \in C (suc n)$
94	14 17 93	rspcedvd	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to \exists m \in ω X \in C (m)$
95	1	isconstr	$⊢ X \in Constr \leftrightarrow \exists m \in ω X \in C (m)$
96	94 95	sylibr	$⊢ ((φ \land n \in ω) \land \{A, B\} \cup \{G, D\} \subseteq C (n)) \to X \in Constr$
97	2 3	prssd	$⊢ φ \to \{A, B\} \subseteq Constr$
98	4 5	prssd	$⊢ φ \to \{G, D\} \subseteq Constr$
99	97 98	unssd	$⊢ φ \to \{A, B\} \cup \{G, D\} \subseteq Constr$
100		prfi	$⊢ \{A, B\} \in Fin$
101	100	a1i	$⊢ φ \to \{A, B\} \in Fin$
102		prfi	$⊢ \{G, D\} \in Fin$
103	102	a1i	$⊢ φ \to \{G, D\} \in Fin$
104	101 103	unfid	$⊢ φ \to \{A, B\} \cup \{G, D\} \in Fin$
105	1 99 104	constrfiss	$⊢ φ \to \exists n \in ω \{A, B\} \cup \{G, D\} \subseteq C (n)$
106	96 105	r19.29a	$⊢ φ \to X \in Constr$

Metamath Proof Explorer

Theorem constrllcllem

Proof