constrrtlc1

Description: In the construction of constructible numbers, line-circle intersections are roots of a quadratic equation, non-degenerate case. (Contributed by Thierry Arnoux, 6-Jul-2025)

	Ref	Expression
Hypotheses	constrrtlc.s	$⊢ φ \to S \subseteq ℂ$
	constrrtlc.a	$⊢ φ \to A \in S$
	constrrtlc.b	$⊢ φ \to B \in S$
	constrrtlc.c	$⊢ φ \to C \in S$
	constrrtlc.e	$⊢ φ \to E \in S$
	constrrtlc.f	$⊢ φ \to F \in S$
	constrrtlc.t	$⊢ φ \to T \in ℝ$
	constrrtlc.1	$⊢ φ \to X = A + T (B - A)$
	constrrtlc.2	$⊢ φ \to \|X - C\| = \|E - F\|$
	constrrtlc.q	$⊢ Q = \frac{\overline{B} - \overline{A}}{B - A}$
	constrrtlc.m	$⊢ M = \frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q}$
	constrrtlc.n	$⊢ N = \frac{- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))}{Q}$
	constrrtlc1.1	$⊢ φ \to A \neq B$
Assertion	constrrtlc1	$⊢ φ \to (X^{2} + M X + N = 0 \land Q \neq 0)$

Proof

