constrrtll

Description: In the construction of constructible numbers, line-line intersections are solutions of linear equations, and can therefore be completely constructed. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	constrrtll.s	$⊢ φ \to S \subseteq ℂ$
	constrrtll.a	$⊢ φ \to A \in S$
	constrrtll.b	$⊢ φ \to B \in S$
	constrrtll.c	$⊢ φ \to C \in S$
	constrrtll.d	$⊢ φ \to D \in S$
	constrrtll.t	$⊢ φ \to T \in ℝ$
	constrrtll.r	$⊢ φ \to R \in ℝ$
	constrrtll.1	$⊢ φ \to X = A + T (B - A)$
	constrrtll.2	$⊢ φ \to X = C + R (D - C)$
	constrrtll.3	$⊢ φ \to ℑ (\overline{B - A} (D - C)) \neq 0$
	constrrtll.n	$⊢ N = A + (\frac{(A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)}{(\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})}) (B - A)$
Assertion	constrrtll	$⊢ φ \to X = N$

Proof

Step	Hyp	Ref	Expression
1		constrrtll.s	$⊢ φ \to S \subseteq ℂ$
2		constrrtll.a	$⊢ φ \to A \in S$
3		constrrtll.b	$⊢ φ \to B \in S$
4		constrrtll.c	$⊢ φ \to C \in S$
5		constrrtll.d	$⊢ φ \to D \in S$
6		constrrtll.t	$⊢ φ \to T \in ℝ$
7		constrrtll.r	$⊢ φ \to R \in ℝ$
8		constrrtll.1	$⊢ φ \to X = A + T (B - A)$
9		constrrtll.2	$⊢ φ \to X = C + R (D - C)$
10		constrrtll.3	$⊢ φ \to ℑ (\overline{B - A} (D - C)) \neq 0$
11		constrrtll.n	$⊢ N = A + (\frac{(A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)}{(\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})}) (B - A)$
12	6	recnd	$⊢ φ \to T \in ℂ$
13	1 3	sseldd	$⊢ φ \to B \in ℂ$
14	1 2	sseldd	$⊢ φ \to A \in ℂ$
15	13 14	cjsubd	$⊢ φ \to \overline{B - A} = \overline{B} - \overline{A}$
16	13 14	subcld	$⊢ φ \to B - A \in ℂ$
17	16	cjcld	$⊢ φ \to \overline{B - A} \in ℂ$
18	15 17	eqeltrrd	$⊢ φ \to \overline{B} - \overline{A} \in ℂ$
19	1 5	sseldd	$⊢ φ \to D \in ℂ$
20	1 4	sseldd	$⊢ φ \to C \in ℂ$
21	19 20	subcld	$⊢ φ \to D - C \in ℂ$
22	18 21	mulcld	$⊢ φ \to (\overline{B} - \overline{A}) (D - C) \in ℂ$
23	19 20	cjsubd	$⊢ φ \to \overline{D - C} = \overline{D} - \overline{C}$
24	21	cjcld	$⊢ φ \to \overline{D - C} \in ℂ$
25	23 24	eqeltrrd	$⊢ φ \to \overline{D} - \overline{C} \in ℂ$
26	16 25	mulcld	$⊢ φ \to (B - A) (\overline{D} - \overline{C}) \in ℂ$
27	12 22 26	subdid	$⊢ φ \to T ((\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})) = T (\overline{B} - \overline{A}) (D - C) - T (B - A) (\overline{D} - \overline{C})$
28	8	oveq1d	$⊢ φ \to X - C = A + T (B - A) - C$
29	7	recnd	$⊢ φ \to R \in ℂ$
30	29 21	mulcld	$⊢ φ \to R (D - C) \in ℂ$
31	20 30 9	mvrladdd	$⊢ φ \to X - C = R (D - C)$
32	28 31	eqtr3d	$⊢ φ \to A + T (B - A) - C = R (D - C)$
33	32 30	eqeltrd	$⊢ φ \to A + T (B - A) - C \in ℂ$
34		fveq2	$⊢ \overline{B - A} (D - C) = 0 \to ℑ (\overline{B - A} (D - C)) = ℑ (0)$
35		im0	$⊢ ℑ (0) = 0$
36	34 35	eqtrdi	$⊢ \overline{B - A} (D - C) = 0 \to ℑ (\overline{B - A} (D - C)) = 0$
37	36	necon3i	$⊢ ℑ (\overline{B - A} (D - C)) \neq 0 \to \overline{B - A} (D - C) \neq 0$
38	10 37	syl	$⊢ φ \to \overline{B - A} (D - C) \neq 0$
39	17 21 38	mulne0bbd	$⊢ φ \to D - C \neq 0$
40	33 29 21 39	divmul3d	$⊢ φ \to (\frac{A + T (B - A) - C}{D - C} = R \leftrightarrow A + T (B - A) - C = R (D - C))$
41	32 40	mpbird	$⊢ φ \to \frac{A + T (B - A) - C}{D - C} = R$
42	41	fveq2d	$⊢ φ \to \overline{\frac{A + T (B - A) - C}{D - C}} = \overline{R}$
43	33 21 39	cjdivd	$⊢ φ \to \overline{\frac{A + T (B - A) - C}{D - C}} = \frac{\overline{A + T (B - A) - C}}{\overline{D - C}}$
44	12 16	mulcld	$⊢ φ \to T (B - A) \in ℂ$
45	14 44	addcld	$⊢ φ \to A + T (B - A) \in ℂ$
46	45 20	cjsubd	$⊢ φ \to \overline{A + T (B - A) - C} = \overline{A + T (B - A)} - \overline{C}$
47	14 44	cjaddd	$⊢ φ \to \overline{A + T (B - A)} = \overline{A} + \overline{T (B - A)}$
48	12 16	cjmuld	$⊢ φ \to \overline{T (B - A)} = \overline{T} \overline{B - A}$
49	6	cjred	$⊢ φ \to \overline{T} = T$
50	49 15	oveq12d	$⊢ φ \to \overline{T} \overline{B - A} = T (\overline{B} - \overline{A})$
51	48 50	eqtrd	$⊢ φ \to \overline{T (B - A)} = T (\overline{B} - \overline{A})$
52	51	oveq2d	$⊢ φ \to \overline{A} + \overline{T (B - A)} = \overline{A} + T (\overline{B} - \overline{A})$
53	47 52	eqtrd	$⊢ φ \to \overline{A + T (B - A)} = \overline{A} + T (\overline{B} - \overline{A})$
54	53	oveq1d	$⊢ φ \to \overline{A + T (B - A)} - \overline{C} = \overline{A} + T (\overline{B} - \overline{A}) - \overline{C}$
55	46 54	eqtrd	$⊢ φ \to \overline{A + T (B - A) - C} = \overline{A} + T (\overline{B} - \overline{A}) - \overline{C}$
56	55 23	oveq12d	$⊢ φ \to \frac{\overline{A + T (B - A) - C}}{\overline{D - C}} = \frac{\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}}{\overline{D} - \overline{C}}$
57	43 56	eqtrd	$⊢ φ \to \overline{\frac{A + T (B - A) - C}{D - C}} = \frac{\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}}{\overline{D} - \overline{C}}$
58	7	cjred	$⊢ φ \to \overline{R} = R$
59	42 57 58	3eqtr3rd	$⊢ φ \to R = \frac{\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}}{\overline{D} - \overline{C}}$
60	41 59	eqtrd	$⊢ φ \to \frac{A + T (B - A) - C}{D - C} = \frac{\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}}{\overline{D} - \overline{C}}$
61	14	cjcld	$⊢ φ \to \overline{A} \in ℂ$
62	12 18	mulcld	$⊢ φ \to T (\overline{B} - \overline{A}) \in ℂ$
63	61 62	addcld	$⊢ φ \to \overline{A} + T (\overline{B} - \overline{A}) \in ℂ$
64	20	cjcld	$⊢ φ \to \overline{C} \in ℂ$
65	63 64	subcld	$⊢ φ \to \overline{A} + T (\overline{B} - \overline{A}) - \overline{C} \in ℂ$
66	21 39	cjne0d	$⊢ φ \to \overline{D - C} \neq 0$
67	23 66	eqnetrrd	$⊢ φ \to \overline{D} - \overline{C} \neq 0$
68	33 21 65 25 39 67	divmuleqd	$⊢ φ \to (\frac{A + T (B - A) - C}{D - C} = \frac{\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}}{\overline{D} - \overline{C}} \leftrightarrow (A + T (B - A) - C) (\overline{D} - \overline{C}) = (\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}) (D - C))$
69	60 68	mpbid	$⊢ φ \to (A + T (B - A) - C) (\overline{D} - \overline{C}) = (\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}) (D - C)$
70	14 44 20	addsubassd	$⊢ φ \to A + T (B - A) - C = A + T (B - A) - C$
71	44 14 20	addsub12d	$⊢ φ \to T (B - A) + A - C = A + T (B - A) - C$
72	70 71	eqtr4d	$⊢ φ \to A + T (B - A) - C = T (B - A) + A - C$
73	72	oveq1d	$⊢ φ \to (A + T (B - A) - C) (\overline{D} - \overline{C}) = (T (B - A) + A - C) (\overline{D} - \overline{C})$
74	14 20	subcld	$⊢ φ \to A - C \in ℂ$
75	44 74 25	adddird	$⊢ φ \to (T (B - A) + A - C) (\overline{D} - \overline{C}) = T (B - A) (\overline{D} - \overline{C}) + (A - C) (\overline{D} - \overline{C})$
76	12 16 25	mulassd	$⊢ φ \to T (B - A) (\overline{D} - \overline{C}) = T (B - A) (\overline{D} - \overline{C})$
77	76	oveq1d	$⊢ φ \to T (B - A) (\overline{D} - \overline{C}) + (A - C) (\overline{D} - \overline{C}) = T (B - A) (\overline{D} - \overline{C}) + (A - C) (\overline{D} - \overline{C})$
78	73 75 77	3eqtrd	$⊢ φ \to (A + T (B - A) - C) (\overline{D} - \overline{C}) = T (B - A) (\overline{D} - \overline{C}) + (A - C) (\overline{D} - \overline{C})$
79	61 62 64	addsubassd	$⊢ φ \to \overline{A} + T (\overline{B} - \overline{A}) - \overline{C} = \overline{A} + T (\overline{B} - \overline{A}) - \overline{C}$
80	62 61 64	addsub12d	$⊢ φ \to T (\overline{B} - \overline{A}) + \overline{A} - \overline{C} = \overline{A} + T (\overline{B} - \overline{A}) - \overline{C}$
81	79 80	eqtr4d	$⊢ φ \to \overline{A} + T (\overline{B} - \overline{A}) - \overline{C} = T (\overline{B} - \overline{A}) + \overline{A} - \overline{C}$
82	81	oveq1d	$⊢ φ \to (\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}) (D - C) = (T (\overline{B} - \overline{A}) + \overline{A} - \overline{C}) (D - C)$
83	61 64	subcld	$⊢ φ \to \overline{A} - \overline{C} \in ℂ$
84	62 83 21	adddird	$⊢ φ \to (T (\overline{B} - \overline{A}) + \overline{A} - \overline{C}) (D - C) = T (\overline{B} - \overline{A}) (D - C) + (\overline{A} - \overline{C}) (D - C)$
85	12 18 21	mulassd	$⊢ φ \to T (\overline{B} - \overline{A}) (D - C) = T (\overline{B} - \overline{A}) (D - C)$
86	85	oveq1d	$⊢ φ \to T (\overline{B} - \overline{A}) (D - C) + (\overline{A} - \overline{C}) (D - C) = T (\overline{B} - \overline{A}) (D - C) + (\overline{A} - \overline{C}) (D - C)$
87	82 84 86	3eqtrd	$⊢ φ \to (\overline{A} + T (\overline{B} - \overline{A}) - \overline{C}) (D - C) = T (\overline{B} - \overline{A}) (D - C) + (\overline{A} - \overline{C}) (D - C)$
88	69 78 87	3eqtr3d	$⊢ φ \to T (B - A) (\overline{D} - \overline{C}) + (A - C) (\overline{D} - \overline{C}) = T (\overline{B} - \overline{A}) (D - C) + (\overline{A} - \overline{C}) (D - C)$
89	12 26	mulcld	$⊢ φ \to T (B - A) (\overline{D} - \overline{C}) \in ℂ$
90	74 25	mulcld	$⊢ φ \to (A - C) (\overline{D} - \overline{C}) \in ℂ$
91	12 22	mulcld	$⊢ φ \to T (\overline{B} - \overline{A}) (D - C) \in ℂ$
92	83 21	mulcld	$⊢ φ \to (\overline{A} - \overline{C}) (D - C) \in ℂ$
93	89 90 91 92	addsubeq4d	$⊢ φ \to (T (B - A) (\overline{D} - \overline{C}) + (A - C) (\overline{D} - \overline{C}) = T (\overline{B} - \overline{A}) (D - C) + (\overline{A} - \overline{C}) (D - C) \leftrightarrow T (\overline{B} - \overline{A}) (D - C) - T (B - A) (\overline{D} - \overline{C}) = (A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C))$
94	88 93	mpbid	$⊢ φ \to T (\overline{B} - \overline{A}) (D - C) - T (B - A) (\overline{D} - \overline{C}) = (A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)$
95	27 94	eqtrd	$⊢ φ \to T ((\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})) = (A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)$
96	22 26	subcld	$⊢ φ \to (\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C}) \in ℂ$
97	90 92	subcld	$⊢ φ \to (A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C) \in ℂ$
98	17 21	mulcld	$⊢ φ \to \overline{B - A} (D - C) \in ℂ$
99		reim0b	$⊢ \overline{B - A} (D - C) \in ℂ \to (\overline{B - A} (D - C) \in ℝ \leftrightarrow ℑ (\overline{B - A} (D - C)) = 0)$
100	98 99	syl	$⊢ φ \to (\overline{B - A} (D - C) \in ℝ \leftrightarrow ℑ (\overline{B - A} (D - C)) = 0)$
101	100	necon3bbid	$⊢ φ \to (\neg \overline{B - A} (D - C) \in ℝ \leftrightarrow ℑ (\overline{B - A} (D - C)) \neq 0)$
102	10 101	mpbird	$⊢ φ \to \neg \overline{B - A} (D - C) \in ℝ$
103		cjreb	$⊢ \overline{B - A} (D - C) \in ℂ \to (\overline{B - A} (D - C) \in ℝ \leftrightarrow \overline{\overline{B - A} (D - C)} = \overline{B - A} (D - C))$
104	98 103	syl	$⊢ φ \to (\overline{B - A} (D - C) \in ℝ \leftrightarrow \overline{\overline{B - A} (D - C)} = \overline{B - A} (D - C))$
105	104	necon3bbid	$⊢ φ \to (\neg \overline{B - A} (D - C) \in ℝ \leftrightarrow \overline{\overline{B - A} (D - C)} \neq \overline{B - A} (D - C))$
106	102 105	mpbid	$⊢ φ \to \overline{\overline{B - A} (D - C)} \neq \overline{B - A} (D - C)$
107	17 21	cjmuld	$⊢ φ \to \overline{\overline{B - A} (D - C)} = \overline{\overline{B - A}} \overline{D - C}$
108	16	cjcjd	$⊢ φ \to \overline{\overline{B - A}} = B - A$
109	108 23	oveq12d	$⊢ φ \to \overline{\overline{B - A}} \overline{D - C} = (B - A) (\overline{D} - \overline{C})$
110	107 109	eqtrd	$⊢ φ \to \overline{\overline{B - A} (D - C)} = (B - A) (\overline{D} - \overline{C})$
111	15	oveq1d	$⊢ φ \to \overline{B - A} (D - C) = (\overline{B} - \overline{A}) (D - C)$
112	106 110 111	3netr3d	$⊢ φ \to (B - A) (\overline{D} - \overline{C}) \neq (\overline{B} - \overline{A}) (D - C)$
113	112	necomd	$⊢ φ \to (\overline{B} - \overline{A}) (D - C) \neq (B - A) (\overline{D} - \overline{C})$
114	22 26 113	subne0d	$⊢ φ \to (\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C}) \neq 0$
115	12 96 97 114	ldiv	$⊢ φ \to (T ((\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})) = (A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C) \leftrightarrow T = \frac{(A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)}{(\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})})$
116	95 115	mpbid	$⊢ φ \to T = \frac{(A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)}{(\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})}$
117	116	oveq1d	$⊢ φ \to T (B - A) = (\frac{(A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)}{(\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})}) (B - A)$
118	117	oveq2d	$⊢ φ \to A + T (B - A) = A + (\frac{(A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)}{(\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})}) (B - A)$
119	8 118	eqtrd	$⊢ φ \to X = A + (\frac{(A - C) (\overline{D} - \overline{C}) - (\overline{A} - \overline{C}) (D - C)}{(\overline{B} - \overline{A}) (D - C) - (B - A) (\overline{D} - \overline{C})}) (B - A)$
120	119 11	eqtr4di	$⊢ φ \to X = N$

Metamath Proof Explorer

Theorem constrrtll

Proof