Step	Hyp	Ref	Expression
1		constrrtlc.s	$⊢ φ \to S \subseteq ℂ$
2		constrrtlc.a	$⊢ φ \to A \in S$
3		constrrtlc.b	$⊢ φ \to B \in S$
4		constrrtlc.c	$⊢ φ \to C \in S$
5		constrrtlc.e	$⊢ φ \to E \in S$
6		constrrtlc.f	$⊢ φ \to F \in S$
7		constrrtlc.t	$⊢ φ \to T \in ℝ$
8		constrrtlc.1	$⊢ φ \to X = A + T (B - A)$
9		constrrtlc.2	$⊢ φ \to \|X - C\| = \|E - F\|$
10		constrrtlc.q	$⊢ Q = \frac{\overline{B} - \overline{A}}{B - A}$
11		constrrtlc.m	$⊢ M = \frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q}$
12		constrrtlc.n	$⊢ N = \frac{- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))}{Q}$
13		constrrtlc1.1	$⊢ φ \to A \neq B$
14	1 2	sseldd	$⊢ φ \to A \in ℂ$
15	14	cjcld	$⊢ φ \to \overline{A} \in ℂ$
16	1 3	sseldd	$⊢ φ \to B \in ℂ$
17	16	cjcld	$⊢ φ \to \overline{B} \in ℂ$
18	17 15	subcld	$⊢ φ \to \overline{B} - \overline{A} \in ℂ$
19	16 14	subcld	$⊢ φ \to B - A \in ℂ$
20	13	necomd	$⊢ φ \to B \neq A$
21	16 14 20	subne0d	$⊢ φ \to B - A \neq 0$
22	18 19 21	divcld	$⊢ φ \to \frac{\overline{B} - \overline{A}}{B - A} \in ℂ$
23	10 22	eqeltrid	$⊢ φ \to Q \in ℂ$
24	14 23	mulcld	$⊢ φ \to A Q \in ℂ$
25	15 24	subcld	$⊢ φ \to \overline{A} - A Q \in ℂ$
26	1 4	sseldd	$⊢ φ \to C \in ℂ$
27	26	cjcld	$⊢ φ \to \overline{C} \in ℂ$
28	25 27	subcld	$⊢ φ \to \overline{A} - A Q - \overline{C} \in ℂ$
29	26 23	mulcld	$⊢ φ \to C Q \in ℂ$
30	28 29	subcld	$⊢ φ \to (\overline{A} - A Q) - \overline{C} - C Q \in ℂ$
31	16 14	cjsubd	$⊢ φ \to \overline{B - A} = \overline{B} - \overline{A}$
32	19 21	cjne0d	$⊢ φ \to \overline{B - A} \neq 0$
33	31 32	eqnetrrd	$⊢ φ \to \overline{B} - \overline{A} \neq 0$
34	18 19 33 21	divne0d	$⊢ φ \to \frac{\overline{B} - \overline{A}}{B - A} \neq 0$
35	10	neeq1i	$⊢ Q \neq 0 \leftrightarrow \frac{\overline{B} - \overline{A}}{B - A} \neq 0$
36	34 35	sylibr	$⊢ φ \to Q \neq 0$
37	30 23 36	divcld	$⊢ φ \to \frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q} \in ℂ$
38	7	recnd	$⊢ φ \to T \in ℂ$
39	38 19	mulcld	$⊢ φ \to T (B - A) \in ℂ$
40	14 39	addcld	$⊢ φ \to A + T (B - A) \in ℂ$
41	8 40	eqeltrd	$⊢ φ \to X \in ℂ$
42	37 41	mulcomd	$⊢ φ \to (\frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q}) X = X (\frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q})$
43	11	a1i	$⊢ φ \to M = \frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q}$
44	43	oveq1d	$⊢ φ \to M X = (\frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q}) X$
45	41 30 23 36	divassd	$⊢ φ \to \frac{X ((\overline{A} - A Q) - \overline{C} - C Q)}{Q} = X (\frac{(\overline{A} - A Q) - \overline{C} - C Q}{Q})$
46	42 44 45	3eqtr4d	$⊢ φ \to M X = \frac{X ((\overline{A} - A Q) - \overline{C} - C Q)}{Q}$
47	12	a1i	$⊢ φ \to N = \frac{- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))}{Q}$
48	46 47	oveq12d	$⊢ φ \to M X + N = (\frac{X ((\overline{A} - A Q) - \overline{C} - C Q)}{Q}) + (\frac{- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))}{Q})$
49	41 30	mulcld	$⊢ φ \to X ((\overline{A} - A Q) - \overline{C} - C Q) \in ℂ$
50	26 28	mulcld	$⊢ φ \to C (\overline{A} - A Q - \overline{C}) \in ℂ$
51	41	sqvald	$⊢ φ \to X^{2} = X X$
52	51	oveq1d	$⊢ φ \to X^{2} Q = X X Q$
53	41 41 23	mulassd	$⊢ φ \to X X Q = X X Q$
54	52 53	eqtrd	$⊢ φ \to X^{2} Q = X X Q$
55	41 23	mulcld	$⊢ φ \to X Q \in ℂ$
56	41 55	mulcld	$⊢ φ \to X X Q \in ℂ$
57	54 56	eqeltrd	$⊢ φ \to X^{2} Q \in ℂ$
58	57 49 50	addsubd	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) - C (\overline{A} - A Q - \overline{C}) = X^{2} Q - C (\overline{A} - A Q - \overline{C}) + X ((\overline{A} - A Q) - \overline{C} - C Q)$
59	54	oveq1d	$⊢ φ \to X^{2} Q - C (\overline{A} - A Q - \overline{C}) = X X Q - C (\overline{A} - A Q - \overline{C})$
60	41 28 29	subdid	$⊢ φ \to X ((\overline{A} - A Q) - \overline{C} - C Q) = X (\overline{A} - A Q - \overline{C}) - X C Q$
61	59 60	oveq12d	$⊢ φ \to X^{2} Q - C (\overline{A} - A Q - \overline{C}) + X ((\overline{A} - A Q) - \overline{C} - C Q) = (X X Q - C (\overline{A} - A Q - \overline{C})) + X (\overline{A} - A Q - \overline{C}) - X C Q$
62	41 28	mulcld	$⊢ φ \to X (\overline{A} - A Q - \overline{C}) \in ℂ$
63	41 29	mulcld	$⊢ φ \to X C Q \in ℂ$
64	56 62 50 63	addsub4d	$⊢ φ \to X X Q + X (\overline{A} - A Q - \overline{C}) - (C (\overline{A} - A Q - \overline{C}) + X C Q) = (X X Q - C (\overline{A} - A Q - \overline{C})) + X (\overline{A} - A Q - \overline{C}) - X C Q$
65	41 26 55 28	submuladdd	$⊢ φ \to (X - C) (X Q + (\overline{A} - A Q) - \overline{C}) = X X Q + X (\overline{A} - A Q - \overline{C}) - (C X Q + C (\overline{A} - A Q - \overline{C}))$
66	9	oveq1d	$⊢ φ \to {\|X - C\|}^{2} = {\|E - F\|}^{2}$
67	41 26	subcld	$⊢ φ \to X - C \in ℂ$
68	67	absvalsqd	$⊢ φ \to {\|X - C\|}^{2} = (X - C) \overline{X - C}$
69	1 5	sseldd	$⊢ φ \to E \in ℂ$
70	1 6	sseldd	$⊢ φ \to F \in ℂ$
71	69 70	subcld	$⊢ φ \to E - F \in ℂ$
72	71	absvalsqd	$⊢ φ \to {\|E - F\|}^{2} = (E - F) \overline{E - F}$
73	66 68 72	3eqtr3d	$⊢ φ \to (X - C) \overline{X - C} = (E - F) \overline{E - F}$
74	8	fvoveq1d	$⊢ φ \to \overline{X - C} = \overline{A + T (B - A) - C}$
75	40 26	cjsubd	$⊢ φ \to \overline{A + T (B - A) - C} = \overline{A + T (B - A)} - \overline{C}$
76	14 39	cjaddd	$⊢ φ \to \overline{A + T (B - A)} = \overline{A} + \overline{T (B - A)}$
77	38 19	cjmuld	$⊢ φ \to \overline{T (B - A)} = \overline{T} \overline{B - A}$
78	7	cjred	$⊢ φ \to \overline{T} = T$
79	14 39 8	mvrladdd	$⊢ φ \to X - A = T (B - A)$
80	79 39	eqeltrd	$⊢ φ \to X - A \in ℂ$
81	80 38 19 21	divmul3d	$⊢ φ \to (\frac{X - A}{B - A} = T \leftrightarrow X - A = T (B - A))$
82	79 81	mpbird	$⊢ φ \to \frac{X - A}{B - A} = T$
83	78 82	eqtr4d	$⊢ φ \to \overline{T} = \frac{X - A}{B - A}$
84	83 31	oveq12d	$⊢ φ \to \overline{T} \overline{B - A} = (\frac{X - A}{B - A}) (\overline{B} - \overline{A})$
85	80 19 18 21	div32d	$⊢ φ \to (\frac{X - A}{B - A}) (\overline{B} - \overline{A}) = (X - A) (\frac{\overline{B} - \overline{A}}{B - A})$
86	10	oveq2i	$⊢ (X - A) Q = (X - A) (\frac{\overline{B} - \overline{A}}{B - A})$
87	85 86	eqtr4di	$⊢ φ \to (\frac{X - A}{B - A}) (\overline{B} - \overline{A}) = (X - A) Q$
88	41 14 23	subdird	$⊢ φ \to (X - A) Q = X Q - A Q$
89	84 87 88	3eqtrd	$⊢ φ \to \overline{T} \overline{B - A} = X Q - A Q$
90	77 89	eqtrd	$⊢ φ \to \overline{T (B - A)} = X Q - A Q$
91	90	oveq2d	$⊢ φ \to \overline{A} + \overline{T (B - A)} = \overline{A} + X Q - A Q$
92	15 55 24	addsub12d	$⊢ φ \to \overline{A} + X Q - A Q = X Q + \overline{A} - A Q$
93	76 91 92	3eqtrd	$⊢ φ \to \overline{A + T (B - A)} = X Q + \overline{A} - A Q$
94	93	oveq1d	$⊢ φ \to \overline{A + T (B - A)} - \overline{C} = X Q + (\overline{A} - A Q) - \overline{C}$
95	55 25 27	addsubassd	$⊢ φ \to X Q + (\overline{A} - A Q) - \overline{C} = X Q + (\overline{A} - A Q) - \overline{C}$
96	75 94 95	3eqtrd	$⊢ φ \to \overline{A + T (B - A) - C} = X Q + (\overline{A} - A Q) - \overline{C}$
97	74 96	eqtrd	$⊢ φ \to \overline{X - C} = X Q + (\overline{A} - A Q) - \overline{C}$
98	97	oveq2d	$⊢ φ \to (X - C) \overline{X - C} = (X - C) (X Q + (\overline{A} - A Q) - \overline{C})$
99	69 70	cjsubd	$⊢ φ \to \overline{E - F} = \overline{E} - \overline{F}$
100	99	oveq2d	$⊢ φ \to (E - F) \overline{E - F} = (E - F) (\overline{E} - \overline{F})$
101	73 98 100	3eqtr3d	$⊢ φ \to (X - C) (X Q + (\overline{A} - A Q) - \overline{C}) = (E - F) (\overline{E} - \overline{F})$
102	26 41 23	mul12d	$⊢ φ \to C X Q = X C Q$
103	102	oveq1d	$⊢ φ \to C X Q + C (\overline{A} - A Q - \overline{C}) = X C Q + C (\overline{A} - A Q - \overline{C})$
104	63 50 103	comraddd	$⊢ φ \to C X Q + C (\overline{A} - A Q - \overline{C}) = C (\overline{A} - A Q - \overline{C}) + X C Q$
105	104	oveq2d	$⊢ φ \to X X Q + X (\overline{A} - A Q - \overline{C}) - (C X Q + C (\overline{A} - A Q - \overline{C})) = X X Q + X (\overline{A} - A Q - \overline{C}) - (C (\overline{A} - A Q - \overline{C}) + X C Q)$
106	65 101 105	3eqtr3rd	$⊢ φ \to X X Q + X (\overline{A} - A Q - \overline{C}) - (C (\overline{A} - A Q - \overline{C}) + X C Q) = (E - F) (\overline{E} - \overline{F})$
107	61 64 106	3eqtr2d	$⊢ φ \to X^{2} Q - C (\overline{A} - A Q - \overline{C}) + X ((\overline{A} - A Q) - \overline{C} - C Q) = (E - F) (\overline{E} - \overline{F})$
108	58 107	eqtrd	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) - C (\overline{A} - A Q - \overline{C}) = (E - F) (\overline{E} - \overline{F})$
109	57 49	addcld	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) \in ℂ$
110	109 50	subcld	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) - C (\overline{A} - A Q - \overline{C}) \in ℂ$
111	108 110	eqeltrrd	$⊢ φ \to (E - F) (\overline{E} - \overline{F}) \in ℂ$
112	50 111	addcld	$⊢ φ \to C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}) \in ℂ$
113	112	negcld	$⊢ φ \to - (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})) \in ℂ$
114	49 113 23 36	divdird	$⊢ φ \to \frac{X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))}{Q} = (\frac{X ((\overline{A} - A Q) - \overline{C} - C Q)}{Q}) + (\frac{- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))}{Q})$
115	48 114	eqtr4d	$⊢ φ \to M X + N = \frac{X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))}{Q}$
116	115	oveq2d	$⊢ φ \to X^{2} + M X + N = X^{2} + (\frac{X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))}{Q})$
117	41	sqcld	$⊢ φ \to X^{2} \in ℂ$
118	49 113	addcld	$⊢ φ \to X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))) \in ℂ$
119	117 23 118 36	muldivdid	$⊢ φ \to \frac{X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))}{Q} = X^{2} + (\frac{X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))}{Q})$
120	57 49 113	addassd	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))) = X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))$
121	109 112	negsubd	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))) = X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) - (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))$
122	109 50 111	subsub4d	$⊢ φ \to (X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q)) - C (\overline{A} - A Q - \overline{C}) - (E - F) (\overline{E} - \overline{F}) = X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) - (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))$
123	110 108	subeq0bd	$⊢ φ \to (X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q)) - C (\overline{A} - A Q - \overline{C}) - (E - F) (\overline{E} - \overline{F}) = 0$
124	121 122 123	3eqtr2d	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))) = 0$
125	120 124	eqtr3d	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))) = 0$
126	57 118	addcld	$⊢ φ \to X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))) \in ℂ$
127	126 23 36	diveq0ad	$⊢ φ \to (\frac{X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))}{Q} = 0 \leftrightarrow X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F}))) = 0)$
128	125 127	mpbird	$⊢ φ \to \frac{X^{2} Q + X ((\overline{A} - A Q) - \overline{C} - C Q) + (- (C (\overline{A} - A Q - \overline{C}) + (E - F) (\overline{E} - \overline{F})))}{Q} = 0$
129	116 119 128	3eqtr2d	$⊢ φ \to X^{2} + M X + N = 0$
130	129 36	jca	$⊢ φ \to (X^{2} + M X + N = 0 \land Q \neq 0)$

Metamath Proof Explorer

Theorem constrrtlc1

Proof